Formal Verification of C-element Circuits
The work
| Authors | Chao Yan; Laurent Fesquet; Florent Ouchet; Katell Morin-Allory |
|---|---|
| Editors | |
| Type | inproceedings |
| Year | 2011 |
| Citekey | yan2011formal |
Where it appeared
| Published in | IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2011) |
|---|---|
| Pages | 55--64 |
Identifiers
| DOI | 10.1109/async.2011.14 |
|---|
Access
| Landing page | https://hal.science/hal-00624249 |
|---|
Empty on purpose
| copy |
Related
| Distinct from | marino1981general |
|---|---|
| Distinct from | martin1990limitations |
From bibtex.
Abstract
It is well known that the correct behavior of asynchronous circuits is not guaranteed when the inputs switch too slowly. The erroneous behavior is generally difficult to be spotted by simulation based methods. We applied formal methods to study the analog switching behavior of a full-buffer circuit composed of C-elements. We used our reachability analysis tool COHO to compute all reachable states of two C-element designs and verified several analog properties. Based on these properties, we identified a sufficient condition under which the full-buffer circuit always supports the designed handshaking protocol. We also improved the COHO tool to automate the verification process, reduce error and improve performance.
How it got here
| How it got here | agent via bibtex |
|---|---|
| Added | 2026-09-17 10:06 UTC |
| Not denied by | a person 2026-10-29 17:12 UTC |
Filed under
Cite it as
@inproceedings{yan2011formal,
title = {Formal Verification of C-element Circuits},
author = {Chao Yan and Laurent Fesquet and Florent Ouchet and Katell Morin-Allory},
year = {2011},
booktitle = {IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC 2011)},
pages = {55--64},
doi = {10.1109/async.2011.14},
}
This record lives at https://refs.drheap.org/yan2011formal/ and will keep doing so.