# Aggregating verified modules together

If you’ve been following my work with the ZipCPU, you’ll know that I have formally verified all of the leaf modules, and that I am now working on verifying the CPU as a whole. By “leaf module”, I mean a design component that references no other design components. You might also remember that I am rather new to formal verification, having only picked it up within this last year. Verifying the ZipCPU may be the most complex design I’ve tried to verify yet.

Prior to my attempts at formally verifying the
ZipCPU,
the most difficult proof I had worked on was for a proprietary block
floating point module. That module assigned a single exponent for all
of the values within a block of `2^N`

numbers, and then output the input
numbers sequentially together with their assigned floating point value. Like
the
ZipCPU,
it also involved proving a module with a leaf module underneath it.
The alignment was very difficult to get right in that implementation
and so I dependended heavily upon the formally verified
properties
of those two modules in order to have the assurance that the component
even worked.

Along the way, I’ve learned that there are some tricks to aggregating formally verified submodules together in order to prove the whole. I’ve now learned two particular techniques, abstraction and invariants, to help control the complexity of a formal proof. Today’s discussion will focus on invariants. If the Lord is willing, we’ll come back and discuss how to use abstraction, and present several examples of it.

I would love to declare, before starting out, that I am an expert on these techniques. I’m not. Perhaps if I had found some article or set of articles describing them I might be able to declare some amount of expertise. Sadly, while I found a small number of articles describing invariants, I struggled to relate the concepts presented within those articles to the formal verification problems I was dealing with. The one source I found to guide me along this road was a presentation from OneSpin Solutions at DVCon 2018 in San Jose.

So with credit to OneSpin Solutions, here’s what I have learned about invariants and how they apply to Formal Verification. More than that, I’ll try to keep this presentation simple enough to be understandable, and focused on how these topics apply to the formal verification of complex RTL modules.

## Formal Property Review

If you are coming in to the discussion late, then there are two concepts
you must understand in order to follow the discussion below. These are
the `assume()`

and `assert()`

System Verilog operators. I like to explain
these with a set of diagrams describing the state of a design at any
given point in time.

One such example state diagram is shown in Fig 2. Consider every point in this image as representing one state of all the flip-flops in your design. Any change to one of the flip-flops in your design will move your system’s state to a new point on the diagram.

Several parts of this diagram are worth noting.

First, note that your design starts from an initial state, as defined by the
`initial`

statements within your design. From this point, the inputs to your
design together with the logic within your design will cause the design
to move from one state to another.

Second, note that there are three different types of states you can be in.
The first set of states are the set of “valid” states. These are all of the
states that may be reached from your initial state without violating any
`assert`

ions within your design. These are shown in green.

The second set of states are those shown in red. These are the “illegal” or
“invalid” states. These are defined by all those states that violate an
`assert()`

statements within your design.
Your goal, using formal methods, will be to prove that you cannot cross from
a point in the set of valid states to one of the invalid states.

There is a third set of states. This set is shown by the largest region
containing all of the others. This is the
universe
of all possible sets of
flip-flop
(register) combinations of values within your design. Initially, this set is
defined by every
flip-flop
combination in your design. Hence if you have `N`

flip-flops
in your design, then without any further assumptions there are initially
`2^N`

states in this set. Not all of these states will be *reachable* from
your initial state.

Within your design, you have two sorts of statements you can make about the
flip-flops
within your design. The first is the `assume()`

statement. This reduces the
size of the
universe
of values your
flip-flops
may be set to.

To use the example of a counter,

we might assume that the `i_reset`

signal is always zero.

This will restrict the
universe
of possibilities to only those where `i_reset`

is
always zero.

The goal of
formal methods
is to examine *every possible* state your design can enter into in order
to prove that your design will never reach an *invalid* state.
As I’m sure you can imagine, this task can be a challenge. In general, this
challenge is `NP-hard`

–the computational complexity is roughly exponential
in the size of the
universe
within your design. Hence, the smaller you can make the
universe
of possibilities the easier it will be to verify a design.

The second basic formal statement is the `assert()`

statement. Unlike the
`assume()`

statement which limits the size of the search space, the `assert()`

statement declares particular states within that
universe
are somehow “illegal” as shown in Fig 4. When you use
formal methods,
your goal will be to guarantee your design remains in a legal state.

If we return to the
timer example
above, we might assert that value of the counter is never one greater than
`TIMEOUT`

.

When applying
formal methods
to this example, the engine will quickly point out that
the initial state may lie within the red or illegal states–since we did nothing
to restrict `r_value`

s contents initially.

These two operators, `assume`

and `assert`

, alone should be enough to get you
started with
formal methods,
and there’s a lot you can do with them. However, if you want to *prove* that
your design will work for all time rather than just the first `S`

time steps,
then you will need to apply the
formal method
called
induction.

Induction
starts by assuming your design is somewhere among the
universe
of all possible states, and that the initial state the engine has chosen
is not illegal. Its first
step is to create `S`

time steps where your design stays out of the
illegal set of states. Then, on the `S+1`

time step, it tries to see if it
is possible to enter into the set of illegal states.

The difficult part of this inductive step is that the formal engine cannot tell the difference between reachable states and unreachable states. This can be particularly problematic for the new user of formal methods to understand. A common refrain is, “how did the formal engine put my design into this state? There’s no way it can get there!”

Addressing this problem was the subject of a
prior article.
In that article, I explained that you must use either an `assume`

or an `assert`

to keep the formal engine from reaching any unreachable states, or you will
never be able to fully *prove* your design meets the properties you have
asserted for all time.

Following our example of a timer, the formal engine might pick a value for
`r_value`

that was `TIMEOUT+S+2`

. It would then follow `r_value`

for
`S`

steps until `r_value`

was `TIMEOUT+2`

. On the next step, our property
that `(r_value != TIMEOUT+1)`

would be violated.

To fix this, one would need to assert instead that `r_value <= TIMEOUT`

.

This makes the size of the “red” area large enough to include the whole
universe, as shown
in Fig 5. To follow the consequence of this in our example above,
`r_value`

would never be allowed to be `TIMEOUT+S+2`

. It would only be allowed
to have a valid value.

To know which of the two, `assert`

or `assume`

, is appropriate at any given
time, I’ve always used what I call the *master rule of Formal Verification*
shown in Fig 6: *assume inputs*, then *assert* properties of both
*internal states and outputs*.

This rule has served me well for all of my formal verification efforts to date. Now that I’ve discovered I need to aggregate modules together, I’ve had to learn some of the fine nuances of this rule. These nuances are the subject of the rest of this article.

## The Concept of an Invariant

What the master rule of
formal verification
doesn’t capture is how you deal
with things that have already been proven. For example, let’s suppose `A`

is a set of assumptions, and `B`

is a set of assertions. Once you’ve proven
that `A`

implies `B`

, which I shall write as `A->B`

, then you shouldn’t need
to prove it again.

This is the concept of an Invariant. Once you know that `A->B`

, then `A->B`

becomes an invariant of your design. Instead of reproving it, you may now treat
it as an assumption. This becomes especially useful when trying to deal
with complex proofs. If you can reduce the complexity, you can then verify
larger and larger designs.

There are two situations where I have found to apply this. The first is that of a parent module with a child (or leaf) module underneath it. The second place is when the proof of a design can be broken into separate sections. I’ve encountered both while trying to verify the ZipCPU. We’ll examine each in turn.

To explain the first situation, consider the module hierarchy (file structure) of the ZipCPU shown in Fig 8. The ZipCPU consists of a master CPU file, an instruction decoder, an ALU with a multiply component within it, a twin bus arbiter, and one of two memory controllers. I use the red bar in Fig 8 to indicate the formal properties within the design. Normally these properties are found at the end of the source file. You’d therefore normally expect this red bar to be at the bottom of each file within the diagram. However, since the concept of invariants turns these properties on end, I show the red bar in this figure at the top of the file–for illustration purposes.

The other three components of the ZipCPU were abstracted. These were the prefetch, divide, and multiply. These are shown in Fig 8 as empty files with dotted lines around them, indicating that due to the abstraction they have very little logic remaining within them. You can find their abstract representations in my bench/formal directory. These also made the proof easier, but for now we’ll leave the mechanics of this for a topic for a future article.

To understand how I applied the principle of invariants to this design, consider Fig 9. This shows a parent module and a leaf or child module–both with assertions and assumptions within them.

In my first step, I verified that the leaf module works. This is shown in the left side of Fig 9. During this step, I ignored the parent module, and only proved that if the child’s assumptions held then the child would never enter into an illegal state.

Once the assumptions and module logic had been used to prove the assertions within the module, I then switched my focus to the parent. This is shown on the right of Fig 9. In this case, I no longer needed to prove the properties of the child. Instead, I needed to prove the properties of the parent. To do this, I asserted that the assumptions of the child held, and then assumed that the assertions therefore held as well.

Hmm, that statement was about as confusing as some of the mathematical articles I’ve read on this topic. Let me try explaining that again.

Suppose we let `LA`

refer to the set of assumptions within the leaf module, and
`LB`

refer to the set of assertions within the leaf module. By
formally verifying
that module, I’ve now proved that `LA -> LB`

.
Unwrapping this a touch, this is equivalent to the
statement that either `LA`

is false, or `LB`

must be true: `(!LA)||(LB)`

.
Said another way, either one of the assumptions of this module must be false,
or all the assertions must be true.

Now I want to move on to the parent module. In this case, I have the additional
assumptions `PA`

and assertions `PB`

from the parent and I would like to prove
that `PA->PB`

.
However, I also need to deal with the leaf module. For the leaf module, I
know that `LA->LB`

. What I don’t know is whether or not `LA`

holds since
it consists of values provided by the parent module. Unless and until I know
that `LA`

holds, I really know nothing about `LB`

. Further, since the wires
composing `LA`

come from the parent, what I really need to do is to *assert*
these properties hold in order to guarantee the proper functioning of the leaf.
Hence, I will now assert `LA`

and assume `LB`

. This is backwards from how I
treated these components before. As a result, I will assume `PA&LB`

and assert
`PB&LA`

.

The fascinating part of this is that the master rule of
formal verification
still applies. We’re still *assuming* the inputs to the parent module and
*asserting* the properties of the internal state and any outputs. How can this
be? It works because the
flip-flops
composing the internal state of the parent module are the input
connections to the child. Hence the assumptions of the child’s inputs
are now outputs from the parent and so they may be asserted. Likewise the
child’s outputs are now the parent’s inputs, and so it makes sense to make
assumptions about them.

It this is still confusing, relax, I’ll show some code snippets to illustrate how I applied this concept in the next section.

The second way that invariants can be used within a design is within a given design component (module). In my case, it was within the ZipCPU core. In this case, we’ll separate the assertions into groups of increasingly complex logic, called stages in Fig 10 below.

Let’s call these sets of assertions `B0`

, `B1`

, and `B2`

. For the first
formal proof, we’ll prove that the assumptions together with the design
logic prove the `B0`

property, `A->B0`

. Within the
ZipCPU core,
I call these `PHASE_ONE_ASSERT`

ions. Once we know that `A->B0`

,
we turn our attention to proving `B1`

. In that case, we now know that
`A`

is true by assumption, but we also know that `B0`

is true by the implication
we just proved. So for this second stage proof, we assume `A`

*and* `B0`

and
attempt to prove `B1`

. We can then repeat this again, assuming
`A`

, `B0`

, and now `B1`

and proving `B2`

.

If you’ve examined the (current)
formal proof
of the
ZipCPU (it’s still a work in
progress), you may have noticed that I am using both of these methods.
First, I am verifying that the component pieces to the
ZipCPU
work as desired. Then, I am aggregating those into the proof of the
ZipCPU as a whole. Second, within the
ZipCPU, I’ve created two parts to the
proof: `B0`

