Techfocus Media :: Formal Verification

Viewing 1 to 4 (4 Total) Formal Verification
zyad_hassan Total Posts: 2 Joined: Dec 2009	Formal verification has emerged as a promising technique for verifying designs. It has been proposed as an alternative to design simulation, which is showing a decreased effectiveness with the increased design sizes, due to the prohibitively long simulation times required to test the full input-pattern space. Model checking, one of the approaches of formal verification, is a mathematical approach that is able to prove that a design satisfies certain properties. Model checking is being gradually adopted into the commercial IC design flow with many companies now using a mix between formal and simulation (non-formal) methods to verify their designs. Currently, model checking is not capable of verifying large designs due to its high complexity. People have different views of formal verification. Some have hopes of it replacing traditional simulation-based verification techniques in the future, while others are skeptic about its ability to handle large designs, and are against investing in formal verification techniques. It would be useful to have people's insight about this topic. The topic is open for discussion. Give your opinion, whether you believe formal verification is going to fly in the future, and whether you would be pro/against adopting it into your company. Posted on 2009-12-14 17:26:52 at 2009-12-14 17:26:52
Display Messages: Threaded Flat 3 Replies
bmoyer Total Posts: 38 Joined: Dec 2009	Stealth-mode formal? I'll add one point to this: while in the past formal was simply a verification technology, now it's being used for very specific kinds of verification (like constraint verification), and the user may or may not know that formal is under the hood. Might formal be more successful out of the spotlight than in it? Posted on 2009-12-22 20:08:27 at 2009-12-22 20:08:27
zyad_hassan Total Posts: 2 Joined: Dec 2009	Model Checking Might formal be more successful out of the spotlight than in it? In most cases, yes. Dealing with formal is not as easy as dealing with non-formal, and thus it's usually better to hide the formal details from the designer. However, in some cases, such as with model checking, exposing the designer to the complexity of formal is a necessity. For example, designers are used to the traditional way of writing testbenches and simulating designs at the HDL-level to verify functionality, but this approach has shown to be unreliable (e.g. the Pentium floating-point bug). Using model checking, on the other hand, the design can be proved to satisfy certain properties, such as that two specific signals should never be high at the same time, or, if a signal is raised, then eventually another signal should be raised, and so on. However, to use this alternate reliable formal method approach, designers have to bear through the complexity of learning how to specify properties about their design in some formal specification language. In addition, they have to be aware in the first place of what properties should be present in their design. Unfortunately, formal verification is currently incapable of handling large designs, and companies therefore either use traditional simulation methods, or semi-formal approaches, which combines both formal and simulation. What I'm hoping to achieve from this post, is to get a general idea of what people working in IC design think about formal verification. Do they believe formal techniques would, in the near future, be able to handle the design sizes they're targeting, and thus they're willing to invest time, effort and money to learn how formal techniques can be applied in their designs? Or do they believe this is not worth it; traditional simulation well-meets their needs? Posted on 2009-12-23 07:07:57 at 2009-12-23 07:07:57
Cliff Total Posts: 21 Joined: Dec 2009	Simulation and formal methods in cahoots! I think it's a mistake to think of formal methods as a simulation replacement. To say it as a sound byte, simulations show your design works, formal methods show your design doesn't not work. While these two may sound much the same, they are not. Just because you have all the facts right, doesn't mean you come to the correct conclusion. Formal methods show all the rules are followed, but that doesn't mean the packet comes out the other side properly modified. Admittedly, that's a little obtuse, but I hope you can see my point. Furthermore, formal methods tend to verify the correctness of the parts of the design that we already know are correct; that is for example, the interactions we can think to formally verify are parts we know will produce the correct results anyway. It's the interactions we aren't thinking of where the bugs scurry about. Still, formal has its place, and so does simulation. They are best eaten as chocolate and peanut butter. They each serve a purpose and can also be a nice combination, but neither will supplant the other. Just my opinion at this particular moment. Cliff Posted on 2010-01-09 21:59:38 at 2010-01-09 21:59:38