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. (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)

The full text of this publication is not available from this repository. (Contact us about this Publication)
Official URL


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
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: Faculties > Science Technology and Medical Studies > School of Computing
Depositing User: O.O. Odanye
Date Deposited: 30 Apr 2009 23:51
Last Modified: 18 Jul 2012 08:30
Resource URI: (The current URI for this page, for reference purposes)
  • Depositors only (login required):