A Hierarchical Approach to Self-Timed Circuit Verification
Published In
2019 25th IEEE International Symposium on Asynchronous Circuits and Systems (ASYNC)
Document Type
Citation
Publication Date
5-1-2019
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.
Locate the Document
DOI
10.1109/ASYNC.2019.00022
Persistent Identifier
https://archives.pdx.edu/ds/psu/34760
Publisher
IEEE
Citation Details
Chau, C., Hunt, W. A., Kaufmann, M., Roncken, M., & Sutherland, I. (2019). A Hierarchical Approach to Self-Timed Circuit Verification. Institute of Electrical and Electronics Engineers (IEEE). https://doi.org/10.1109/async.2019.00022