Title

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.

DOI

10.1109/ASYNC.2019.00022

Persistent Identifier

8850663

Publisher

IEEE

Share

COinS