Yan Peng

As a Ph.D. student still at school, I would say, it's because it's fun. To solve formal verification problems is like to solve puzzles with well-crafted computer programs. I can still remember the rejoice and excitement when I first found a counter-example that pinpoints a glitch bug from a large circuit module. Only a piece of freshly-made mango mousse cake can compete with that. Other than the fun of it, doing formal methods and formal verification make you think more about programs. You would constantly ask yourself: "Why would I believe this function terminate?", "Why is there no deadlock?", "Why is this algorithm correct?" and etc. You will become a better programmer at the end of the day.

As a practical researcher, I would also tell you that formal verification is largely needed. Traditional testing is not good enough for making sure of the correctness of programs. Often, it suffers from the problem that testing can't be exhaustive. For example, you can't test every number from the real numbers. Even for the discrete space, no one want to test all 2⁶⁴ possible values, right? This is what makes formal methods attractive. Imagine using formal logic to reason about programs themselves, instead of dwelling upon each individual inputs.

Let's see if you can find what is wrong about this piece of code:

;; Replace all sublists that matches old-list in char-list with new-list
(defun replace-sublist (char-list old-list new-list)
  (cond ((endp char-list) nil)
        ((equal (take (len old-list) char-list) old-list)
         (append new-list (replace-sublist (nthcdr (len old-list) char-list) old-list new-list)))
        (t (cons (car char-list) (replace-sublist (cdr char-list) old-list new-list

My first project and my major project.

This is an idea that combines SMT solvers with a theorem prover. The starting point of this combination has nothing to do with an SMT solver, nor a theorem prover. Instead, we were aiming at proving global convergence of a digital Phase-Locked Loop. After a while of researching, we find Z3's arithmetic capabilities super powerful. We developed a mathematical proof. For arithmetic inequalities in the proof, which are not within the computing power of a human brain, we use Z3 for discharging the claims.

However, we are not satisfied with that, because there are still unproven theorems that form the other parts or the structure of this proof. For example, there is an induction proof that is very crucial to the circuit convergence. Unfortunately, the current Z3 does not handle that kind of induction proof. Then, ta-da, we found ACL2.

We combine Z3 as an external procedure for ACL2 and we call our interface Smtlink. With its help, we are able to formulate the other parts of our proof into ACL2 and when ACL2 becomes slow in proving complicated arithmetic formulas, we fire Z3. We also applied the tool to several other problems described below.

A huge amount of work has been done to ensure the soundness of this integration. Check out the code and paper for detail.

Timed asynchronous circuits is like a concurrent system, for which instead of connecting computers, they connect circuit gates. And like concurrent systems, they follow certain hand-shaking protocols in order for signals to transmit in the right way. They have the same properties of being nondeterministic, that is events can happen in different orders. Timing constraints are required for the timed asynchronous circuits to work correctly.

We modelled timed asynchronous circuits using timed traces and proved safety properties of self-timed pipelines with an inductive invariant. We use Smtlink for the proof.

Just like what compilers do, in digital circuit design, a logic synthesis tool is used for compiling high-level RTL behavioural models into gate-level netlist implementations. Even though logic synthesis maintains boolean equivalence, it is still possible to introduce bugs into the netlist implementation even when the RTL behavioural model prohibits such bugs. This is due to the lack of knowledge about timing in logic synthesis.

We use the theorem prover ACL2 and the SAT solver Glucose to help circuit designers identify such bugs and we've got very nice results. This is the first time for me to use formal methods to solve a real-world-scale problem. The process is both challenging and exciting.

Mathematicians working in the optimization aspect of machine learning have been continuously coming up with new optimization algorithms that promotes the efficiency of machine learning tasks. Simple algorithms had already been explored and new algorithms tend to be much more sophisticated as in why they should achieve better performance. A typical proof of convergence rate can expand 10 or more pages with a lot of details being omitted. In another perspective, the researchers have strong belief that they are over-constraining their algorithm parameters. It will be great if their proofs can be made symbolic so that they can easily push the parameters to the limit and see if the proofs will break.

This report is a very prelimitary attempt at automating machine learning proofs to solve above problems.

Automatic differentiation automatically calculates the exact gradient of a function at a specific data point.

For analog circuits verification, it will be very useful if a program can easily calculates the tendency of change of any quantity in the circuit in comparison to another quantity. For example, we can properly model a correctness specification for a circuit in a mathematical function. We can also produce a mathematical model for a circuit. The correctness function will in some sense relate to the circuit model's state variables or even parameters. Thus, by calculating the derivatives, we are able to see the relative relations between those quantities. This information can be used in proving specifications of a circuit, generating new designs and etc.

This prelimitary work attempts at applying automatic differentiation to real circuit designs modelled in MATLAB functions.