Abstract:
Formal verification has become a well-established part of standard hardware design flows leveraging SAT solvers and model checkers for verification tasks including logical equivalence checking, property checking, and protocol verification. These tools are largely based on all-digital, synchronous, single clock-domain models of hardware behaviour. To address the needs of system-on-chip and multi-core designs, we are developing verification methods for asynchronous, analog, mixed-signal, and mixed-timing circuits.
A key enabling technology for our research is the integration of an SMT solver, Z3, into an interactive theorem prover, ACL2. Our integration, Smtlink, exploits ACL2’s extensive support for reflection: we can write lisp functions that operate on the syntax of pending goals by extracting facts (e.g. function definitions and previously proven theorems) from the ACL2 logical world. Smtlink can automatically translate high-level goals that include user-defined data types and recursive functions into formulas that are in the logic of the SMT solver. We demonstrate the efficacy of this approach with the verification of timed asynchronous handshake circuits and a convergence proof for a digital phase-locked loop.
I will briefly describe related verification work including using automatic differentiation (AD) based algorithms to reason about synchronizers and analog circuits, and interval-arithmetic based verification algorithms to reason about convergence properties of non-linear circuits. Currently, I am working with students and other faculty at UBC to explore verification challenges arising in operating system research, cyber-physical systems, and numerical optimization algorithms used for machine learning.
I gratefully acknowledge my collaborators including Chris Chen, Ian Jones, Matt Kaufmann, Carl Kwan, Yan Peng, Justin Reiher, Mark Schmidt, and Margo Seltzer.
Bio:
Mark Greenstreet is a professor in the Department of Computer Science at the University of British Columbia. He earned his B.Sc. (1981) from Caltech, and his MA (1988) and Ph.D. (1992) from Princeton. His research interests span a wide range of formal verification topics, especially any problem, hardware or software, that involves concurrency and/or continuous models. Mark has industrial chip design experience spanning from a design of an FFT chip set for ESL (at TRW subsidiary) in the early 1980’s to work on verifying the synchronizers and clock-domain-crossing circuits in many generations of SPARC CPUs.