Formal verification of design correctness of sequential circuits based on theorem provers
- 10 December 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
After a presentation of alternative time modeling techniques, the description techniques available in OTTER, a first-order logic proof environment at the different abstraction levels are presented. A discussion is presented of the methodology envisaged for the proof of correctness and its implementation in OTTER depending on the circuit characteristics and on the reasoning technique. Some experimental results are also reported.Keywords
This publication has 6 references indexed in Scilit:
- Resolution-based correctness proofs of synchronous circuitsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Formal Boolean manipulations for the verification of sequential machinesPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Assessing the diagnostic power of test pattern setsMicroprocessing and Microprogramming, 1990
- Formal verification of hardware correctness: introduction and survey of current researchComputer, 1988
- An algebra of processesJournal of Computer and System Sciences, 1987
- Macro Testing: Unifying IC And Board TestIEEE Design & Test of Computers, 1986