and `B1`

. I’m expecting to create a third and possibly fourth
component later. Currently, I can prove both `B0`

and `B1`

using
SymbiYosys.

According to OneSpin Solutions, this method can increase the depth of the proof or rather the number of state transitions that can be examined in a reasonable amount of time by perhaps a thousand fold. These are their numbers, though. In my own experience, I can only say that formally verifying the second stage of the ZipCPU used to take longer than all night. (I’m not really sure how long–I never let it finish.) It now takes just over an hour.

## How this concept appears in Verilog

The previous sections have discussed a lot about formal verification in the abstract. They’ve been so far from coded reality that I would imagine I’ve now left several readers wondering what I’m talking about. So let’s bring these abstract concepts to reality, and discuss how they might look within a piece of Verilog code.

We’ll start with a fairly plain Verilog module. Almost all of my modules have the following rough format.

They start with a copyright statement, and then declare the `default_nettype`

to be none instead of wire. (This catches a *lot* of bugs.) The module
definition then follows with the core logic within it. Following the module
logic, there’s an `ifdef FORMAL`

delimited section ending just before the
`endmodule`

on the last line of the file. Inside that section I
place any assumptions or assertions regarding the logic above. Indeed,
if you browse through any of the code I’ve formally verified, you’ll find
this to be the common form.

If it is possible that this might be a leaf or child module to some other
module within a formal proof, then I’ll make some adjustments to the formal
section. First, I’ll use a synthesis define to indicate `THISMODULE`

is
the module being verified. Inside the module’s yosys script, I’ll also
modify the `read_verilog`

command to include a `-D THISMODULE`

. So, for
example, within the pipelined memory controller
module,
there’s a check for whether or not `PIPEMEM`

is defined. Likewise, you
can see the definition within its its yosys
script.
Second, I’ll define macros which I can then use to reference either the
`assume`

and `assert`

statements. If `THISMODULE`

is defined, these
will refer to `assume`

and `assert`

as expected. If not, they’ll be
swapped. Then I rewrite the formal properties to use these macros.

This is how I handle creating the logic pictured in Fig 9 above within any of the non-abstracted child modules.

Perhaps the best example of how this might be useful is in the ZipCPU’s pipelined memory controller. The “contract” the ZipCPU has with the user is that it will not speculatively execute memory operations–since the ZipCPU places both memory and peripherals on the same bus. Bus operations may be pipelined, meaning that multiple reads may be ongoing at any given time. Now consider, what would happen if one of those reads set the program counter? There would be no way to undo any of the other reads that might be in progress by this point.

For example, consider the following string of loads. In the
ZipCPU ISA,
an `LW`

instruction loads a word of data from the bus into the register given
as the second argument. (ZipCPU
instructions read left to right.) The second to the last of these loads reads
a value into the
program counter.

Any time the program counter (PC) is set, the CPU jumps to a new instruction. Hence, this memory read into the PC is really a jump instruction.

Should the CPU initiate the read into `R6`

? No. Not until the read into the
PC completes.

To check for this, the memory controller assumes that any read into the program counter must be the last read in a sequence. To formally prove this in an inductive manner, I need to check via assertions that the nothing in the pipeline of ongoing reads contains a read into the program counter. Once proven, the controller then asserts that if any output is to the program counter then it must be the last return value in the sequence. When this component is aggregated, the “check every FIFO element” code is quietly removed, being replaced only be the final assertion on the output. This final assertion, however, has been replaced by this process with an assumption that no longer needs to be checked–simplifying the proof of the ZipCPU as a whole.

The second method of applying invariants is the application within a given
file, as shown in Fig 10 above. In this case, you want to prove several
sets of assertions. Within the
ZipCPU
core,
I call these `PHASE_ONE`

, `PHASE_TWO`

, and so on.
Associated with each phase is an assertion macro, `PHASE_ONE_ASSERT`

,
`PHASE_TWO_ASSERT`

, etc. To then verify the component, you’d run it through
the formal engine twice: first as is, to test all of the phase one assertions,
and then again with `PHASE_TWO`

defined in order to test the phase two
assertions. The second set of assertions are excluded from being evaluated
during the first set by a synthesis `ifdef`

directive.

You can see the SymbiYosys script for this here.

The relevant code, shown below, was lifted from the beginning of the ZipCPU’s formal properties section. It starts out with a commented list of all of the formal phases supported by the ZipCPU module.

These aren’t strictly necessary, but they remind me which defines I am supporting.

Then each of the phases is given its own assertion macro.

If `PHASE_TWO`

is defined, the `PHASE_ONE_ASSERT`

macro is then redefined as
an assumption.

Likewise, if `PHASE_THREE`

is also defined then the `PHASE_TWO_ASSERT`

is redefined to be an assumption. This process then repeats for all of the
phases supported by the design.

At this point, the formal properties can proceed in sections. The first section makes any input assumptions necessary.

Then the first set of assertions follows these assumptions.

This set of assertions is created
using the `PHASE_ONE_ASSERT`

macro. That will allow us to replace these
assertions with assumptions in the next pass–once they’ve been proven
true in a first pass.

Later, we can split into a second section of assertions–but only after
we’ve used the formal tools to verify the first set of assertions, and only
if `PHASE_TWO`

is defined. In this latter section, assertions are created
using the `PHASE_TWO_ASSERT`

macro. Further, in order to get into this
section the `PHASE_ONE_ASSERT`

macro used the previous section will have
been redefined to be an `assume`

statement instead of the original `assert`

statement.

In the case of the
ZipCPU,
the second phase of
formal verification
includes several free variables (yosys’s
`$anyconst`

) used to track an arbitrary instruction from an arbitrary address
working its way through the ZipCPU’s
logic.

Using this method, I can reconstruct the operands for any operation before that operation is issued, and verify that they have the right values.

If you’ll recall from the article describing the
ZipCPU’s
instruction set,
almost all
ZipCPU
instructions have the basic form: `OP.C Ra,Rb+I`

, where `Ra`

and `Rb`

are
arbitrary registers, and `I`

is some immediate constant.

Prior to entering the
ALU
stage, the
ZipCPU
adds the `Rb`

register value and `I`

together. Then, while waiting for the
ALU
stage to become available, any write to either `Ra`

or `Rb`

adjusts these
values.

What makes this difficult is that, in order to keep clock speed high, there’s
no opportunity to re-add the immediate constant `I`

to `Rb`

–that would take an
extra clock tick. Dealing with this requires some careful pipeline stall
logic, and getting this logic right has been
tricky. By allowing the formal engine to pick an arbitrary pipeline state
and then examine an arbitrary instruction going into the
ALU,
I can guarantee that the `Ra`

and `Rb+I`

operands are valid no matter
which instruction precedes them.

Searching through all of the possibilities of these free variables can be expensive. Indeed, this was the phase that was taking many hours of processing as I was working on verifying this core module within the ZipCPU. Now, using this method of invariants, the entire formal verification of the (still not quite complete properties of the) ZipCPU takes less than two hours.

## Conclusion

Invariants are only one method of handling formal complexity when aggregating multiple modules together. As I mentioned in the opening, I am by no means an expert in formal verification, and so this is only my first application of the principle of invariants to any project–in this case the ZipCPU. However, even in the case of the ZipCPU, the value of using invariants has saved many, many formal verification CPU cycles.

We’ll have to return to this topic later in order to handle the concept of abstraction in formal methods. Abstraction may be an even more powerful concept than invariants. As you may remember from above, I’ve been using abstracted components to represent the prefetch, multiply, and divide components. As another illustration, consider this: when formally verifying any container of the ZipCPU, whether the ZipSystem, ZipBones, or some yet to be determined container, I’m anticipating being able to replace the entire complicated ZipCPU core with an abstracted version of it, and then to be able to prove the formal properties of the wrapper in question.

*And that ye study to be quiet, and to do your own business, and to work with your own hands, as we commanded you (1Thes 4:11)*