| Title | A Hierarchical Approach to Self-Timed Circuit Verification |
| Publication Type | Conference Paper |
| Year of Publication | 2019 |
| Authors | Chau, Cuong, Hunt, Warren A., Kaufmann, Matt, Roncken, Marly, Sutherland, Ivan |
| Conference Name | 2019 25th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC) |
| Keywords | ACL2 theorem prover, arbitrated merge, asynchronous circuit modeling, asynchronous circuit verification, combinational circuits, compositionality, Computational modeling, Flip-flops, greatest common divisor, greatest common divisor circuit model, hardware description language, hardware description languages, hierarchical verification, Integrated circuit modeling, Iterative methods, iterative self-timed circuits, Latches, link joint model, link-joint style, Logic gates, mechanical theorem proving, non deterministic behavior, Predictive Metrics, pubcrawl, Resiliency, Scalability, scalable verification, self-timed circuit verification, theorem proving, Timing, timing circuits, Wires |
| Abstract | Self-timed circuits can be modeled in a link-joint style using a formally defined hardware description language. It has previously been shown how functional properties of these models can be formally verified with the ACL2 theorem prover using a scalable, hierarchical method. Here we extend that method to parameterized circuit families that may have loops and non-deterministic outputs. We illustrate this extension with iterative self-timed circuits that calculate the greatest common divisor of two natural numbers, with circuits that perform arbitrated merges non-deterministically, and with circuits that combine both of these. |
| DOI | 10.1109/ASYNC.2019.00022 |
| Citation Key | chau_hierarchical_2019 |
A Hierarchical Approach to Self-Timed Circuit Verification