Clifford Wolf has written a nice tool,
yosys-smtbmc, based upon his
yosys synthesys tool, that allows you to apply
to your Verilog code. The promise of
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 SPI-based 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.
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 flip-flops, together with the values of all of your inputs.
The first step in yosys-smtbmc 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 yosys-smtbmc, 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
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,
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.
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
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,
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,
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
assert(), but with the exception that the theorem prover doesn’t try to
prove that the
assume() statement is true. Instead, it forces the
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
assume() statement removes particular states from the
realm of possibilities.
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
assert() statement were false.
restrict() instruction is similar to the
restrict() also reduces the size of the state space that
the theorem prover needs to work within. In that way, a
is much like an
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:
$fell(). Since these are important,
let’s work our way through them.
$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
N, defaults to one, so
$past(expression) is just the same as
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,
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
that with wishbone nothing happens
(i_wb_stb)&&(!o_wb_stall)? This means that once the
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
goes high, none of the bus request information will change until the
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
for the same effect:
The last of the basic commands you’ll want to know is the
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,
$fell() primitive exists as well for testing negative clock edges.
yosys provides one more helpful feature.
Anytime you use
to generate a formal description of your code,
yosys defines the
FORMAL flag. Hence, you
can surround your formal properties with
ifdefs, as in:
These, therefore, are your basic formal declaration statements:
restrict(). They are helped by the functions
$fell(), and perhaps some others that I
haven’t learned yet. (Remember, this is only my first week.)
declares statements to be illegal, 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.
The basic approach to formally describing your program is to
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
the values that will be passed to the lower level module rather than
A FIFO example
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,
The only time
r_last are equal is when the
FIFO is empty.
Likewise, the number of items within the
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 pre-compute two values:
will_overflow, which is true if the next write will overflow the
will_underflow, which will be true if the next read will read from an
All of these details may also be derived from
r_last alone. If
they don’t match, the FIFO
is in an illegal state. Therefore, these properties are a perfect match
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
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
starts in it’s reset state, by insisting that the
i_rst line is initially
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
would return valid results. We’ll use the
f_past_valid register for this
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.
r_fill output should be equal to the number of
memory entries that are full. This is given by the difference between
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
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
is empty any time
r_first is equal to
r_last. We can use
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.
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
was empty on the last clock, and if there was a request to read from the
on that clock, then we had an underflow. In that case, assert that the
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
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_fillweren’t originally initialized.
When calculating the number of elements in the FIFO, I had assumed that if the
will_overflowvalue was true that any write to the FIFO would overflow the FIFO. This isn’t the case. If
will_overflowis 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.
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)