Jump to content

My own journey with Formal Verification


Recommended Posts

At the invitation of @zygot, I thought I might share about my own experiences using formal verification when building FPGA designs.  This comes up in the context of debugging Xilinx's AXI-lite demonstration code, and from demonstrating that with an interface property file any AXI-lite core can simply be debugged with only about 20 or so lines of code.

So how did I get here?

I imagine that most FPGA users in this community probably start out their journey without formal verification.  They either start out with VHDL/Verilog or with the schematic entry form of design.  I personally started out with Verilog only.  I never learned to simulate any of my designs until a couple of years into my own journey.  About two years after that, I learned about doing formal verification with yosys-smtbmc, and then with SymbiYosys.  (SymbiYosys is a wrapper for several programs, including yosys-smtbmc, that has an easier to use user interface than the underlying programs do.)

The first design I applied formal verification to was a FIFO.  By this time I was quite confident that I knew how to build FIFO's.  (Imagine a puffed out chest here ...)  In other words, I was very surprised when the formal tools found a bug in my FIFO.  (That puffed out chest just got deflated ..)  This was my first experience, which I would encourage you to read about here.

Why didn't I find the bug with simulation?  Because there was one situation/condition that I just never checked with simulation: what should happen when reading and writing an empty FIFO at the same time.  Perhaps I'm too junior when using test benches, perhaps I'm just not creative enough to imagine the bugs I might find, either way this just wasn't a situation I tested.

Some time later, I was working with my ZipCPU and had to trace down a bug.  You know the routine: late nights, bloodshot eyes, staring at GB of traces just to find that one time step with the error in it, right? You can read about it the mystery bug here.  (Spoiler alert: I found the bug in a corner case of my I-cache implementation.)  Wouldn't you rather instead use formal methods to find bugs earlier and faster?  I certainly would!  Anything to avoid needing to dig through GB of trace files looking for some obscure bug.  You can read about the three formal properties you need for verifying memory designs (such as caches) here--had I verified my I-cache using these three properties, I would've found the bug much earlier.

After that first experience with the FIFO, I started slowly working my way through all of my cores and applying formal methods to them.  I discovered subtle errors when building even a simple count-down/interval timer.  With every bug I found, I was motivated all the more to continue looking for more.  I was haunted by the idea that someone might try out one or more of my cores, find that it doesn't work, and then write me off as a less than credible digital designer.  (Remember, I was looking for work during this time and using my on-line digital designs and blog as an advertisement for my capabilities.)

One ugly bug I found in my SDRAM controller would've caused the controller to read or write the wrong address in certain (rare) situations.  None of my test benches had ever hit these situations, nor is it likely they would have.  You'd have to hit the memory just right to get this error.  In other words, had I not used formal methods, I would've found myself two years from now wondering why some
ZipCPU program wasn't working and not realizing that the (proven via simulation and testbench) SDRAM controller still had a bug within it.

What does design using formal methods look like?  The design flow is a bit different.  Instead of simulating your design through several independent tests in a row, and then looking through a long trace to find out if the design worked, formal methods get applied to several steps of a design only.  If your design fails, you will typically get a trace showing you how the design could be made to go into an unacceptable mode.  You can then adjust your design, and run again. In that sense, it is very much like simulation.  However, unlike simulation, the trace generated by the formal tool stops immediately at the first sign of a bug, leading you directly to where the problem started.

I said the trace tends to be short.  How short?  Often 20 cycles is plenty.  For example, 12 steps are sufficient to verify the ZipCPU for all time, whereas 120 steps are necessary to verify a serial port receiver with an assumed (asynchronous) transmitter with a dissimilar clock rate.  This is very different from running an instruction checking program through the CPU, or a playing a long speech through the serial port receiver.

As you might imagine, like the other examples, when I finally got to the point where I was ready to verify the full CPU I found many more bugs in my "working" CPU than I expected I would find.

As a result of these experiences, I now apply formal verification during my design process--long before I enter any "verification" phase.  Any time I need to re-visit something I've written before, I immediate add properties to the design so I can use formal methods.  Any time I design something new, I now start with formal methods.  I will also use formal before simulation.  (It's easier to set up than test benches were anyway.)  I use cover() statements to make sure my design can do what it is supposed to, and assert() statements to guarantee that it will never do what it isn't supposed to.

While formal can find bugs in corner cases, and it can do so relatively quickly, it isn't the solution to every problem.  The formal engines struggle with an exponential explosion of possibilities that need to be checked.  As an example, both multiplies and cryptographic algorithms have been known to hit this combinatorial explosion limit relatively quickly.  (I can exhaustively verify a multiply with Verilator in 15-minutes that would take over 4-days with formal methods.)  For this reason, you want to keep the design given to them relatively simple if possible.  That doesn't mean that you can't formally verify large designs.  As an example, I recently formally verified an FFT generator.  I just did it one piece at a time.

