Evaluation of the Larch/VHDL Interactive Prover in Hardware Verification
Abstract
This report concludes an in-house evaluation of the Larch/VHDL hardware design verification tool. The evaluation is part of a larger activity to transition Larch/VHDL from a research phase to application usage within universities and industry. The Larch/VHDL tool environment has been developed by Odyssey Research Associates (ORA) under a contract with Rome Laboratory that combines a specification language, Larch, with a widely used hardware design language, VHSIC Hardware Description Language (VHDL). These two notations provide a highly structured input to the third major component of the tool environment, the Penelope theorem prover, also developed by ORA under Rome Laboratory contract. In conjunction with traditional hardware design simulation, the theorem prover provides a compact methodology for verifying correctness of a design which otherwise would be computationally unfeasible with simulation alone. The evaluation has shown that significant portions of completed verification work on one portion of a design can be reused for proving correctness of other portions of the design.
Document Details
- Document Type
- Technical Report
- Publication Date
- Oct 01, 1997
- Accession Number
- ADA337948
Entities
People
- Edward P. Stabler
- Michael P. Nassif
- Robert J. Paragi
Organizations
- Rome Laboratory