Accession Number : ADA288813

Title :   Some Examples of Verifying Stage 1 Hardware Descriptions Using the State Delta Verification System (SDVS).

Corporate Author : AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP

Personal Author(s) : Filippenko, I. V. ; Boulder, J. M. ; Levy, B. H.

PDF Url : ADA288813

Report Date : 30 SEP 1962

Pagination or Media Count : 71

Abstract : We illustrate, by a sequence of examples, how the State Delta Verification System (SDVS) can be used to create formal specifications and correctness proofs for hardware descriptions in Stage 1 VHDL, a subset of the VHSIC Hardware Description Language (VHDL). The examples include the following: a handshake protocol for interprocess communication, a counter, a description involving TRANSPORT delay, a description involving a WAIT statement embedded in a conditional, a description involving a WAIT statement embedded in a loop, a description involving an EXIT from a nested loop, a shift-and-add multiplier. Of these, the first two and the last are realistic hardware descriptions, while the remainder are intended to demonstrate the additional functionality of Stage 1 VHDL compared to Core VHDL, the original SDVS VHDL language subset.

Descriptors :   *COMPUTER ARCHITECTURE, *COMPUTER PROGRAM VERIFICATION, COMPUTER COMMUNICATIONS, INTEGRATED CIRCUITS, TRANSPORT, DELAY, HIGH LEVEL LANGUAGES, DIGITAL COMPUTERS.

Subject Categories : Computer Programming and Software
      Computer Hardware

Distribution Statement : APPROVED FOR PUBLIC RELEASE