Extending ACL2 with SMT Solvers

TL;DR

This paper introduces Smtlink, a new clause processor that integrates SMT solvers into ACL2, enhancing verification capabilities for physical systems by combining ACL2's inductive reasoning with SMT's domain support.

Contribution

The paper presents Smtlink, a novel extension of ACL2 that enables the use of SMT solvers, addressing integration challenges and expanding verification methods for complex systems.

Findings

Successfully integrated SMT solvers into ACL2 using Smtlink.

Enhanced verification of physical systems, including AMS designs.

Identified key design and implementation considerations for SMT integration.

Abstract

We present our extension of ACL2 with Satisfiability Modulo Theories (SMT) solvers using ACL2's trusted clause processor mechanism. We are particularly interested in the verification of physical systems including Analog and Mixed-Signal (AMS) designs. ACL2 offers strong induction abilities for reasoning about sequences and SMT complements deduction methods like ACL2 with fast nonlinear arithmetic solving procedures. While SAT solvers have been integrated into ACL2 in previous work, SMT methods raise new issues because of their support for a broader range of domains including real numbers and uninterpreted functions. This paper presents Smtlink, our clause processor for integrating SMT solvers into ACL2. We describe key design and implementation issues and describe our experience with its use.