Formal methods in verification flow

alexg · Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa

The following statistics is copied from J.Cooley's DVCON trip report
(http://www.deepchip.com/items/dvcon04-10.html):

"What do you think about "bug hunters" like 0-in, Jasper,
@HDL, RealIntent, Averant, or Synopsys Magellan (Ketchum)?
Does your company use such tools?"

don't use : ################################### 70%
0-in : ####### 14%
Jasper : ## 5%
Synopsys Magellan : ## 5%
RealIntent Verix : # 4%
Averant Solidify : # 3%
@HDL : # 2%
Cadence BlackTie : 1%

As we see, after about 5 years from introduction of commercial formal model checking tools, only 30% of verification engineers are using them.

There is also another posting from ESNUG:
http://www.deepchip.com/items/0430-08.html

where anon user complains about Synopsys inability to fit it's own formal verification tool into it's own verification flow.

It would be interesting to get more opinions on this topic.

Regards,
Alexander Gnusin

ncr · Posted: Fri Jul 30, 2004 2:19 am **Post subject:**

I have been using several of these tools for the past few years. In my opinion not
many of these tools are mature enough to be used on a large scale design.

-ncr

alexg · Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa

Design size is serious limitation, and formal tool vendors realize that. So, some of them present formal tools as a powerful verification means for block-level (not chip-level) verification, where design size is more affordable.
However, 70% of users still prefer to run verification without the formal tools. The reasons for that, IMHO, may be:
1. Difficulties to formulate assertions
2. Problems with setting and trusting block-level constraints, developed to prove block-level assertions
3. Design size: block-level size is still large for the formal tools
4. Block level verification is not really popular comparing to the chip-level one.
5. Dynamic verification, enhanced with assertions, stimilus randomization and functional coverage, is sufficient enough.

Is it correct?

-Alex

confused · Senior Joined: Jan 09, 2004 Posts: 185

daveola · Posted: Sun Aug 01, 2004 3:41 am **Post subject:**

alexg · Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa

confused · Senior Joined: Jan 09, 2004 Posts: 185

alexg · Senior Joined: Jan 07, 2004 Posts: 586 Location: Ottawa

Darren · Posted: Wed Aug 11, 2004 3:58 am **Post subject:**

Firstly, there is a problem with the statistics in the ESNUG report - it doesn't allow you to reply if you use something else. I use an in-house tool called GateProp which was originally developed by Siemens, and as formal tools go, it's excellent.

Formal verification is necessary for block level verification, and I believe that it compliments random verification very nicely, and I would refer you to a paper written by Mike Bartley, Tim Blackmore and myself, published at DAC 2002, which compares directed, random and formal approaches on a bus bridge. Yes, formal verification is constrained by the size of design it can handle, and the need to define a legal start state. We solved some of this by always starting from reset. This limited us to exploring the state within 15 cycles of reset, but this proved deep enough. The formal tool found the extreme corner cases which would have been very difficult to hit randomly (or simply taken a lot of simulation), and the random tool enabled us to find the easy bugs quickly to enable the formal tool to explore the design properly. If the random tool hadn't been used, the formal tool would have found the same bugs, and it often did, but usually with scenarios so bizarre that working out what was the root cause was often difficult. The random tool tended to find slightly simpler entry routes to the problem.

In addition, you can use the formal tool to prove that you have really fixed a bug found randomly. If a bug is found with the random tool, the designer changes the design to "fix" it. You re-run your random test with the same seed, and the test passes. Have you really fixed the bug, or have you moved the entry point to some other place? Have you fixed all of the entry points? If you can write a property to describe the bug, you can then use the formal tool to prove that you have fixed the bug in all cases.

Assertions
Assertions should be both black box and white box - not either/or. Assertions should be considered in 2 parts.

Black box - these should be written by verification engineers from reviewing the specification. The specification should describe all of the interfaces and interface behaviours, and it is this that the verification engineer should be hoping to check without recourse to the internals of the design.

White box - these should initially be written by the designer, and should aim to describe the intent behind what the designer has implemented. They should capture any assumptions that the designer has made (such as block x will always assert signal z after signal y), and any particularly complex areas of the design. These assertions help to increase the observability of the design during debug (if an assertion fires, it's a great way to pinpoint the failure with more exactness, rather than tracing back from the outputs, if the failure even makes it that far), and document assumptions that were made.

Once the initial test plan has been implemented, then the verification engineer can perhaps start developing white-box assertions to check the design based on the knowledge gained so far. However, performing white-box assertion verification before then could perhaps influence the verification engineer to test what has been implemented, rather than what was specified.

Assertions don't have to be written from scratch - you can re-use your formal environment at this point. To get the formal environment correct, you typically have to describe the legal behaviour which the formal environment can subject your DUT to. These are assumptions about the inputs. Each of these assumptions can be coded up as assertions within your design. This has additional benefits - not only do you get additional assertions to check your design, but you are also verifying the correctness of your formal environment.

This approach can be of particular benefit when testing modules which are particularly complex. It may be the case that you have to overconstrain the inputs of your module in order for the formal verification to be able to reach a sufficient state depth. In these cases, you can take the property you are using and code it as an assertion within your HDL, or within your random verification environment. You can then run the same property in the normal system. In this way we found bugs within the design which we couldn't hit in the formal tool (the state space had been reduced to make the problem manageable), but could randomly. In addition, the property pin-pointed the failure location - the failure took 100s of clock cycles to make it to the visible outputs of our processor, but the property immediately pin-pointed the interface at which the failure occurred.

Formal verification is NOT as difficult as people make out, and to a large extent I blame the EDA vendors themselves, and the conference circuit. At DAC, sessions on formal verification aren't really about formal verification - they are about the mathematical techniques used within the tools themselves. You don't need to know this. After all, you don't need to understand the optimisation techniques used within your simulator in order to use it. You don't need a PHD in mathematics either - I don't have one. The languages used by the tools themselves are usally quite simple once learnt, and the best example I can give is when I used our inhouse tool for the first time. Our expert showed me the language, and how to construct a property. Within half an hour I had found my first bug within the design. Formal tools can be very easy to use - it is up to the vendors to make this clearer. Having people on DAC panels (as at DAC last year) saying that you need huge teams and one very smart person to use it does the field a huge disservice. On the block discussed in the paper mentioned above, we had a team of three. It worked wonderfully.

confused · Senior Joined: Jan 09, 2004 Posts: 185

Darren · Posted: Mon Aug 16, 2004 9:41 am **Post subject:**

Doing the formal verification isn't so difficult - it is the size of the problem you are trying to prove. The more state there is in a design, the more difficult it is to exhaustively prove everything. In the case I mentioned above where we took the property and used it dynamically, the extra couple of signals which were checked dynamically and were constrained in the formal environment were enough to cause the state space to explode.

There are ways around this. You can try to make your properties simpler and prove subsets, and then inherit the proof upwards. But not all things can be reduced this way. Secondly, you can define all of the legal states. This prevents the formal tool from starting in illegal states and then getting false positives, but is difficult to do for any design of moderate size. The Averant tool Solidify attempts to do this, and uses the illegal states it finds as a constraint, but the resulting proof speed wasn't any better than the tool we normally use which doesn't do this.

I don't believe we can yet rely on formal verification to fully verify blocks. However it is a useful addition to the verification armoury. You need to work out where it can be best applied given the cost/benefit of introducing it. We have found it extremely good at handling bus bridges, which have limited pipeline depths internally. It can be more difficult to apply to processor blocks. Mind you, the European Union has just sponsored a group to verify formally a processor to prove formal techniques, and they claim it can be done in two years. But then this team has experts in it who write the tools, so they are far better at it than I.........

tblackmore · Posted: Mon Aug 23, 2004 4:06 am **Post subject:**

I think it may be worth differentiating between formal verification and semi-formal verification.

Semi-formal verification (a.k.a. dynamic formal verification and amplified simulation, amongst other names no doubt) starts from a known state and proves a property holds for as many clock cyles as possible from this known state (the number of clock cycles being the proof-radius of the property). The start state can be the reset state, or it can be a state read in from a simulation trace. The proof-radius depends both on the complexity of the block and the complexity of the property - so it may be 15 cycles as Darren mentioned above for the most complex properties on complex designs, and it may be a good deal more. Also the capability of reading in states from simulations means that the bug does not have to be findable within 15 cycles from reset - although it would probably surprise people familiar with only simulation just how many bugs can be forced to become manifest within 15 cycles from reset by a formal tool.

Formal verification attempts to prove a property holds for all time. The most feasible way to do this is to start from a 'generic' start state. This then describes relationships between the inputs and registers of the design algebraically. Since currently available formal tools cannot determine all of these relationships for even a reasonably complex block it is normally necessary to do this manually. This makes the task much more difficult than semi-formal verification but it is still tractable. As Darren says a complete modern processor design is currently being formally verified, although I think the estimated time is something over three man years and the project is being sponsored by the German government. I wonder if this investment is suggestive of a difference in attitude towards fromal verification between Europe and the rest of the world, with Europe being ahead in this instance. A contentious viewpoint no doubt.

From my experience over the last four years, semi-formal verification is a powerful way to find bugs. It can be applied to any block whose interfaces are understood (and preferably documented) - whether these interfaces are standard busses or an internal interface in a processor. It is a relatively easy way into formal verification, although possibly requires a certain mindset to be utilised to its full potential (but does not require a Ph.D. in Maths). Formal verification is more than just a way to find bugs - it actually verifies rather than 'falsifies' a design. In the absence of formal engines capable of a full reachable state analysis of a design it is at present an 'assisted code review' and requires a good deal of mental effort. Idon't think that this is a good reason not to use it though.

confused · Senior Joined: Jan 09, 2004 Posts: 185

It seems safe to assume that all verification tools are helpful. It is also generally good to assume that the exhaustive verification of a modern design is not practical (though it might be different for some special projects). Even Intel only formally verifies some parts of its processors.

For small blocks, the "old fashioned" approach is to manually provide input waves for some typical scenarios and visually inspect the circiut behavior. Most RTL classes are probably still taught this way. These blocks can likely be exhaustive verified, but many managers do not have enough schedule time or tool budget for most of their engineers to do so. If such "old fashioned" simulation is not solid enough, more solid verification is done after integrating all blocks together.

For the whole chip or very big blocks, more serious verification is done with a testbench for each group of typical scenarios. Now, there is no way to exhautively verify the whole thing. Assertions / properties / semi-formal tools are all helpful. However, they hardly reduce any testbench / simulation work, and it is hard to tell how much assertion / property / semi-formal effort is enough. Therefore, these "new things" become just "above and beyond" or extra credits.

I wonder why the above situation would not become typical in the industry.

tblackmore · Posted: Tue Aug 24, 2004 3:51 am **Post subject:**

confused · Senior Joined: Jan 09, 2004 Posts: 185