Automatic verification of refinement

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 refine...

Full description

Saved in:
Bibliographic Details
Main Authors: Wing Sang Lee, Greenstreet, M.R., Seger, C.-J.
Format: Conference Proceeding
Language:English
Subjects:
Boolean functions
Circuits
Computer science
Councils
Data structures
Hardware
Safety
State-space methods
Sun
Very large scale integration
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.< >
DOI:10.1109/ICCD.1994.331894