UBC Theses and Dissertations

UBC Theses Logo

UBC Theses and Dissertations

Combining SMT with theorem proving for AMS verification : analytically verifying global convergence of a digital PLL Peng, Yan


Ubiquitous computer technology is driving increasing integration of digital computing with continuous, physical systems. Examples range from the wireless technology, cameras, motion sensors, and audio IO of mobile devices to sensors and actuators for robots to the analog circuits that regulate the clocks, power supplies, and temperature of CPU chips. While combining analog and digital brings ever increasing functionality, it also creates a design verification challenge: the modeling frameworks for analog and digital design are often quite different, and comprehensive simulations are often impractical. This motivates the use of formal verification: constructing mathematically rigorous proofs that the design has critical properties. To support such verification, I integrated the Z3 “satisfiability modulo theories” (SMT) solver into the ACL2 theorem prover. The capabilities of these two tools are largely complementary – Z3 provides fully automated reasoning about boolean formulas, linear and non-linear systems of equalities, and simple data structures such as arrays. ACL2 provides a very flexible framework for induction along with proof structuring facilities to combine simpler results into larger theorems. While both ACL2 and Z3 have been successfully used for large projects, my work is the first to bring them together. I demonstrate this approach by verifying properties of a clock-generation circuit (called a Phase-Locked Loop or PLL) that is commonly used in CPUs and wireless communication.

Item Media

Item Citations and Data


Attribution-NonCommercial-NoDerivs 2.5 Canada