I still use simulation.  Why?  Because of the combinatorial explosion problem associated with formal methods, I tend to only verify components or clusters of components but never my whole design.  Using Simulation, I can get the confidence I am missing that my entire design works.  Besides, would you believe me if I told you my FFT worked without showing you charts of the inputs and outputs?

Only after a design (component) passes both formal verification and simulation will I now place it on hardware.  Why?  Because it's easier to debug a design using formal than using simulation, and it's easier to debug a design using simulation than it is to debug it on the actual hardware.

Eventually, SymbioticEDA approached me in January of last year, after I had been convinced to use formal verification for all my projects and after I had started writing about my experiences, and asked me to do contract work for them.  If you aren't familiar with SymbioticEDA, they are the company that owns and maintains SymbiYosys.  My first job for them was to create a training class to teach others how to use their tool.  I was a natural fit for this job, since I was already convinced in the efficacy of the formal methods they had made available through SymbiYosys.  I've had other jobs with them since, to include formally verifying a CPU that had been committed to silicon several times already.  (Yes, there were bugs in it.)  In other words, while this may sound like a paid advertisement, the experiences I've had and discussed above have been genuine.

If you've never tried SymbiYosys, then let me invite you to do so if for no other reason than to determine whether or not my own experiences might play out in your designs.  SymbiYosys is free and open source, and using it to verify a Verilog component will cost you nothing more than your time.  Feel free to share with me your experiences if you would like.  Likewise, you can find many other articles on these topics at zipcpu.com.

Dan

P.S.  I'm slowly building a tutorial on how to design using Verilog, Verilator, and SymbiYosys.  The course is intended to be (somewhat) hardware agnostic, so you should be able to use Yosys, Vivado, ISE, or even Quartus with it.  Each lesson consists of a new concept and a design that will teach that concept.  The lesson then goes over the steps to building the Verilog, Simulating the design and co-simulating any peripherals using Verilator, as well as formally verifying the design using SymbiYosys.  While the tutorial remains a work in progress, many have enjoyed it even in its incomplete state.

P.P.S.  In my "story" above, I didn't pay attention to chronology, so some of the events may appear to be out of order with reality.

Link to comment
Share on other sites

@D@n,

Thanks for the post. I find it to be very interesting reading.

1 hour ago, D@n said:

Perhaps I'm too junior when using test benches, perhaps I'm just not creative enough to imagine the bugs I might find, either way this just wasn't a situation I tested

This is a problem with RTL verification using testbench code and standard logic simulation. It requires a lot of experience ( generally learning about all of the ways your RTL code might fail and long hours of debugging ) to get a sense of where to look. The obvious (highly case specific) usually covers the dumb errors but this is rarely good enough for implementations that don't tolerate failures. The difficulty comes when your design fails in hardware once every couple hundred million clocks. There are some solutions to  helping identify corner cases of RTL behaviour. One is automation. A tool that systematically checks for all possible logic combinations can't be a bad thing. But this is still RTL simulation/verification.

1 hour ago, D@n said:

Eventually, SymbioticEDA approached me in January of last year, after I had been convinced to use formal verification for all my projects and after I had started writing about my experiences, and asked me to do contract work for them.

I appreciate (expect) your openness about your relationship with the owners of the tool. This wasn't stated in your blog ( as far as I noticed ). I don't read much into this as I can usually spot a 'sales pitch' even when it's completely free of encumbrances. Sometimes we hit upon an idea or tool that just gets us excited. But still it's nice to know for context. Personally I'm open to new ideas and methodologies if they are presented in a way that relates to my experience and stimulates my curiosity.

I'll be interested in any tutorial that you come up with.

As far as I can see the SymbiYosys tool is an extension of Verilog that helps automate RTL simulation/verification. This still doesn't cover post place and route timing simulation and by extension is not a replacement for it.

What I haven't found is a cogent document describing what SymbiYosys does or how it does what it does. Any help that you can provide in this regard would be appreciated. I do intend to investigate further.

I do admit that I'm a bit skeptical; Over the years I've been promised a lot from expensive tool vendors only to be disappointed. One thing that I haven't worked out is how SymbiYosys understands the synthesis tool for various FPGA vendors. You'd think that syntax implies a determinate implementation in a particular devices resources. Having used synthesis tools from at least 5 FPGA vendors I can say with certainty that this is not so. I've had code that generated errors using Quartus that produced expected results in Vivado. It depends on how and when things are evaluated. And of course bugs come and go in all vendors synthesis tools. Usually companies opt to use something like Synplicity as the final word over the vendors synthesis tool.

Link to comment
Share on other sites

@zygot,

5 minutes ago, zygot said:

Thanks for the post. I find it to be very interesting reading.

Thank you!  I'd given you up as a lost cause.  :D

