Embedded tutorial: formal equivalence checking between system-level models and RTL
2005
A rigorous system-level model (SLM) for a hardware design project is extremely important, often critical. Such a functional model not only defines the architect's ideas but also builds a precise foundation for both hardware designers and verification engineers. The key uses of SLMs are: architecture validation; performance modeling and architectural trade-off; platforms for software development and verification; and functional reference model. In this tutorial, we discuss how to formally verify sequential equivalence between SLMs and RTL, for both timed and untimed models. First, we provide a formal definition of the sequential equivalence. Then we discuss various formal verification technology that enables such practice in real designs.
Keywords:
- Computer architecture
- Computer science
- Hardware architecture
- Formal equivalence checking
- Formal methods
- Intelligent verification
- Verification
- High-level verification
- Functional verification
- Formal verification
- Programming language
- Runtime verification
- Software verification
- Computer engineering
- Real-time computing
- Correction
- Source
- Cite
- Save
- Machine Reading By IdeaReader
9
References
28
Citations
NaN
KQI