Automatic verification of refinement
Wing Sang Lee, Mark R. Greenstreet, C.-J.H. Seger · 2002
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.>