Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation
The work
| Authors | Randal E. Bryant; Derek L. Beatty; Carl-Johan H. Seger |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 1991 |
| Citekey | bryant1991formal |
Where it appeared
| Published in | Proceedings of the 28th ACM/IEEE Design Automation Conference (DAC '91) |
|---|---|
| Pages | 397--402 |
Identifiers
| DOI | 10.1145/127601.127701 |
|---|
Access
| Landing page | https://www.cs.cmu.edu/~bryant/pubdir/dac91a.pdf |
|---|
Related
| Distinct from | bryant1981switchlevel |
|---|---|
| Distinct from | bryant1987cosmos |
| Distinct from | bryant1990ternary |
| Distinct from | bryant1991memory |
| Distinct from | oleary1999formally |
| Distinct from | seger1995formal |
From bibtex.
Abstract
Symbolic trajectory evaluation is a new approach to formal hardware verification combining the circuit modeling capabilities of symbolic logic simulation with some of the analytic methods found in temporal logic model checkers. We have created such an evaluator by extending the symbolic switch-level simulator COSMOS. This program gains added efficiency by exploiting the ability of COSMOS to evaluate circuit operation over a ternary logic model, where the third value X represents an unknown logic value. This program can formally verify systems containing complex features such as switch-level models, detailed timing, and pipelining.
Cite it as
@inproceedings{bryant1991formal,
title = {Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation},
author = {Randal E. Bryant and Derek L. Beatty and Carl-Johan H. Seger},
year = {1991},
booktitle = {Proceedings of the 28th ACM/IEEE Design Automation Conference (DAC '91)},
pages = {397--402},
doi = {10.1145/127601.127701},
}
This record lives at https://refs.drheap.org/bryant1991formal/ and will keep doing so.