This Article 
 Bibliographic References 
 Add to: 
An Algebraic Model for Asynchronous Circuits Verification
July 1988 (vol. 37 no. 7)
pp. 835-847
An algebraic methodology for comparing switch-level circuits with higher-level specifications is presented. Switch-level networks, 'user' behavior, and input constraints are modeled as asynchronous machines. The model is based on the algebraic theory of characteristic functions (CF). An asynchronous automation is represented by a pair of CFs, called a dynamic CF (DCF): the first CF describes th

[1] Barrow, H.G., "Verify: A Program for Proving Correctness of Digital Hardware Designs,"Artificial Intelligence, Vol. 24, 1984, pp. 437-491.
[2] B. Beizer, "Towards a new theory of sequential switching networks,"IEEE Trans. Comput., vol. C-19, pp. 939-956, Oct. 1970.
[3] G. Bochmann, "Hardware specifications with temporal logic: An example,"IEEE Trans. Comput., vol. C-31, no. 3, 1982.
[4] R. E. Bryant, "A switch-level model and simulator for MOS digital systems,"IEEE Trans. Comput., vol. C-33, no. 2, 1984.
[5] R. E. Bryant, "Symbolic verification of MOS circuits," inProc. Chapel Hill Conf. VLSI, 1985.
[6] J. A. Brzozowski and M. Yoeli, "On a ternary model of gate networks,"IEEE Trans. Comput., vol. C-28, no. 3, pp. 178-184, 1979.
[7] E. Cerny, "An approach to unified methodology of combinational switching circuits,"IEEE Trans. Comput., vol. C-26, no. 8, 1977.
[8] E. Cerny, "Controllability and fault observability in modular combinational circuits,"IEEE Trans. Comput., vol. C-27, no. 10, 1978.
[9] E. Cerny, "Characteristic functions in multivalued logic systems,"Digital Processes, vol. 6, pp. 167-174, 1980.
[10] E. Cerny and J. Gecsei, "Simulation of MOS circuits by decision diagrams,"IEEE Trans. Computer-Aided Design, vol. CAD-4, pp. 685-693, Oct. 1985.
[11] D. L. Dill and E. M. Clarke, "Automatic verification of asynchronous circuits using temporal logic," inProc. Chapel Hill Conf. VLSI, 1985.
[12] M. Gordon, "A model of register transfert systems with applications to microcode and VLSI correctness," Comput. Sci. Rep. CSR-82-81, Univ. Edinburgh, 1981.
[13] J. P. Hayes, "A unified switching theory with applications to VLSI design,"Proc. IEEE, vol. 70, no. 10, pp. 1140-1151, 1982.
[14] R. M. Keller, "Towards a theory of universal speed-independent modules,"IEEE Trans. Comput., vol. C-23, no. 1, 1974.
[15] Z. Kohavi,Switching and Finite Automata Theory. New York: McGraw-Hill, 1978.
[16] S. M. Leinwand, "Automatic design verification and test generation for digital systems," Ph.D. dissertation, Weizmann Instit. Sci., Rehovot, 1980.
[17] L. R. Marino, "General theory of metastable operation,"IEEE Trans. Comput., vol. C-30, no. 2, 1981.
[18] C. Mead and L. Conway,Introduction to VLSI Systems. Reading, MA: Addison-Wesley, 1980, pp. 150-152.
[19] R. E. Miller,Switching Theory. New York: Wiley, 1965.
[20] G. J. Milne, "A model for hardware description and verification," inProc. 21st Design Automat. Conf., 1984.
[21] B. Mishra and E. M. Clarke, "Automatic and hierarchical verification of asynchronous circuits using temporal logic," Tech. Rep. CMU-CS- 83-155, Carnegie-Mellon Univ., Pittsburgh, PA, 1983.
[22] B. Moszkowski, "A temporal logic for multilevel reasoning about hardware,"IEEE Computer, no. 2, 1985.
[23] V. Pitchumani and E. P. Stabler, "An inductive assertion method for register transfer level design verification,"IEEE Trans. Comput., vol. C-32, no. 12, 1983.
[24] S. Rudeanu,Boolean Functions and Equations. Amsterdam, The Netherlands: North-Holland, 1974.
[25] R. Shostack, "Formal verification of circuit design," inProc. VI Int. Conf. Hardware Description Languages, IFIP, 1983.
[26] S. Unger,Asynchronous Sequential Switching Circuits, New York: Wiley-Interscience, 1969.
[27] T. J. Wagner, "Hardware verification," Ph.D. dissertation, STAN-CS-77-632, Stanford Univ., 1977.
[28] Wojcik, A.S., "A Formal Design Verification System Based on an Automated Reasoning System,"ACM IEEE 21st Design Automation Conf., July 1984, pp. 641-647.
[29] L. Wos, R. Overbeek, E. Lusk, and J. Boyle,Automated Reasoning: Introduction and Applications. Englewood Cliffs, NJ: Prentice-Hall, 1974.

Index Terms:
machine composition; logic testing; algebraic model; asynchronous circuits verification; switch-level circuits; asynchronous machines; asynchronous automation; Boolean algebra; Boolean inequalities; Boolean functions; logic testing; program verification.
C. Berthet, E. Cerny, "An Algebraic Model for Asynchronous Circuits Verification," IEEE Transactions on Computers, vol. 37, no. 7, pp. 835-847, July 1988, doi:10.1109/12.2229
Usage of this product signifies your acceptance of the Terms of Use.