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

摘要

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.