I spent the first week of March, 2018, at DVCon in San Francisco, talking to vendors and asking questions regarding Formal Verification.

Many vendors offered Verification IP (VIP) modules that you could use in simulation to know that your interface matched the specification. These models would attach to your design, allowing you to then run tests on your design. When/if your design didn’t match what the protocol required, these commercial VIP modules would issue an error.

Indeed, it seems like the primary method of proving that an ASIC design would work prior to tape out is to feed the simulated design with random data and requests, over and over again, in order to get the design to fail. Several presentations discussed how to do this. Hardware was advertised that could help to make this happen. While I’ll admit that the level of effort discussed and presented goes well beyond my simple scripted test bench failures, it still only provides a small stochastic confidence that the design would work.

What a difference from formal!

When using formal methods, every path through the your logic is tested to determine if the design works. Every path.

This led me to wandering through the exhibit hall, asking vendor after vendor if they had any formal VIP. Perhaps 5-10% of the VIP available was available for proving something formally. While the reasons were mixed, the general consensus was that formal was more difficult to use, and so there wasn’t the same market for it. One vendor even declared that his tools were faster, better, and cheaper than formal, although less than formal in capability.

What?? Really? Is formal really all that difficult to use?

Let’s look at a simple example or two. Then, we can discuss how I go about getting started with formal on any new design, and what designs I apply formal methods to. Finally, we’ll attempt to address the question of whether formal methods really are all that hard.

Cover

Just one simple cover statement can have an amazing impact on a new design. As an example, in a recent design I was working on for the TinyFPGA, a project I am calling TinyZip, I simply inserted

always @(posedge i_clk)
	cover(o_wb_ack);

into the new/updated dual I/O flash controller. (I was starting with this QSPI flash controller.) If you aren’t familiar with a cover statement, you can consider it a challenge to the formal tools to find some way to make the predicate inside of the cover statement–in this case o_wb_ack–true. To do this, the formal tools needed to trace my design through the flash bring-up, the bus request, the address passing to the flash, and the return value.

No extra logic was required!

I didn’t need to build a simulation, to tell the simulator to tick the clock, tell it how many clocks to tick, feed it with just the right input along the way–none of that. With one line I had an example trace through the important parts of my code.

Was that all that hard?

Ok, so it wasn’t perfect: the bus wires were being driven incoherently. However, with some additional assumptions, such as those we discussed for the Wishbone Bus, the traces greatly improved. (No, the controller isn’t finished yet …) Later, I added another cover statement to make certain I could keep the design loaded with one request after another.

State Machines

Many of my designs use state machines that don’t completely cover all of the states bits available. For example, the “lite” versions of my serial port modules only use states 0-8 and 15. What if the design entered into any other state? Would such be possible? With just a simple assertion,

always @(posedge i_clk)
	assert((state <= 8)||(state == 15));

I can then use formal methods to tell me if my state machine will ever get out of bounds. Indeed, this concept is so useful, it’s worth discussing further in the next section.

Dependent logic

Formal methods are also very useful for making sure that dependencies between logic elements are captured. Hence, if you have two variables, A and B that must have a dependent relationship, formal methods are very useful for making sure that dependent relationship is maintained.

For example, many designs depend upon a state machine that transitions at a speed much slower than the system clock. My own UART implementation makes a great example of this. In this design, as with many similar ones, there is often a counter used to determine when the next state change will be.

always @(posedge i_clk)
if (counter != 0)
	counter <= counter - 1'b1;
else if (state_change) // && counter == 0
	counter <= NEW_VALUE-1'b1;

The problem with this approach is that within the state machine logic, I would need to place tests for whether or not counter == 0.

always @(posedge i_clk)
if (i_reset)
	state  == reset_state;
else if (counter == 0)
begin
	case(state)
	STATE_ONE:
		// ...
	end case
end

This test for zero can make the state transition logic unnecessarily complex, so I’ll often calculate it the clock prior with something like:

always @(posedge i_clk)
	zclk <= (counter == 1)||((counter == 0)&&(!state_change));

To determine if I got the logic right, I only need to formally verify that:

always @(posedge i_clk)
	assert(zclk == (counter == 0));

When the formal proof passes, I’ll know that these two dependent registers, zclk and counter, are guaranteed to maintain their dependent relationship. Hence, I can rely upon this dependency always being true within my code–as I intended.

Certainly other internal code dependencies can exist as well–often more complex than this one. For example, a packet index or address might need to be zero any time the network is idle. As I recognize that I have such a dependency when writing my own code, I’ll often quickly write an assertion to capture it. Indeed, I do this so often that I’ll discuss how to go about this in the next section.

While writing code

Often, when I write RTL, I’ll come across a situation where I recognize some dependency within my code that must be hold true. Rather than write a fully defensive piece of code that handles any potential internal failure, it is often effective (and easier) to write a quick assertion to remind myself to come back later and place this into the list of formal properties at the end of the module.

Making sure I remember all of these dependencies later can be a hassle.

Here’s a method I’ve found useful for that purpose.

As I’m working on creating a module,

