Visible to the public Biblio

Filters: Author is Sutherland, Ivan  [Clear All Filters]
2020-03-16
Chau, Cuong, Hunt, Warren A., Kaufmann, Matt, Roncken, Marly, Sutherland, Ivan.  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.