Abstract
The Forte formal verification environment for datapath-dominated hardware is described. Forte has proven to be effective in large-scale industrial trials and combines an efficient linear-time logic model-checking algorithm, namely the symbolic trajectory evaluation (STE), with lightweight theorem proving in higher-order logic. These are tightly integrated in a general-purpose functional programming language, which both allows the system to be easily customized and at the same time serves as a specification language. The design philosophy behind Forte is presented and the elements of the verification methodology that make it effective in practice are also described.
Original language | English (US) |
---|---|
Pages (from-to) | 1381-1404 |
Number of pages | 24 |
Journal | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |
Volume | 24 |
Issue number | 9 |
DOIs | |
State | Published - Sep 2005 |
Keywords
- BDDs
- Formal verification
- Model checking
- Symbolic trajectory evaluation
- Theorem proving
ASJC Scopus subject areas
- Software
- Computer Graphics and Computer-Aided Design
- Electrical and Electronic Engineering