Accession Number : ADA337948

Title :   Evaluation of the Larch/VHDL Interactive Prover in Hardware Verification

Corporate Author : ROME LAB ROME NY

Personal Author(s) : Paragi, Robert J. ; Nassif, Michael P. ; Stabler, Edward P.

PDF Url : ADA337948

Report Date : OCT 1997

Pagination or Media Count : 42

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.

Descriptors :   *COMPUTER AIDED DESIGN, *COMPUTER PROGRAM VERIFICATION, TEST AND EVALUATION, COMPUTER COMMUNICATIONS, SPECIFICATIONS, INTEGRATED CIRCUITS, MULTIPROCESSORS, DESIGN CRITERIA, HIGH LEVEL LANGUAGES, SIMULATION LANGUAGES, STRUCTURED PROGRAMMING.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE