# An Exercise in using Formal Induction

In many ways I’m still quite the beginner when it comes to proving designs
using formal methods:
I’ve only used
formal methods
for about about five months. However, over those five months I’ve found
so many bugs in my “*working*” code that I’ve started using
formal methods
for every new component and design I’ve built since.

I’ve also found myself counseling others on the #yosys IRC forum. It’s been rather strange, though, since I very much feel as though I myself am quite the beginner, and yet I’m answering questions and explaining things as though I’d been doing this for years.

I haven’t.

However, I’d like to share with you today an example piece of code that really taught me a lot about formal methods, and in particular about the induction step. It’s come up recently as I’ve tried to explain induction to someone with even less experience than I have, and I’ve found that it makes a good and simple example to learn from.

I’ll be honest–my own mentors haven’t thought that much of the
example below. Their response
has been something like, “Oh, yes, of course.” Yet to me, I’ve found
this example
to be *very* instructive.

## The Example Code

The basic example
consists of two shift registers, `sa`

and `sb`

, although
the example would also work if you were comparing Fibonacci versus Galois
linear feedback shift registers
(LFSR)s–it just wouldn’t be
nearly as clear. However, the example does require that the two
shift register outputs need to be identical.

We’ll allow our two shift registers to have a parameterized
length, `LN`

, although for the purposes of today’s discussion we’ll only
set this length to a constant 16, `LN=16`

.

For this example to be instructive, both shift registers must have *identical*
logic. Therefore, we’ll initialize both registers to zero.

We’ll clear both registers on any synchronous reset.

Finally, any time `i_ce`

is true, the input value will be placed into the
least significant bit (LSB) of each shift register, while we shift the rest
of the register to the left.

In all other clocks, `sa`

and `sb`

will remain unchained.

Our example needs an output, so let’s set our output value to be the exclusive OR of the most significant bits in each register.

If these two shift registers are truly identical, then we should be able to assert this fact to the formal solver, as in:

If you stop here and try to prove this one property,

it will pass a bounded model check, but not induction.

Once I understood why this simple design struggled with induction, I was suddenly able to figure out why various designs were struggling with induction, and I then understood how to deal with it. Therefore, let’s spend the rest of this article discussing the difficulty with this design, and also how we might go about solving it.

## Running SymbiYosys

If you have SymbiYosys installed, then all it takes is a very simple script to run this test. Since adjusting parameters is fairly easy with SymbiYosys, we’ll use it for our tests today.

There are four basic parts to any SymbiYosys script: the options, the formal engine, the yosys script, and the list of component files involved.

In our case, we’ll want to use the formal mode *prove*. This will run both
the bounded model checker (BMC), *and* the
induction engine.
Other modes I’ve worked with include *bmc*, which just runs the bounded
model checker, and *cover*, which checks cover properties.
SymbiYosys
also supports a mode for checking liveness, called mode *live*, but I have
yet to try that mode.

We’ll also be adjusting the depth of the proof. This is the number of logic
steps the formal solver uses to test our design. In *bmc* mode, this will
be the number of clock cycles, measured from the beginning of time, that
are checked for any assertion failures. For the
induction step, in
*prove* mode, this will decide the number of clock cycles for both the *bmc*
pass and the
induction pass. For
the induction pass,
all but the last cycle will assume your `assert`

’s are true. On the last cycle,
however, the formal engine will try to find one example where it can show that
an assertion fails.

In my initial SymbiYosys script, I’ll set this depth to 31.

As I mentioned, we’ll be adjusting this value during today’s exercise.

We’ll also need to specify which formal solving engine we want to use. In this case, the yices engine will work quite nicely.

Other engines are available, and may produce different results.

We’ll then provide SymbiYosys with a very simple set of yosys commands to build our test,

Be aware when you are working with
SymbiYosys
that the `[files]`

section
will specify where your source files are coming from.
SymbiYosys will then copy
these files to a working directory before running
yosys,
so the `read_verilog`

command within the
yosys
`[script]`

section will reference all files
from within the current directory where
SymbiYosys placed them.

Let’s save this script to a file, kitest.sby. Put together, the whole SymbiYosys script will look like,

Assuming you have SymbiYosys, yosys, and yices installed, then all it then takes to run SymbiYosys is the command,

Pay attention to the last line returned by SymbiYosys. If all goes well, you’ll get the line:

However, if our design passes BMC (which it will) but fails induction, then this last line will instead read,

In the next section, we’ll look at what happens when we apply SymbiYosys to our example.

## Exploring what happens

Let’s spend some time exploring what happens within this example design, and see what it will take to get us to fully prove our property that the output bit will always be zero.

We’ll start out by describing a set of tests, each containing a different
approach to handling this problem. We’ll use the local parameter
`FORMAL_TEST`

to select from among several possible options for proving
this.

Now, let’s work our way through these tests, shall we?

When `FORMAL_TEST`

is zero, the test passes–much as we might expect.
Since it does pass, there’s no trace generated to examine and we can move
on. We’ll come back to this, though, in a moment.

When `FORMAL_TEST`

is set to `3'b001`

, however, the test fails. Why would
this be? It doesn’t make sense, right? I mean, if you look at the
code,
you can clearly (by examination) tell that `sa==sb`

, and so there must be
something wrong with the
formal methods,
therefore, if it can’t tell that these two are equal.

Well, not quite. Let’s dig a little deeper.

In particular, let’s pull up the trace associated with this failure. If you look through the SymbiYosys output, you’ll find the line ending with

We can open `trace_induct.vcd`

in GTKWave
and look at what’s going on here. You’ll find this file in the
`kitest/engine_0`

directory where
SymbiYosys
placed it.

If you look through the trace, you’ll notice that `sa`

and `sb`

are
indeed different.

What? How can this be?

To understand this, you need to understand a bit about how formal
induction works.
The induction step
works by picking random initial values for every registered signal within
the design. Well, okay, that’s not quite right. The values aren’t truly
chosen *randomly*, they are actually chosen *exhaustively*. Were they chosen
randomly, it might be possible to miss some choices that would cause the design
to fail. The benefit of formal, however, is that it will try every possible
combination in order to find one that will cause your design to fail.
To you as a developer looking at the traces through your code, it might feel
like these values are chosen *randomly*, although there’s actually a method
to this madness.

Either way, the engine knows nothing about whether or not the design could ever achieve the initial values it chooses. It only knows whether or not any of these violate any assumptions or assertions.

For the first 31 steps of this test, the only constraint upon `sa`

and `sb`

is
that their most significant bits are equal. The engine has kept this true for
us. Nothing in our example
constrains the rest of the shift register, either `sa[LN-2:0]`

or `sb[LN-2:0]`

,
so those values can be anything.

Then, in step 31, the engine chooses to set `i_ce`

high. This forces a
comparison between `sa[LN-1]`

and `sb[LN-1]`

on step 32, where the comparison
(which is formed by our assertion) fails.

This is obviously not what we want, so
what can we do to fix this? The most obvious answer is to
assert that `sa==sb`

. This is `FORMAL_TEST`

`3'b010`

. This test passes
very quickly, with little fanfare. This works.

What else might we do?

Suppose we went back and examined our first test again, with our depth set to 15 instead of 31. You’ll need to adjust the depth option within the SymbiYosys configuration script to do this.

As before, we can pull up the trace to see what happened.

In this trace, `sa`

and `sb`

are different again. This time,
though, the difference starts out in bit zero on the first timestep (not shown).
On every clock following, this one differing bit moves one step closer to our
assertion that the most significant bits of `sa`

and`sb`

are identical. As
this assertion is applied in the first 15 steps, it is applied as an
assumption–forcing the fifteen most significant bits of `sa`

and `sb`

to be
identical. However, on step 16, the assertion
is treated not as an assumption but rather as a full-blown assertion.
This time it fails, because we never told the formal engine that bits zero
in both shift registers were initially identical.

This suggests that this test will pass for a depth of 16. Feel free to try that one on your own.

Now let’s move on and try `FORMAL_TEST`

`3'b011`

.

In this test, `i_ce`

is never allowed to be zero for two clocks in a row.
It is allowed to be true on every clock, or to alternate between true and
false, or some combination between the two.

Let’s make one more change as well. We’ll set the induction depth to 30 steps in kitest.sby.

This test also fails.

As before, we can pull up the trace to see what happened.

This looks very much like the last test that failed: both failed because the
induction engine
allowed `sa`

and `sb`

to start out with different least significant bit.

The only thing that’s different here is `i_ce`

. In this case, the
induction
engine has chosen to alternate `i_ce`

with high and low.
Why? Because the alternating `i_ce`

value pushes the assertion regarding
this bit far enough forward in formal steps that the proof now fails.

However, it failed on the *last* step. I know,
induction
always only ever fails on its last step. That’s not what I mean. What I mean
is that if we just extend the search depth by one clock,

then this test will pass.

The last test, `FORMAL_TEST`

`3'b100`

, is very similar to test `3b011`

. I’ll
leave this one as homework for you.

I’ll also leave as homework for you the task of insisting that `i_ce`

is
true at least one of every eight clocks cycles. How many induction steps will
that take to succeed?

I like this example, because it does a good job fleshing out how the formal induction proof works.

Reality turns out to be very similar to this example, although it never looks
as simple. In most of the designs I’ve worked with, there’s always been some
amount of state that I can’t quite capture with a proper `assert`

statement.
By using a longer
induction
length, though, I can often force the state within my designs to flush itself.

Even this doesn’t always work.

You may remember my discussion of the formal
properties
of a wishbone
bus. Nothing within the
specification
forces a slave to drop its `STALL`

output to accept a new request within a
given number of cycles. Likewise, nothing within the specification forces
a slave to respond to the request by raising the `ACK`

signal within a
given number of clock cycles. This creates a possibility where there may
be some amount of hidden state. In order to deal with that possibility,
just like we forced `i_ce`

to be high at least one in `N`

clock cycles, I
would force
the stall line, `STALL`

, to be dropped if it was ever asserted for too long.
In a similar fashion, I would
prevent
the slave from waiting too many clock cycles before acknowledging a request.

## Other Approaches

If you have a chance to try some other formal engines, you may find they work better in this example. For example, the pdr engine,

avy,

and suprove

don’t seem to struggle with this problem.

## Conclusion

Induction may be the more difficult step of using formal methods. It need not be, but you need to understand how it works in order to understand the reasons while it might fail. The example above is, in my estimation, simple enough to show the difficulties with induction. If you understand the details of this example, this example, you should be ready to fully formally prove your own designs.

*And thine house and thy kingdom shall be established for ever before thee: thy throne shall be established for ever. (2Sam 7:16)*