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
Distribution Statement : APPROVED FOR PUBLIC RELEASE