### 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 language | English |
---|---|

Title of host publication | 1990 IEEE International Conference on Computer-Aided Design. Digest of Technical Papers |

Publisher | Publ by IEEE |

Pages | 38-41 |

Number of pages | 4 |

ISBN (Print) | 0818620552 |

Publication status | Published - Dec 1 1990 |

Event | 1990 IEEE International Conference on Computer-Aided Design - ICCAD-90 - Santa Clara, CA, USA Duration: Nov 11 1990 → Nov 15 1990 |

### Publication series

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

### Other

Other | 1990 IEEE International Conference on Computer-Aided Design - ICCAD-90 |
---|---|

City | Santa Clara, CA, USA |

Period | 11/11/90 → 11/15/90 |

### Fingerprint

### All Science Journal Classification (ASJC) codes

- Engineering(all)

### Cite this

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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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

}

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 -