A simple theorem prover based on symbolic trajectory evaluation and BDD's

Formal hardware verification based on symbolic trajectory evaluation shows considerable promise in verifying medium to large scale VLSI designs with a high degree of automation. However, in order to verify today's designs, a method for composing partial verification results is needed. This pape...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on computer-aided design of integrated circuits and systems 1995-04, Vol.14 (4), p.413-422
Main Authors: Hazelhurst, S., Seger, C.-J.H.
Format: Article
Language:English
Subjects:
Applied sciences
Boolean functions
Circuits
Data structures
Design automation
Design methodology
Design. Technologies. Operation analysis. Testing
Electronics
Exact sciences and technology
Hardware
Humans
Integrated circuits
Large-scale systems
Logic
Semiconductor electronics. Microelectronics. Optoelectronics. Solid state devices
Very large scale integration
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Formal hardware verification based on symbolic trajectory evaluation shows considerable promise in verifying medium to large scale VLSI designs with a high degree of automation. However, in order to verify today's designs, a method for composing partial verification results is needed. This paper presents a theory of composition for symbolic trajectory evaluation and shows how implementing this theory using a specialized theorem prover is very attractive. Symbolic trajectory evaluation is used to prove low level properties of a circuit, and these properties are combined using the prover. Providing a powerful and flexible interface to a coherent system (with automatic assistance in parts) reduces the load on the human verifier. This hybrid approach, coupled with powerful and simple data representation, increases the range of circuits which can be verified using trajectory evaluation. The paper concludes with two examples. One example is the complete verification of a 64 b multiplier which takes approximately 15 minutes on a SPARC 10 machine.< >
ISSN:0278-0070
1937-4151
DOI:10.1109/43.372367