Formal Verification of Memory Circuits by Switch-Level Simulation
The work
| Authors | Randal E. Bryant |
|---|---|
| Editors | |
| Type | article |
| Year | 1991 |
| Also known as | bryant1991formalc |
| Citekey | bryant1991memory |
Where it appeared
| Published in | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems |
|---|---|
| Volume | 10 |
| Issue | 1 |
| Pages | 94--102 |
Identifiers
| DOI | 10.1109/43.62795 |
|---|
Access
| Landing page | https://www.cs.cmu.edu/~bryant/pubdir/tcad91.pdf |
|---|
Related
| Distinct from | aagaard1999are |
|---|---|
| Distinct from | bryant1987cosmos |
| Distinct from | bryant1990ternary |
| Distinct from | bryant1991complexity |
| Distinct from | bryant1991methodology |
| Distinct from | chen1996verification |
| Distinct from | cohn1988correctness |
| Distinct from | seger1995formal |
| Distinct from | slobodova2011flexible |
| Distinct from | trippel2021fuzzing |
From bibtex.
Abstract
A logic simulator can prove the correctness of a digital circuit if it can be shown that only circuits implementing the system specification will produce a particular response to a sequence of simulation commands. Three-valued modeling, where the third state indicates a signal with unknown digital value, can greatly reduce the number of patterns that need to be simulated for complete verification. As an extreme case, an n-bit random-access memory (RAM) can be verified by simulating just O(n log n) patterns. This approach to verification is fast, requires minimal attention on the part of the user to the circuit details, and can utilize more sophisticated circuit models than other approaches to formal verification. The technique has been applied to a CMOS static RAM design using the COSMOS switch-level simulator. By simulating many patterns in parallel, a massively-parallel computer can verify a 4K RAM in under 6 minutes.
A copy is held
pdf, 145.9 kB. Not published — it may be under copyright. The facts and links here are.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-16 23:03 UTC |
| Approved by | a person 2026-09-23 14:09 UTC |
Filed under
Cite it as
@article{bryant1991memory,
title = {Formal Verification of Memory Circuits by Switch-Level Simulation},
author = {Randal E. Bryant},
year = {1991},
journal = {IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems},
volume = {10},
number = {1},
pages = {94--102},
doi = {10.1109/43.62795},
}
This record lives at https://refs.drheap.org/bryant1991memory/ and will keep
doing so. It used to be called bryant1991formalc, and those addresses still resolve to this one.