NASA Logo

NTRS

NTRS - NASA Technical Reports Server

Collections About News Help Login
Back to Results
Specification and verification of gate-level VHDL models of synchronous and asynchronous circuitsWe 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.
Document ID
19950016413
Acquisition Source
Legacy CDMS
Document Type
Contractor Report (CR)
Authors
Russinoff, David M. (Computational Logic, Inc. Austin, TX, United States)
Date Acquired
September 6, 2013
Publication Date
January 1, 1995
Subject Category
Computer Systems
Report/Patent Number
NAS 1.26:191608
NASA-CR-191608
Accession Number
95N22830
Funding Number(s)
PROJECT: RTOP 506-64-10-13
CONTRACT_GRANT: NAS1-18878
Distribution Limits
Public
Copyright
Work of the US Gov. Public Use Permitted.

Related Records

There are no records associated with this record.
No Preview Available