### Abstract

An automatic verification system for sequential circuits is described in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, the system does not require user assistance and is quite fast; experimental results show that state machines with several hundred states can be checked for correctness in a matter of seconds. The verification system uses a simple and efficient algorithm, called a model checker. The algorithm works in two steps: in the first step, it builds a labeled state-transition graph; in the second step, it determines the truth of a temporal formula with respect to the state-transition graph. Two different techniques that have been implemented for automatically generating the state-transition graphs are discussed.

Original language | English (US) |
---|---|

Pages (from-to) | 1035-1044 |

Number of pages | 10 |

Journal | IEEE Transactions on Computers |

Volume | C-35 |

Issue number | 12 |

State | Published - Dec 1986 |

### Fingerprint

### ASJC Scopus subject areas

- Hardware and Architecture
- Electrical and Electronic Engineering

### Cite this

*IEEE Transactions on Computers*,

*C-35*(12), 1035-1044.

**Automatic verification of sequential circuits using temporal logic.** / Browne, Michael C.; Clarke, Edmund M.; Dill, David L.; Mishra, Bhubaneswar.

Research output: Contribution to journal › Article

*IEEE Transactions on Computers*, vol. C-35, no. 12, pp. 1035-1044.

}

TY - JOUR

T1 - Automatic verification of sequential circuits using temporal logic

AU - Browne, Michael C.

AU - Clarke, Edmund M.

AU - Dill, David L.

AU - Mishra, Bhubaneswar

PY - 1986/12

Y1 - 1986/12

N2 - An automatic verification system for sequential circuits is described in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, the system does not require user assistance and is quite fast; experimental results show that state machines with several hundred states can be checked for correctness in a matter of seconds. The verification system uses a simple and efficient algorithm, called a model checker. The algorithm works in two steps: in the first step, it builds a labeled state-transition graph; in the second step, it determines the truth of a temporal formula with respect to the state-transition graph. Two different techniques that have been implemented for automatically generating the state-transition graphs are discussed.

AB - An automatic verification system for sequential circuits is described in which specifications are expressed in a propositional temporal logic. In contrast to most other mechanical verification systems, the system does not require user assistance and is quite fast; experimental results show that state machines with several hundred states can be checked for correctness in a matter of seconds. The verification system uses a simple and efficient algorithm, called a model checker. The algorithm works in two steps: in the first step, it builds a labeled state-transition graph; in the second step, it determines the truth of a temporal formula with respect to the state-transition graph. Two different techniques that have been implemented for automatically generating the state-transition graphs are discussed.

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

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

M3 - Article

AN - SCOPUS:0022890039

VL - C-35

SP - 1035

EP - 1044

JO - IEEE Transactions on Computers

JF - IEEE Transactions on Computers

SN - 0018-9340

IS - 12

ER -