My first experience with Formal Methods
Clifford Wolf has written a nice tool, yosyssmtbmc
, based upon his
yosys synthesys tool, that allows you to apply
formal methods
to your Verilog code. The promise of
formal methods
is that you can then mathematically prove that your code works, or if not
then the formal solver should be able to tell you where your code is failing.
I’ve only been working with these methods for a week or so, but already there are some things I can share.
The first project I tried applying these formal methods to was a simple SPIbased A/D converter. This particular controller is designed to interact with a Digilent product containing a MEMs based microphone. I’ve had the project built for some time, although I’ll admit I’ve never actually done anything more with it than plug it in.
Since the project is simple enough, I thought I’d try applying formal methods to it, to prove that my controller worked. Sure, I had a test bench that I had built some time earlier to convince me that the project worked. The design worked well against this test bench, so I didn’t expect to find many problems using formal methods.
Imagine my surprise when I found several bugs instead. Not only that, many of those bugs were within my FIFO implementation–something that I’d passed from one project to another for some time. You see, when I built my FIFO I only tested it in a fashion such as a “reasonable” person might use it. Under this “reasonable use” scenario, the FIFO had done well.
The formal prover, however, didn’t limit itself to what I considered “reasonable” usage of the FIFO. It created underruns and overruns, wrote to the FIFO when it was full, and read from the FIFO when it was empty. It even wrote and read from the empty FIFO on the same clock, and it wrote and read from the full FIFO on the same clock as well. When the internal logic didn’t “match” the criteria I gave the solver, it then showed me where my FIFO code didn’t properly handle these conditions.
I guess I just didn’t have that much creativity when I created my test bench in the first place.
Was the result worth it? Keep in mind, I’ve never used these methods before. So did I think it was worth it? I think so. I haven’t “proved” all of my projects yet, nor do I know if I will be able to, but I have added proofs to some of them—and found bugs as a result.
Today, though, I’d like to share some of what I have learned.
State Sets
If you’ve never worked with formal methods before, the basic concept is that you will go through your code and declare which states are valid and which are not. You’ll then use a theorem prover to mathematically prove that you can never enter an invalid state from a valid one. If the prover cannot prove this, then typically you will have either a bug in your code, or a bug in your formal assertions.
You can think of the “state” as the values in all of your flipflops, together with the values of all of your inputs.
The first step in yosyssmtbmc based theorem solving is the bounded model checker (BMC), figuratively shown in Fig 1. This part of the theorem solver starts your design in its initial state, and then walks through all of the state transitions that it can, stepping your logic forward from one time step to the next, just to see if any set of conditions will drive your model to an invalid state.
This may be the most straightforward part of using yosyssmtbmc, and the easiest to understand. The problem with the BMC step is that your time is limited. Therefore, you will only want to allow the BMC step to check some finite number of transitions. This number needs to be chosen carefully, otherwise there may be states you might eventually get into over time that it won’t find.
You can also find these additional states via the second step: the induction step.
The induction step is just like the mathematical
induction you learned in
Precalculus. You
first prove that some property is true for the first value,
n=1
. This was the purpose of the BMC step above. If it is true for this
base case, you then proceed with the inductive step. This step assumes that
your logic is within some initially valid state, say state n
, and it then
tries to prove that your logic will only transition to a valid state,
say state n+1
.
That’s the idea.
In practice, I’ve struggled with this induction step. The challenge to the designer with the induction step is that you have to declare every unreachable state as invalid, or it might start processing from an unreachable state you aren’t expecting. As figure 2 shows, states that are neither valid nor invalid, but still states that the design will never reach, may easily become starting states for induction. It is therefore up to the designer to clearly indicate that all states must be either valid or invalid.
Let me try to explain this a touch better. In a moment we’ll go over some System Verilog statements that yosys will recognize. These statements declare only the state that you cannot get to. They do this by either reducing the size of the total state space examined, or by declaring particular states to be illegal. That part is the job of the formal specification designer. The job of the formal method is to determine which states may be reached, and to then cross check these states against the illegal ones.
Perhaps a simple table, such as the one in Fig 4, might help to explain this.
What you want to know, as a designer, is whether or not there is any way that you might reach an invalid state from a valid one. Hence, you want to know if a particular illegal state is reachable from a valid state. This is the purpose of formal methods.
The part I struggled with while working through the induction step is that any state that isn’t declared to be invalid might be a starting point for induction–even if the state is unreachable.
This should help give you an idea, should you try working with formal methods yourself, that you need to make certain that unreachable states are either declared to be invalid or removed from the set of possible states.
Speaking of, that’s our next step: discussing how to declare states to be invalid when using yosys.
Formal Declarations
yosys
can be made to understand some basic formal statements, drawn from a
subset of the System Verilog formal verification language. This can be
frustrating for a new user of
formal methods with
yosys,
since most of the material on line discusses the full System Verilog formal
description language subset. What yosys
supports is much less than that. Basically,
yosys supports assert()
, assume()
,
restrict()
, and some expressions about transitions. Let’s examine those
formal verification statements here.
The first statement of interest is the assert()
statement. At first blush,
this statement works very much like the assert()
statement within C/C++.
The value given to the assert()
statement must be true, or you your design
isn’t working as desired. assert()
s do more than that, though.
assert()
s declare states that are invalid within your design.
We’ll come back to that thought in a moment.
The other thing you need to know about assert()
s is that within a simulation,
if the assert()
is ever not true, the simulation will halt on a failure.
This allows you focus on what caused the problem within your design.
The next basic statement is the assume()
statement. This statement is like
the assert()
, but with the exception that the theorem prover doesn’t try to
prove that the assume()
statement is true. Instead, it forces the assume()
to be true. Any logic path that would cause the assume()
to be false
is quietly culled. From the perspective of the state space that will be
examined, the assume()
statement removes particular states from the
realm of possibilities.
For example,
will force the i_clk
input to the design to toggle with every
simulation step (that’s the meaning of the $global_clock
–it’s true on
every change of the time step). States and state transitions where the
clock doesn’t toggle are just quietly removed from the realm of possibility.
assume()
statements have one more feature: if during a simulation the
condition is invalid, the simulation will halt with an error just as it would
if the assert()
statement were false.
The restrict()
instruction is similar to the assume()
instruction.
Like assume()
, restrict()
also reduces the size of the state space that
the theorem prover needs to work within. In that way, a restrict
statement
is much like an assume()
statement.
However, unlike the assume()
statement, the simulator will ignore any
restrict()
statements within your code.
I’ve also found several functions to be very valuable: $past()
,
$stable()
, $rose()
, and $fell()
. Since these are important,
let’s work our way through them.
The $past()
function has the form of $past(expression, N)
, for arbitrary
expressions, and positive integers, N
. This statement returns the value
of the expression N
clocks ago. Hence, $past(expression,1)
references what
the expression evaluated to during the last clock. The number of clocks
parameter, N
, defaults to one, so $past(expression)
is just the same as
$past(expression,1)
.
System Verilog allows two more arguments to the $past()
function for a total
of four. Not so with yosys, however you
may not find these extra arguments necessary either. For example, the fourth
System Verilog argument to the $past()
function specifies what clock and
clock edge you are referencing the $past()
expression from. Instead,
yosys
only allows expressions of $past()
values within a clocked
always block, and so it uses the clock specified in the always statement to
define the clock the $past()
function is relative to.
There is one other trick with the $past()
function: prior to the first
clock, the $past value is undefined and often assumed to be zero by many
formal theorem solvers. You’ll need to be careful, therefore, not to expect
the $past value to reference any initial
value within your logic.
For this reason, I’ve gotten in the habit of creating a signal to tell me if the past value is valid, such as:
I can then use f_past_valid
as part of an expression to determine whether or
not the inputs to a wishbone
slave will not
change once the strobe goes high until the stall line is low. Remember how
we discussed
that with wishbone nothing happens
until (i_wb_stb)&&(!o_wb_stall)
? This means that once the
wishbone master
asserts the strobe signal, i_wb_stb
, that it is likely to wait for the
o_wb_stall
signal to lower before changing the bus request details.
To capture this thought, we’ll assume that once i_wb_stb
goes high, none of the bus request information will change until the
clock after o_wb_stall
goes low:
Alternatively, instead of assuming that the current value was equal to the
last value, we could have instead assumed that these values were $stable()
for the same effect:
The last of the basic commands you’ll want to know is the $rose()
command.
This command returns true or false depending on whether the signal given to
it has risen (positive edge) over the last clock period or not.
This particular function is very useful for telling the theorem prover that your inputs are only going to change on the positive edge of the clock,
A similar $fell()
primitive exists as well for testing negative clock edges.
yosys provides one more helpful feature.
Anytime you use
yosys
to generate a formal description of your code,
yosys defines the FORMAL
flag. Hence, you
can surround your formal properties with ifdef
s, as in:
These, therefore, are your basic formal declaration statements:
assert()
, assume()
, and restrict()
. They are helped by the functions
$stable()
, $past()
, $rose()
, $fell()
, and perhaps some others that I
haven’t learned yet. (Remember, this is only my first week.) assert()
declares statements to be illegal, and assume()
and restrict()
are used
to limit the size of the state space.
With these basic principles, let’s look at some formal theorem proving concepts.
Basic concept
The basic approach to formally describing your program is to assume()
that
the inputs will be valid, and then to assert()
that the outputs are valid.
You may also wish along the way to assert()
particular internal states
are valid as well.
This works until you aggregate up one level, so that you have a higher level
module instantiating a lower level one. In that case, you want to assert()
the values that will be passed to the lower level module rather than
assume()
ing them.
A FIFO example
Let’s work our way through a simple example–that of a FIFO. In this case, we’ll examine the FIFO I just worked with for my SPIbased microphone ADC core.
As you may remember from our last
FIFO discussion, a
FIFO depends upon two
memory pointers: the write pointer, r_first
, and the read pointer, r_last
.
The only time r_first
and r_last
are equal is when the
FIFO is empty.
Likewise, the number of items within the
FIFO is
determined by r_first
minus r_last
.
There are some other rules associated with these two variables. The first is that we cannot be allowed to read from the FIFO any time it is empty. The second rule is that we cannot write to the FIFO when it is full, unless we are also reading from the FIFO at the same time. Any attempt to read from an empty FIFO, or write to a full FIFO should generate an error.
In order to keep the state transitions from being dependent upon the
number of items in the
FIFO, I precompute two values:
will_overflow
, which is true if the next write will overflow the
FIFO, and
will_underflow
, which will be true if the next read will read from an
empty FIFO.
Further, this particular FIFO also returns a status value indicating 1) how many items are in the FIFO, 2) whether or not the FIFO is nonempty, and 3) whether or not the FIFO is past halffull.
All of these details may also be derived from r_first
and r_last
alone. If
they don’t match, the FIFO
is in an illegal state. Therefore, these properties are a perfect match
for learning
formal methods
The first step is to gate all of our work so that the synthesis tool will ignore it, unless we are working with the formal verification methods.
Next, within this FORMAL
block we want to make certain that the assumptions
we are going to make regarding our inputs will become asserts when this core
is included into a larger design. We’ll do this by creating an ASSUME
macro
that we can use to constrain our inputs.
Remember that you only want to constrain via ASSUME
statements about
parameters that can be set by a higher level module, not external inputs.
Earlier, I described what it would take to assume that the clock toggles.
We’ll repeat that here. We’re also going to insist that this
FIFO
starts in it’s reset state, by insisting that the i_rst
line is initially
valid.
Before leaving this beginning statement, let’s also insist that our inputs only change on the positive edge of the clock.
We also discussed above the need to know whether the $past()
function
would return valid results. We’ll use the f_past_valid
register for this
purpose.
This also highlights the fact that your formal verification logic may have and use registers, just like the rest of your logic–even though you won’t be using it within your design other than for formal verification.
Next, let’s look at making sure that our helper logic works.
First, the r_fill
output should be equal to the number of
FIFO
memory entries that are full. This is given by the difference between
r_first
and r_last
. Above, we chose to use a clocked register to hold this
value. We did this for timing reasons, but there is the possibility that
we got this wrong. So, let’s check it here. Formally, one might say that
the state where r_fill
doesn’t equal this difference is an illegal state.
Now, let’s move on to our empty flag. Any time the
FIFO
is empty, we want to set the will_underflow
flag. In addition, we want
o_empty_n
to be true any time we are not empty. As I mentioned before, the
FIFO
is empty any time r_first
is equal to r_last
. We can use f_fill
from
above for this purpose.
In a similar value, any time the fill is one less than the number of items in the buffer, then the buffer is “full”. Let’s make sure we got that logic right too.
The
FIFO
code
also has a value, r_next
, which is supposed to
reference the next value to be read. To know if we got this right, let’s add
one to the r_last
pointer,
and then look to see if r_next
equals this as desired,
Finally, let’s examine the pointers under overflow and underflow conditions. First, on any reset, both pointers will be set to zero and any output error will be cleared.
If we are not in reset, we might have an underflow. Let’s check. If the
FIFO
was empty on the last clock, and if there was a request to read from the
FIFO
on that clock, then we had an underflow. In that case, assert that the
FIFO
read pointer, r_last
, has not changed as a result.
Had this pointer changed, the FIFO might accidentally jump from the empty state to the full state with garbage in the buffer. We want to avoid this.
We do almost the same thing on an overflow condition, but there are just a
couple differences.
First, in the case of a read and write on the same clock while we are full,
no overflow has taken place. Hence we need to check that a write without
a read has taken place. That’s the first difference. The second difference
is that this core reports overflow conditions, but not underflow conditions.
Hence, we assert that o_err
is true on any overflow. Likewise, on any
overflow we also assert that the r_first
pointer hasn’t changed.
As with the underflow, a pointer change during an overflow condition can be catastrophic as well. It could cause the FIFO to suddenly become empty, losing any of the data within it. This formal check about tells the theorem prover that doing so would be illegal, and that we want to know if anything would create such a condition.
What we haven’t discussed are the instructions for installing yosys, SymbiYosys, and the various theorem provers. These may be found on line. Neither have we discussed the Makefile I used to coordinate the proof, nor the yosys config that I used. Feel free to examine these on your own if you would like.
What did I find?
You may recall from earlier that I found several errors in my FIFO as a result of using these methods. If you are reading this, then you may be wondering just how significant those errors were. Here are some of the things I found:

