Automatic and semi-automatic verification of switch-level circuits with temporal logic and binary decision diagrams

Masahiro Fujita, Yusuke Matsunaga, Taeko Kakuda

Research output: Chapter in Book/Report/Conference proceedingConference contribution

3 Citations (Scopus)

Abstract

Automatic and semi-automatic verification methods for switch-level circuits are presented. Switch-level circuits with no delay (but with/without charge effects) are automatically verified using a formalism with binary decision diagrams (BDD) and temporal logic. Purely bidirectional transistors, such as those whose signal directions are dynamically determined in operations, are treated in the uniform way as nonbidirectional transistors. In the case of switch-level circuits with arbitrary delays, based on the work by M. E. Leeser (1989), the authors present a semi-automatic verification method which uses a propositional theorem prover using BDD. First some assignments of propositional variables to terms of temporal logic are manually given, and then the automatic theorem prover does verification.

Original languageEnglish
Title of host publication1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers
PublisherPubl by IEEE
Pages38-41
Number of pages4
ISBN (Print)0818620552
Publication statusPublished - Dec 1 1990
Externally publishedYes
Event1990 IEEE International Conference on Computer-Aided Design - ICCAD-90 - Santa Clara, CA, USA
Duration: Nov 11 1990Nov 15 1990

Publication series

Name1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers

Other

Other1990 IEEE International Conference on Computer-Aided Design - ICCAD-90
CitySanta Clara, CA, USA
Period11/11/9011/15/90

All Science Journal Classification (ASJC) codes

  • Engineering(all)

Fingerprint Dive into the research topics of 'Automatic and semi-automatic verification of switch-level circuits with temporal logic and binary decision diagrams'. Together they form a unique fingerprint.

  • Cite this

    Fujita, M., Matsunaga, Y., & Kakuda, T. (1990). Automatic and semi-automatic verification of switch-level circuits with temporal logic and binary decision diagrams. In 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers (pp. 38-41). (1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers). Publ by IEEE.