caa a22 4500 47579754X CHVBK 20180406123728.0 cr unu---uuuuu 170329e20000301xx s 000 0 eng 10.1023/A:1008791128550 doi (NATIONALLICENCE)springer-10.1023/A:1008791128550 Hanna Keith Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK aut Reasoning About Analog-Level Implementations of Digital Systems [Elektronische Daten] [Keith Hanna] 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. Kluwer Academic Publishers, 2000 specification nationallicence reasoning nationallicence analog nationallicence gates nationallicence transistors nationallicence TTL nationallicence higher-order logic nationallicence Formal Methods in System Design Kluwer Academic Publishers 16/2(2000-03-01), 127-158 0925-9856 16:2<127 2000 16 10703 https://doi.org/10.1023/A:1008791128550 text/html Onlinezugriff via DOI 1 research-article jats NATIONALLICENCE 856 40 https://doi.org/10.1023/A:1008791128550 text/html Onlinezugriff via DOI NATIONALLICENCE 100 1- Hanna Keith Computing Laboratory, University of Kent, CT2 7NF, Canterbury, Kent, UK aut NATIONALLICENCE 773 0- Formal Methods in System Design Kluwer Academic Publishers 16/2(2000-03-01), 127-158 0925-9856 16:2<127 2000 16 10703 Metadata rights reserved Springer special CC-BY-NC licence nationallicence BK010053 XK010053 XK010000 NATIONALLICENCE NATIONALLICENCE NL-springer