Title :
Automatic verification of refinement
Author :
Greenstreet, Mark R. ; Seger, C.-J.
Abstract :
Given two models of a circuit, Q and Q´, we say that Q´ as a refinement of Q if every possible behavior of Q´ is allowed by Q. We present a unified framework for verifying refinement using both model-checking and symbolic trajectory evaluation techniques. In this framework, the refinement conditions are derived and verified automatically. To demonstrate this approach, we present a design for a synchronizer circuit used in a high-speed synchronous design
Keywords :
VLSI; formal verification; network synthesis; synchronisation; automatic verification; circuit models; high-speed synchronous design; model-checking; refinement conditions; refinement verification; symbolic trajectory evaluation; synchronizer circuit; Boolean functions; Circuits; Computer science; Councils; Data structures; Hardware; Safety; State-space methods; Sun; Very large scale integration;
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 1994. ICCD '94. Proceedings., IEEE International Conference on
Conference_Location :
Cambridge, MA
Print_ISBN :
0-8186-6565-3
DOI :
10.1109/ICCD.1994.331894
