Biblio
Filters: Keyword is arbitrated merge [Clear All Filters]
.
2019. A Hierarchical Approach to Self-Timed Circuit Verification. 2019 25th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC). :105–113.
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.