Automatic verification of sequential circuit designs
The work
| Authors | E. M. Clarke; Jerry R. Burch; Orna Grümberg; David E. Long; Kenneth L. McMillan |
|---|---|
| Editors | |
| Type | article |
| Year | 1992 |
| Citekey | clarke1992automatic |
Where it appeared
| Published in | Philosophical Transactions of the Royal Society of London Series A Physical and Engineering Sciences |
|---|---|
| Publisher | Royal Society |
| Volume | 339 |
| Issue | 1652 |
| Pages | 105--120 |
Identifiers
| DOI | 10.1098/rsta.1992.0028 |
|---|---|
| OpenAlex | W2012211183 |
Access
| Landing page | https://doi.org/10.1098/rsta.1992.0028 |
|---|
From OpenAlex, which stores abstracts as an index of words and their positions: what is shown is rebuilt from that, and reads fluently whether or not it is what the author wrote.
Abstract
Abstract Temporal logic model checking is a method for automatically deciding if a sequential circuit satisfies its specifications. In this approach, the circuit is modelled as a state transition system, and specifications are given by temporal logic formulas. Efficient search algorithms are used to determine if the specifications are satisfied or not. The procedure has been used successfully in the past to find subtle errors in a number of non trivial circuit designs. Recently, the size of the circuits that can be handled by this technique has increased dramatically. It is now possible to verify transition systems that are many orders of magnitude larger than was previously the case. In this paper, we describe some of the techniques that have made this increase possible. These techniques are based on the use of binary decision diagrams to represent transition systems and sets of states.
How it got here
| How it got here | agent via openalex |
|---|---|
| Added | 2026-10-26 02:15 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@article{clarke1992automatic,
title = {Automatic verification of sequential circuit designs},
author = {E. M. Clarke and Jerry R. Burch and Orna Grümberg and David E. Long and Kenneth L. McMillan},
year = {1992},
journal = {Philosophical Transactions of the Royal Society of London Series A Physical and Engineering Sciences},
publisher = {Royal Society},
volume = {339},
number = {1652},
pages = {105--120},
doi = {10.1098/rsta.1992.0028},
}
This record lives at https://refs.drheap.org/clarke1992automatic/ and will keep doing so.