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
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

Fingerprint

Binary decision diagrams
Temporal logic
Switches
Networks (circuits)
Transistors

All Science Journal Classification (ASJC) codes

  • Engineering(all)

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.

Automatic and semi-automatic verification of switch-level circuits with temporal logic and binary decision diagrams. / Fujita, Masahiro; Matsunaga, Yusuke; Kakuda, Taeko.

1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers. Publ by IEEE, 1990. p. 38-41 (1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers).

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

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. 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers, Publ by IEEE, pp. 38-41, 1990 IEEE International Conference on Computer-Aided Design - ICCAD-90, Santa Clara, CA, USA, 11/11/90.
Fujita M, Matsunaga Y, Kakuda T. 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. Publ by IEEE. 1990. p. 38-41. (1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers).
Fujita, Masahiro ; Matsunaga, Yusuke ; Kakuda, Taeko. / Automatic and semi-automatic verification of switch-level circuits with temporal logic and binary decision diagrams. 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers. Publ by IEEE, 1990. pp. 38-41 (1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers).
@inproceedings{96f2ba93f4f04596bbea98dba44f5b28,
title = "Automatic and semi-automatic verification of switch-level circuits with temporal logic and binary decision diagrams",
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.",
author = "Masahiro Fujita and Yusuke Matsunaga and Taeko Kakuda",
year = "1990",
month = "12",
day = "1",
language = "English",
isbn = "0818620552",
series = "1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers",
publisher = "Publ by IEEE",
pages = "38--41",
booktitle = "1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers",

}

TY - GEN

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

AU - Fujita, Masahiro

AU - Matsunaga, Yusuke

AU - Kakuda, Taeko

PY - 1990/12/1

Y1 - 1990/12/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0025556063&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0025556063&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:0025556063

SN - 0818620552

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

SP - 38

EP - 41

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

PB - Publ by IEEE

ER -