DID YOU KNOW? DTIC has over 3.5 million final reports on DoD funded research, development, test, and evaluation activities available to our registered users. Click HERE
to register or log in.
Some Examples of Verifying Stage 1 Hardware Descriptions Using the State Delta Verification System (SDVS).
AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP
Pagination or Media Count:
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.
APPROVED FOR PUBLIC RELEASE