A correct-by-construction methodology for designing symmetric circuits
Ashish Darbari · ePrints Soton (University of Southampton) · 2007
Symbolic trajectory evaluation [1] or STE in short has been successfully used in verification of large industrial sized circuit designs [2]. However, the data abstraction in STE via Xs is often insufficient to bring about any reasonable reduction in the size of the verification of memory based circuits such as random access memories (RAM), content addressable memories (CAM) and caches. Memory based circuits offer a significant opportunity in achieving a reduction in the size of the verification problem due to the inherent symmetry in their structure. Our overall research goal is to develop a symmetry based reduction methodology for STE model checking. Two key problems have to be addressed in any symmetry based reduction approach for model checking hardware. These are: