Some Examples of Verifying Stage 1 Hardware Descriptions Using the State Delta Verification System (SDVS).
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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 30, 1962
- Accession Number
- ADA288813
Entities
People
- B. H. Levy
- I. V. Filippenko
- J. M. Boulder
Organizations
- The Aerospace Corporation