Accession Number:

ADA288813

Title:

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

Descriptive Note:

Corporate Author:

AEROSPACE CORP EL SEGUNDO CA ENGINEERING AND TECHNOLOGY GROUP

Personal Author(s):

• Filippenko, I. V.
• Boulder, J. M.
• Levy, B. H.

Report Date:

1962-09-30

Pagination or Media Count:

71.0

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