Verifying Timed, Asynchronous Circuits using ACL2
Yan Peng, Mark R. Greenstreet · 2019
This paper presents a novel approach to verifying timed, asynchronous circuits. We model a circuit as a trace-recognizer: a trace is a sequence of states where a state is a mapping from hierarchical signal names to values and transition times. This approach naturally models non-determinism and continuous quantities such as time. ACL2 supports the use of rich data types and highly expressive functions in the model, and induction in the proofs which enables parameterized verification. Much of the detailed reasoning is automated by using an integrated SMT solver. We prove properties of self-timed pipelines with timing constraints.