Originally, I had said that a write during an underflow would only take you out of the underflow condition if there was no read at the same time. This is wrong.
A write to an empty FIFO will always succeed, independent of whether or not a read is taking place at the same time, and a read from an empty FIFO should always fail–independent of a write taking place at the same time.
Fixing this required several changes throughout.

I hadn’t initialized all of my variables. In particular,
r_next
andr_fill
weren’t originally initialized. 
When calculating the number of elements in the FIFO, I had assumed that if the
will_overflow
value was true that any write to the FIFO would overflow the FIFO. This isn’t the case. Ifwill_overflow
is true, then any write without a concurrent read will overflow the FIFO. A read and write during the same clock period will not overflow the FIFO.
If you’d like, all of the changes are captured within the github repository on line, so you can review what I found here.
Final Thoughts
Please keep in mind, I’m only a beginner at formal methods. I’ve never used any of them before this week, but I’ve already found several problems in my own code using them. Are formal methods worth the effort? Well, for me and in this example, they were.
I’d like to come back to this topic in the future after I’ve learned some more. I’d also like to apply these methods to many other problems as well. However, I’ve also got some problems which I’m not yet certain how to prove. For example, while I’ve managed to prove a low level QSPI flash driver, I have yet to figure out how to prove the entire protocol. Likewise, I’ve managed to prove that my UART transmitter (lite) works, but not yet the receiver or the entire IP core including the wishbone interface.
For now, I think I’ll just see if I can’t prove my WB to AXI4 bridge next. I think that would be useful for all.
Ye have heard that it hath been said, Thou shalt love thy neighbour, and hate thine enemy. But I say unto you, Love your enemies, bless them that curse you, do good to them that hate you, and pray for them which despitefully use you, and persecute you (Matt 5:44)