Name
Title | ||
|---|---|---|
A New Verification Technique for Custom-Designed Components at the Arithmetic Bit Level |
Abstract | ||
|---|---|---|
Arithmetic Bit-Level (ABL) normalization has been proven a viable approach to formal property checking of datapath designs.
It is applicable where arithmetic bit level components and sub-components can be identified at the register-transfer (RT)
level of the design and the property. This chapter extends the applicability of ABL normalization to cases where some of the
arithmetic components are custom-designed entities, e.g., specified using Boolean equations or gates. We transform these entities
into ABL building blocks using Reed–Muller expressions as an intermediate representation. We show how Boolean logic expressed
in Reed–Muller form can be automatically transformed into ABL components so that such logic blocks can be treated together
with the remaining ABL components in a subsequent normalization run. The approach is evaluated on a number of industrial designs
generated by a commercial arithmetic module generator.
|
Year | DOI | Venue |
|---|---|---|
2009 | 10.1007/978-1-4020-9714-0_17 | FDL |
Keywords | Field | DocType |
custom-designed component · reed-muller expansion · abl normalization | Datapath,Normalization (statistics),Model checking,Bit slicing,Arbitrary-precision arithmetic,Computer science,Arithmetic,Boolean algebra,High-level verification,Saturation arithmetic | Conference |
Citations | PageRank | References |
0 | 0.34 | 14 |
Authors | ||
6 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Evgeny Pavlenko | 1 | 7 | 4.21 |
| Markus Wedler | 2 | 77 | 12.44 |
| Dominik Stoffel | 3 | 176 | 28.93 |
| Wolfgang Kunz | 4 | 236 | 33.71 |
| Oliver Wienand | 5 | 30 | 4.69 |
| Evgeny Karibaev | 6 | 2 | 0.73 |