This Article 
 Bibliographic References 
 Add to: 
Functional Description of Connector-Switch-Attenuator Networks
January 1988 (vol. 37 no. 1)
pp. 111-114
The switch-level abstraction of digital MOS circuits has been used primarily in simulators. In formal verification, a functional description must be first extracted from the switch network. It is shown here how the theory of characteristic functions can be applied to analyze such networks and to extract their functional description.

[1] J. P. Hayes, "A unified switching theory with applications to VLSI design,"Proc. IEEE, vol. 70, pp. 1140-1151, Oct. 1982.
[2] E. Cerny and M. A. Marin, "An approach to unified methodology of combinational switching circuits,"IEEE Trans. Comput., vol. C-26, pp. 745-756, Aug. 1977.
[3] E. Cerny, "Controllability and fault observability in modular combinational circuits,"IEEE Trans. Comput., vol. C-27, pp. 896-903, Oct. 1978.
[4] E. Cerny, "Unique and identity solutions of Boolean equations,"Digital Processes, vol. 3, pp. 331-337, Fall 1977.
[5] E. Cerny, "Characteristic functions in multivalued logic systems,"Digital Processes, vol. 6, pp. 167-174, 1980.
[6] E. Cerny, D. Mange, and E. Sanchez, "Synthesis of minimal binary decision trees,"IEEE Trans. Comput., vol. C-28, pp. 472-482, July 1979.
[7] 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.
[8] R. E. Bryant, "An algorithm for MOS logic simulation,"LAMBDA/ VLSI J., vol. 1, pp. 46-53, Fourth Quarter 1980.
[9] R. E. Bryant, "A switch-level model and simulator for MOS digital systems,"IEEE Trans. Comput., vol. C-33, pp. 160-177, Feb. 1984.
[10] R. E. Bryant, "Symbolic verification of MOS circuits," inProc. Chapel Hill Conf. VLSI, 1985.
[11] M. Gordon, "Proving a computer correct with LCF-LSM hardware verification system," Computer Lab. Tech. Rep. 42, Cambridge University, 1983.
[12] D. L. Dill and E. M. Clarke, "Automatic verification of asynchronous circuits using temporal logic," inProc. Chapel Hill Conf. VLSI, 1985.
[13] C. Berthet and E. Cerny, "Input-constrained memory elements in speed-independent circuits," inProc. Canadian Conf. VLSI (CCVLSI '86), Oct. 27-28, 1986.
[14] C. Berthet and E. Cerny, "An algebraic model for asynchronous circuits verification," Publi. 571, Département d'informatique et de recherche opérationnelle, Universitéde Montréal,IEEE Trans. Comput., to be published.
[15] D. L. Dietmeyer,Logic Design of Digital Systems. Boston, MA: Allyn and Bacon, 1979.
[16] S. Rudeanu,Boolean Functions and Equations. Amsterdam, The Netherlands, North-Holland, 1974.

Index Terms:
connector-switch-attenuator networks; switch-level abstraction; digital MOS circuits; formal verification; functional description; characteristic functions; electron device testing; failure analysis; field effect integrated circuits; logic testing; switching networks.
E. Cerny, J. Gecesi, "Functional Description of Connector-Switch-Attenuator Networks," IEEE Transactions on Computers, vol. 37, no. 1, pp. 111-114, Jan. 1988, doi:10.1109/12.75142
Usage of this product signifies your acceptance of the Terms of Use.