Sciweavers

DAC
2007
ACM

Memory Modeling in ESL-RTL Equivalence Checking

13 years 7 months ago
Memory Modeling in ESL-RTL Equivalence Checking
When designers create RTL models from a system-level specification, arrays in the system-level model are often implemented as memories in the RTL. Knowing the correspondence between ESL arrays and RTL memories can significantly reduce the complexity of a formal equivalence check between the ESL model and the RTL. In practice, however, handling memory mappings in ESLRTL equivalence checking is non-trivial for the following reasons: First, because of a lack of bit-accurate data-types in the systemlevel language, the information stored in an array location may be stored in a compressed form in the RTL. Second, a single array in the ESL model may be implemented by multiple memories in the RTL and/or corresponding data items may be stored in different locations. And last but not least, due to timing differences between the ESL model and the RTL, the correspondence between arrays and memories may not hold in every clock cycle. In this paper, we propose an approach to ESL-RTL equivalence che...
Alfred Kölbl, Jerry R. Burch, Carl Pixley
Added 14 Aug 2010
Updated 14 Aug 2010
Type Conference
Year 2007
Where DAC
Authors Alfred Kölbl, Jerry R. Burch, Carl Pixley
Comments (0)