//
// All files start with a (legalese) comment block
//
module name(/* portlist */);
	//
	// Module code is indented by one tab
	//

I’ll add any formal properties in line as I’m writing–but with the caveat that these ad-hoc properties are not indented like the rest of the code.

// Properties that need to be moved around later are not indented
// This helps me remember, when I see something that doesn't line
// up, that this property needs to be moved to another location.
always @(posedge i_clk)
	assume(!i_reset);

My development will then continue, returning to my original indentation scheme.

	//
	// Further module code (now indented again) may follow
	//

Then, some time later, I’ll collect these ad-hoc assumtions and assertions into a section at the end of the module together with the rest of its formal properties.

`ifdef	FORMAL
	// Here's where the formal properties will eventually be placed:
	// between `ifdef FORMAL and it's associated `endif.
`endif

For example, a UART baud counter should never count higher than one baud interval. Hence, as I’m putting my UART component design together, I’ll place an assertion to this effect into my code.

always @(posedge i_clk)
	assert(baud_counter < ONE_BAUD);

Some of my code, such as the dual I/O flash controller I mentioned above, depends upon the ability to peek at a bus request at certain times before accepting it. This requirement is easily captured by formal properties.

always @(posedge i_clk)
if ((f_past_valid)&&($past(request))&&(!$past(accepted)))
	assert(request_details == $past(request_details));

Once I realize this, usually while building the code, I’ll just write it in as I discussed above. Asserts and assumptions like this alone have helped me flush out many pipeline bugs!

Knowing that I intend to use formal methods to verify a design helps to encourage me to write properties within my code as I write my code–even though I’ll place those at the end of the file later.

Some modules are just too critical not to use formal

Some interfaces I deal with are just too critical not to use formal methods to prove a design component before introducing it to hardware. For example, just one misbehaving bus component and the whole design will come crashing down.

Remember how this happened to me in my first Cyclone-V project? Before I got the formal properties of the Avalon bus just right, I had to deal with several cases of hardware lockup. It would seem as though a Cyclone-V can’t recover if my own logic fails to lower the wait request line, or equivalently if it returns random bus responses that don’t follow requests). In my case, only cycling power ever rescued my design, leaving me wondering what had happened.

If you’ve been reading this blog for a while, you may now recognize this purpose in the formal WB properties post. Bus control logic is just too sensitive to mess up. All it takes is one master missing a response to a request and your design may be locked up until a hard reset.

Cache controllers are another example, as they can be a real pain to get right. Worse, all it takes is one ugly caching error and you may be spending days (or weeks) looking in the wrong place to find the bug.

My recommendation, therefore, would be that you consider this principle for any portion of your design that, if it fails, will cause the whole design to fail while leaving you in FPGA Hell. Formally verify those components early in your design cycle, before ever placing them onto real hardware. Then verify them again any time you change them.

Some simple contracts

I’ve recently started looking at the designs I’m building as providing a service, and so when I start building the design I’ll often create a contract to describe the service that must be provided. These contracts are usually just a couple of lines of formal properties that describe outputs in relationship to the designs inputs. Such design contracts are often so fundamental that if the contract holds, the design will be 80% verified (or better).

Consider, for a moment, some simple peripherals from the standpoint of a “contract”.

  • Bus requests should always be followed by a bus response. There should be no more responses than there are requests.

  • A cache should always return the value that would be found in memory at the given address, whether it needs to read from memory to get it or instead if it is already in the cache.

  • Reads from a memory controller (SDRAM, flash, etc.) should always return the value that exists in the memory at that location, and writes should change the memory.

  • An MMU should act as a bus bridge, between one set of addresses (the virtual ones) and another (the physical ones), while creating page misses for anything that doesn’t match.

The neat thing about these contracts is that they can help me prove that an item works–to include passing the induction step. Specifically, until the contract can be proven, the induction solver will keep presenting me with traces I need to examine. This helps me know how many properties I need to write.

If the Lord wills, I’m hoping to blog about this concept soon with respect to a second ZipCPU prefetch module, showing how a contract can be written using a couple free variables.

Why do people think formal is hard?

After hearing that formal was too hard, I tried to gather all of the excuses I heard to see if there might be some merit to any of them.

  1. Induction is harder than Bounded Model Checking (BMC)

    Many of the simple examples I gave above would be perfect for bounded proofs. These proofs are only applicable for the first N steps (i.e the bound) following a reset. Bounded proofs are much easier than the full proofs, simply because in the case of a full proof you need to find ALL the internal dependencies. within your design and make them known to the formal engine via additional properties–whether they be assumptions or assertions. This can be a pain, and so I can understand that you might not wish to use induction at first. Even in this case, though, the bounded model check is still valuable–just not nearly as valuable as the full proof with induction.

  2. Some modules are just too complex to prove using formal methods

    This isn’t an excuse, nor should it be. It is just a reality.

    While I’ve been able to prove all of the leaf modules of the ZipCPU, the complexity of the CPU as a whole has caused me to pause before diving into it. While I think I can formally prove that it works, the sheer complexity has caused me to pause.

  3. The full System Verilog Assertions syntax can be confusing

    If you’ve looked at the articles I’ve written so far regarding formal methods, you may notice that I haven’t used the full System Verilog Assertion (SVA) syntax. This is for two reasons.

    First, the open source yosys synthesis tool that I’m using to get access to formal methods without re-mortgaging my home doesn’t understand this syntax (yet). Indeed, I’ve managed to formally verify many designs with only the subset that yosys supports. Since yosys is the tool I can afford, it’s the tool I’ve been using.

    Second, I’m in the process of building a class in formal methods. This class includes a section on how to use the full SVA syntax: properties, sequences, clocking blocks, bind statements, and more. Since I’ve now been introduced to the full SVA syntax, my initial impressions are that it is very expressive, terse and compact, and as a result it is confusing to those who are not familiar with them. On the other hand, the assert and assume statements I’ve used within always or initial blocks have been expressive enough for me, and simpler to understand.

    It just happens that this simpler subset is also the set that yosys currently supports.

  4. It can be really difficult to sell formal Verification IP, simply because formal verification is a form of white box testing

    Fig 3. Just attaching VIP to a formal design doesn't usually work

What I mean by this is that attaching any vendor supplied Verification IP module to your design isn’t as simple as just instantiating the two components within the same design. The formal methods, and induction in particular, won’t work if you just plug and play related design pieces together such as Fig 3. attempts to show. This makes it more difficult to sell, purchase, or use vendor provided Verification IP with formal.

In order to connect an external set of formal properties, such as those from a piece of vendor supplied Verification IP, to the formal properties within your own design–relevant portions of the design need to be constrained to be properly dependent with the VIP. Success in this fashion is far more intrusive, and not nearly as simple as just purchasing someone else’s IP.

Fig 4. Passing Induction requires component state to interact

Perhaps a good example of this is my Wishbone bus arbiter. Internal to the Wishbone formal property IP modules are the counters necessary to insure that slaves will only respond to outstanding requests. This requires counting the number of requests, the number of acknowledgments, and then making certain that there are never more acknowledgments than requests. When I then try to use these properties within the bus arbiter to pass induction, the formal engine may set these counters to any initial value it wants. However, the arbiter is designed so that only one master can ever have access to the bus at a time. This means that the counters for the two slave inputs and the master output must be kept in sync. Doing this requires knowledge of the counters within the Wishbone propert module, enough so that I can assert that when one bus source has access to the bus, the other sources number of outstanding requests must remain at zero.

always @(posedge i_clk)
if (r_a_owner)
begin
	// If A owns the bus

	// B must have no outstanding requests, nor may it
	// have received any acknowledgements
	assert(f_b_nreqs == 0);
	assert(f_b_nacks == 0);

	// The total number of outstanding requests must equal
	// the number of outstanding requests A is expecting
	assert(f_a_outsanding == f_outstanding);
end else begin
	// Else B must own the bus
	// Same properties as before, just reversed
	assert(f_a_nreqs == 0);
	assert(f_a_nacks == 0);
	assert(f_b_outsanding == f_outstanding);
end
Fig. Here's how I ended up attaching WB properties to a simple design

If you fail to do this, your design won’t be able to pass induction.

Even if your design doesn’t pass induction, (most big chip maker designs don’t) your formal properties may still be good enough to accomplish some purposes, since you can still find lots of bugs via a simple Bounded Model Check. You just can’t prove that your design will maintain those properties for all time.

Does it take a genius? Not really. Indeed, from my own experience, it just takes someone smart enough to write Verilog RTL in the first place.

Formal isn’t perfect

My thesis today is just that formal isn’t really any more difficult than normal RTL coding. Not only that, it fits nicely into the RTL coding process and even adds to it. Now that I’ve used it for a while, and now that I’ve found as many errors as I have using formal, I’m convinced from my own experience that it’s not really that hard. Indeed, if I had the choice today, I would find it difficult to start a project without the help formal methods provide.

While I was at the DVCon conference, I heard two fascinating comments regarding how valuable formal methods are, and many fascinating anecdotes. The first comment I scribbled down was that, “Without formal, 70% of the bugs in a design are found after the module is turned in. With formal, 80% of the bugs in a design are found before the module is turned in.” No, I’m not sure any more where these numbers came from, so if I can find the study I’d love to share it with you. The second comment was from one of the panelists who noted that a rough 80% of a verification engineer’s time is spent fixing the silly bugs. The implication in this statement was that, had only formal methods been used, the verification engineer wouldn’t need to be spending his time fixing the stupid mistakes.

Formal methods aren’t perfect. By that I mean that, in my own experience, I’ve still had to chase down bugs that “passed” a formal proof. These include problems with not constraining my design enough, with adding careless assumptions, and even misunderstood requirements.

However, I find formal methods easier to use than the alternative, and I also feel like I am finding more bugs by using them as part of my design process. As a result, I now use formal methods first, and then continue with simulation when I’m done.

So why do people think formal is all that difficult? My best guess is that formal methods appear difficult to those who have not tried them, and additionally to those selling Verification IP.