DocumentCode
2160963
Title
Automatic verification of refinement
Author
Greenstreet, Mark R. ; Seger, C.-J.
fYear
1994
fDate
10-12 Oct 1994
Firstpage
226
Lastpage
229
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/ICCD.1994.331894
Filename
331894
Link To Document