Loading...
Please wait, while we are loading the content...
Similar Documents
Specification and verification of gate-level vhdl models of synchronous and asynchronous circuits
| Content Provider | NASA Technical Reports Server (NTRS) |
|---|---|
| Author | Russinoff, David M. |
| Copyright Year | 1995 |
| Description | We present a mathematical definition of hardware description language (HDL) that admits a semantics-preserving translation to a subset of VHDL. Our HDL includes the basic VHDL propagation delay mechanisms and gate-level circuit descriptions. We also develop formal procedures for deriving and verifying concise behavioral specifications of combinational and sequential devices. The HDL and the specification procedures have been formally encoded in the computational logic of Boyer and Moore, which provides a LISP implementation as well as a facility for mechanical proof-checking. As an application, we design, specify, and verify a circuit that achieves asynchronous communication by means of the biphase mark protocol. |
| File Size | 4271189 |
| Page Count | 144 |
| File Format | |
| Alternate Webpage(s) | http://archive.org/details/NASA_NTRS_Archive_19950016413 |
| Archival Resource Key | ark:/13960/t8md3vk76 |
| Language | English |
| Publisher Date | 1995-01-01 |
| Access Restriction | Open |
| Subject Keyword | Hardware Description Languages Protocol Computers Proving Mathematical Logic Mathematical Models Delay Circuits Lisp Programming Language Program Verification Computers Vhsic Circuits Ntrs Nasa Technical Reports Server (ntrs) Nasa Technical Reports Server Aerodynamics Aircraft Aerospace Engineering Aerospace Aeronautic Space Science |
| Content Type | Text |
| Resource Type | Technical Report |
