Combining ACL2 and a /spl nu/-calculus model-checker to verify system-level designs

The purpose of this paper is the formal verification of temporal properties of system-level descriptions that include both a control part, which corresponds to a finite set of symbolic states, and a data path with numeric variables. Keeping these variables under their numeric form, without assuming any encoding, induces an infinite state space. We propose a combination of a model-checker for the modal /spl nu/-calculus with the theorem prover ACL2. Due to the induction mechanism of ACL2, this approach allows to consider the infinite state space without having to appeal to reduction techniques. Two simple but significant examples illustrate our results.