Distinguishing formulas for free
- 1 January 1993
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 105-110
- https://doi.org/10.1109/edac.1993.386492
Abstract
A system for the efficient verification of the input/output correctness of finite state machines with data path and control unit is presented. This system, which is based on First-Order Logic theorem proving, automatically provides distinguishing formulas expressing all test patterns that witness a behavioral difference between two descriptions. Experimental results illustrate the test pattern generation feature for stuck-at faults, functional faults, and initialization faults, and the efficiency which results from the compositionality of the verification.Keywords
This publication has 5 references indexed in Scilit:
- Automated RTL verification based on predicate calculusPublished by Springer Nature ,2005
- A data path verifier for register transfer level using temporal logic language TokioPublished by Springer Nature ,2005
- Formal verification of design correctness of sequential circuits based on theorem proversPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Verification of synchronous circuits by symbolic logic simulationPublished by Springer Nature ,1990
- Graph-Based Algorithms for Boolean Function ManipulationIEEE Transactions on Computers, 1986