This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Equivalence of the Arbiter, the Synchronizer, the Latch, and the Inertial Delay
July 1983 (vol. 32 no. 7)
pp. 603-614
J.C. Barros, Development Company
An axiomatic method for proving correctness properties about digital circuit implementations under the influence of asynchronous inputs is presented. This method, termed hardware correctness, is used to prove properties about a target digital circuit that is implemented in terms of constituent digital circuits. The proof consists of deducing theorems about properties of the target circuit from known properties of the constituent circuits. Three types of properties are considered, and they are expressed as axioms in first order predicate calculus. The axioms describe ideal behavior of the four most commonly studied asynchronous circuits, the inertial delay, the synchronizer, the time-bounded arbiter, and the latch. These axioms are derived from the less precise behavioral descriptions used by other investigators.
Index Terms:
ternary algebra, Arbiter, axiomatic model, inertial delay, latch, sequential circuit, synchronizer
Citation:
J.C. Barros, B.W. Johnson, "Equivalence of the Arbiter, the Synchronizer, the Latch, and the Inertial Delay," IEEE Transactions on Computers, vol. 32, no. 7, pp. 603-614, July 1983, doi:10.1109/TC.1983.1676292
Usage of this product signifies your acceptance of the Terms of Use.