Skip to main content

Reasoning about analog-level implementations of digital systems

Hanna, Keith (2000) Reasoning about analog-level implementations of digital systems. Formal Methods in System Design, 16 (2). pp. 127-158. ISSN 0925-9856. (doi:10.1023/A:1008791128550) (The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided) (KAR id:16185)

The full text of this publication is not currently available from this repository. You may be able to access a copy if URLs are provided.
Official URL:
http://dx.doi.org/10.1023/A:1008791128550

Abstract

An approach is described for specifying and reasoning about implementations of digital systems that are described at the analog level of abstraction. It is an extension of existing methods that use higher-order logic for reasoning about implementations described in terms of ideal components at the digital level of abstraction. The behaviour of analog components (transistors, etc) are conservatively specified by predicates on the analog voltages and currents at their terminals. A syntactically defined class of specifications is identified that has been found both to be adequately expressive and also to possess computationally tractable decision procedures. The overall approach is illustrated by deriving the conditions for correctness and for compositionality of TTL implementations of logic gates.

Item Type: Article
DOI/Identification number: 10.1023/A:1008791128550
Uncontrolled keywords: specification; reasoning; analog; gates; transistors; TTL; higher-order logic
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 75 Electronic computers. Computer science
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Depositing User: O.O. Odanye
Date Deposited: 30 Apr 2009 23:51 UTC
Last Modified: 16 Nov 2021 09:54 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/16185 (The current URI for this page, for reference purposes)

University of Kent Author Information

Hanna, Keith.

Creator's ORCID:
CReDIT Contributor Roles:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.