5 minutes ago, zygot said:

This still doesn't cover post place and route timing simulation and by extension is not a replacement for it.

We can continue this discussion in the forum thread we started it in.  I've heard enough from others to suggest you are right in this, I just don't know enough that I could explain it convincingly, so I need to learn more about the issue.

5 minutes ago, zygot said:

This is a problem with RTL verification using testbench code and standard logic simulation. It requires a lot of experience ( generally learning about all of the ways your RTL code might fail and long hours of debugging ) to get a sense of where to look.

Let's start here, since you have just highlighted one of my own struggles when analyzing my own experience.  I cannot separate how much of the problems I found and solved via formal were because I didn't know how to write a good test bench, and how many of them are a result of the formal tools just being fundamentally better approach to digital design.  I appreciate your insight here, and would love to hear your insight again after you've tried the tools a couple of times on your own designs--should you choose to do so.  Your experiences might help me answer this question.  Quick hint here: start simple, work up to complex--as with anything in life.

5 minutes ago, zygot said:

I'll be interested in any tutorial that you come up with.

It's a work in progress, but I'd be glad to let you know when the entire tutorial is complete if you would like.  There is already a discussion on how to use SymbiYosys that starts in lesson 3 on FSMs.  SymbiYosys tasks are covered in lesson 4, as is the $past() operator.  My current work is focused on the block RAM chapter as well as the serial port receiver chapter--to include how to verify each.

5 minutes ago, zygot said:

As far as I can see the SymbiYosys tool is an extension of Verilog that helps automate RTL simulation/verification.

What I haven't found is a cogent document describing what SymbiYosys does or how it does what it does. Any help that you can provide in this regard would be appreciated. I do intend to investigate further.

Well, not quite.  Let me try to clarify.  Yosys (not SymbiYosys yet) is a Verilog synthesizer.  It can ingest Verilog and output one of several outputs types including EDIF (for working with Xilinx tools), VQM files (for working with Altera), JSON (for working with the open source NextPNR tool), and Aiger and SMT2 (for working with formal solvers).  That's one program.  Next, there are several formal solvers available for download from the internet: abc, z3, yices, boolector, avy, suprove, etc.  These are separate from Yosys and SymbiYosys, although SymbiYosys very much depends upon them.  These solvers accept a specially formatted property file as input--including Aiger (avy, suprove) and SMT2 (z3, boolector, yices) as examples.  SymbiYosys is a fairly simple python script that connects these two sets of tools together based upon a setup script.  The official web site for SymbiYosys can be found here, although I'll admit I've blogged about using it quite a bit. (Try this article regarding asynchronous FIFOs for an example.SymbiYosys itself can be found on github, just like Yosys and the various solvers, together with some examples that can be used to test it.

As for the the comment about SymbiYosys implementing an extension of Verilog, please allow me to clarify again.  The "extensions" you refer to are actually a subset of the System Verilog assertion language found in the SystemVerilog standard.  (No, the entire SV language is not supported in the open version, neither is the entire SVA subset supported.)  Yosys supports the "immediate assertion" subset of the SVA language.  In particular, it supports making assertions, assumptions, and cover statements within always/initial blocks, but not these statements on their own.

5 minutes ago, zygot said:

I do admit that I'm a bit skeptical; Over the years I've been promised a lot from expensive tool vendors only to be disappointed. One thing that I haven't worked out is how SymbiYosys understands the synthesis tool for various FPGA vendors. You'd think that syntax implies a determinate implementation in a particular devices resources. Having used synthesis tools from at least 5 FPGA vendors I can say with certainty that this is not so. I've had code that generated errors using Quartus that produced expected results in Vivado. It depends on how and when things are evaluated. And of course bugs come and go in all vendors synthesis tools. Usually companies opt to use something like Synplicity as the final word over the vendors synthesis tool.

Please do be skeptical.  I've been very skeptical of it, but you've just read my conclusions from my own experiences above.  I'd love to hear your thoughts!  Also, feel free to send me a PM if you have any struggles getting started.

As for your next statement, SymbiYosys doesn't understand the synthesis tool outputs from the various FPGA vendors.  It understands (through Yosys) Verilog plus the immediate assertion subset of SVA (System Verilog Assertion language).  That is, you'll need to provide the properties together with your design in order to have SymbiYosys verify that your properties hold as your design progresses logically.  Further, I normally separate my design logic from the formal properties within by `ifdef FORMAL// and `endif lines.  This keeps things so that Vivado/Quartus/Yosys can still understand the rest of the logic, while SymbiYosys or rather Yosys can understand the stuff within the ifdef as well.  One last item: Verilator understands many of these properties as well--they aren't unique to SymbiYosys.

Hope this starts to make some more sense,

Dan

Link to comment
Share on other sites

Archived

This topic is now archived and is closed to further replies.

×
×
  • Create New...