Abhishek Datta Blog

Re: Questions about IFV - PLS Help! - New to IFV

FormalGuy — Thu, 20 Nov 2008 16:52:46 GMT

Further, if you wanted the second term of the cover to be"nevermind" then you can write it like so -

s7: cover {INPUT1; true; INPUT2; current_state= 7} @(posedge clk);

Re: Questions about IFV - PLS Help! - New to IFV

FormalGuy — Thu, 20 Nov 2008 16:49:11 GMT

Hi Alexlop,

You might want to get in touch with your Cadence support person for some IFV help. IFV has good support and they should help you get started on your formal verfication adventure.

As far as your question goes - it looks like you are trying to shape a specific input stimulus through assumptions. This is a common mistake made by beginners who are familiar with simulation environments (I should know, I was one). Assumptions are used to inform the tool of the DUT's external environment - it is typically not a good idea to use assumptions to specify a directed input sequence like you are trying to do.

Now, I think your intent is to do some design exploration. This is good and a cool application of IFV. To do this sort of thing - setup assumptions on your design inputs that capture the protocols for those inputs. For instance, if your design uses an AHB interface, then write a set of AHB assumptions so that the tool considers only valid AHB input sequences.

Next, if you want to see if a specific sequence of events can occur, you write a cover statement like so -

coverS7: cover {INPUT1 ; !INPUT1 ; INPUT2 ; current_state = 7} @(posedge clk);

If this sequence is possible, within the set of assumptions on the design, then the tool will show you a trace demonstrating how this can happen. The nice thing about the trace is that if your inputs are not behaving as you (and the design) expect them to, then you can add more input assumptions. If it is not possible for the sequence to occur, then the tool will say that the cover Failed.

Finally, this is the right forum for this type of question and you should find an adequate level of support here. Let me know if this helped.

Formal Moment Of Zen

FormalGuy — Thu, 23 Oct 2008 08:00:00 GMT

Most of my experience in functional verification prior to my dabbling in FPV was in the area of SystemC/SCV and simulation acceleration. I naturally brought a simulation-mindset to FPV. As a matter of fact, it is possible to go far in FPV by thinking about the verification problem in procedural terms. Instead of writing BFMs and behavioral checkers, you write properties that each model a small portion of the environment, and together model the whole. You can almost imagine (wrongly, of course, as pointed out in my last post) FPV as some form of random simulation based on the PSL/SVA/OVL constraints.

It was a while before I realized that FPV might call for a whole different way of looking at the problem domain. My moment of zen was triggered by a piece of code that someone had sent me. It went something like this -

1.... module test ( );
2....
3....     ...
4....     wire        wen;
5....     wire        ren;
6....     wire [4:0] wdata;
7....     wire [4:0] rdata;
8....
9....     fifo i_fifo(clk, rst, wen, wdata, ren, rdata);
10..
11..     wire [4:0] data;
12..
13..     stability_constraint: assume property (
14..         @(posedge clk) disable iff(rst)
15..         data == $past(data)
16..     );
17..
18..     data_check: assert property (
19..         @(posedge clk) disable iff(rst)
20..         (wen && wdata == data) |-> ##[0:$] (ren && rdata == data)
21..     );
22..
23.. endmodule

The purpose of this piece of code was to check that the FIFO -

Did not corrupt data
Did not drop data

Lines 13-16, declare that the undriven wire "data" must always be equal to its value in the previous cycle. This "data" signal is then used in the assertion of the FIFO's data integrity in,

Lines 18-21, which express the assertion that -
Whenever we see a write into the FIFO, the same data must eventually be read out.

I spent a while trying to parse the assumption (13-16) and how it affected the assertion (18-21). My a-ha moment was the realization that,

the assumption "fixed" the current value of the "data" in terms of its value in the previous cycle,
but it said nothing about the initial value of "data" at i.e. at time 0, and
since the initial value of "data" is undefined and there are no other drivers on it, formal analysis has to consider all possible initial values for "data".

If you followed the discussion so far you would appreciate, as I did at the time, the perfectly cool way in which this achieved data enumeration by relying on the first principle of formal analysis - that it considers all possible states that are admitted by the constraints.

To elaborate this further, since the "data" value is un-initialized, the analysis will initialize it to all values between 0-31 and analyze the assertion for each. In pseudo-code the analysis might be represented by -

foreach i in (0 ... 31)
fork // Imagine each check is analyzed simultaneously
    data_check_i: assert property (
        @(posedge clk) disable iff(rst)
        (wen && wdata == i) |-> ##[0:$] (ren && rdata == i)
    )
join
endfor

It was the first time I really understood the significance of formal analysis considering all possible states within the set of constraints. Further, I was blown away by how concisely I could represent the data-integrity property of the FIFO that -

Could be rigorously proven using formal methods
Was immediately usable in the verification of most FIFO implementations

I have subsequently discovered other cool ways of expressing properties that are specific to FPV and are not completely intuitive to someone from a simulation background. But these patterns and idioms of FPV are intuitive once the mechanics of formal analysis are internalized. Frequently, all it requires is a single moment of zen.

Have you a formal moment of zen to share?

Top 5 Stumbling Blocks In FPV Adoption

FormalGuy — Thu, 16 Oct 2008 08:00:00 GMT

My first post served as a context for this blog. It also telegraphed my intention to set down a few reasons for the initial difficulties faced by long-time simulation users, specifically verification engineers, in applying formal property verification (FPV). Here is my Top-5 list in no particular order.

1. Procedural Versus Declarative Expression Of Intent

Simulation languages like Verilog, SystemC, e and the rest are procedural languages (blurring the lesser differences between OOP, AoP and procedural code). Simulation testbenches that model the verification environment are typically modeled using procedural code, though there is an increasing shift to declarative idioms with constraint specifications in sophisticated environments.

FPV environments on the other hand are almost completely declarative (PSL, SVA and OVL), whether they are assertions that state something about the design behavior or constraints that model the design environment.

I have found that, much like the procedural versus declarative debates in the AI community, the debate between FPV and simulation evangelists (the former in shorter supply) is ultimately irrelevant. I think there is increasing consensus that each has strengths that are complementary in most cases. The point remains that the two are distinct ways of thinking about verification problems and knowledge of one (idioms and patterns) does not always translate to the other.

2. If Not Simulation, Then What?

If only I had a penny for every discussion I have had about whether formal analysis is basically like an under-the-hood simulation within the set of constraints. While such a constraint-based simulation is definitely possible, FPV does not use simulation in converging assertions to proofs. Instead it relies on clever representations and algorithms to get mathematical proofs for the assertions about the design.

Considering that there are about a handful of people that can talk intelligently about the algorithms used in FPV, this watered-down answer does not satisfy an engineer in the trenches. This is in contrast to the simulation world where most engineers understand the mechanics of event-driven simulation and there is no notion of not converging to a desired result.

Verification engineers are paid to suspect and are properly suspicious of anything that is presented to them as black-magic. In cases where I have encountered this sort of thing, I like to point to that poster-child of formal methods - equivalency checking. Formal tools use algorithmic techniques to analyze a state transition only once, and can examine many state transitions simultaneously. Contrast this with simulation in which there are numerous repetitions of state transitions. It is in this sense that formal analysis increases coverage per unit time.

As in simulation, there is feedback from the analysis that allows the fine-tuning of the verification environment. Only, this feedback is different from that in simulation. It is a matter of training and application to get comfortable with any new technology and FPV is no exception.

3. The Capacity Issue

Simulation users make an implicit assumption about their environments - that they will scale with their design as long as they are able to crank the requisite number of simulation cycles. This is typically done by throwing more machines at the problem, or even relying on hardware accelerators for larger designs.

This is typically not true for FPV. Complexity in formal analysis is exponential in design size. Despite rapid strides in improved performance and capacity of formal engines, commercial FPV tools do not scale like simulation.

New users can get discouraged with FPV as a result. Almost every instance in which I have seen this happen, the problem has been the imbalance of design choice versus user experience. Choosing a target design (or function within a design) commensurate with the experience of the verification engineer is a critical component of successful FPV application. Which leads us to...

4. Inadequate Planning

Like simulation, FPV requires thorough planning to focus the verification effort. Unfortunately, it is common to encounter situations where FPV is applied without a set of clear goals. Perhaps this has to do with the economy of expression in property specification languages, that allows easy setup of an FPV environment. Be that as it may, experience shows that successful application of FPV, that justifies the investment, is deterministic only in the context of a verification plan.

A plan should address the following questions amongst others -

Can I split the design into functions and sub-functions?
Does the design have functions that are amenable to FPV?
What functions of the design do I intend to formally verify?
For each function, what are the assertions and constraints I require?
What functions in the design will not be verified with FPV, if any?
Am I looking for proofs, bounded proofs, bug-hunting or a mix of the three?

Note how the emphasis in the planning is not on describing coverage goals and test scenarios. Instead it is a hierarchical plan that decomposes the larger design problem into tractable sub-functions. Verification planning is an important topic in FPV and something that I plan to take up in future posts. I will only note that almost all FPV tools espouse a methodology that directly addresses planning.

5. Verification Closure

Most simulation users are familiar with the use of metrics such as line, expression, toggle and functional coverage. Unfortunately, there does not exist a comparable set of widely used and understood metrics for FPV. This is an area of active research and there are a bunch of ideas that look promising. But the truth is, the coverage metrics as traditionally understood by the simulation-savvy engineer do not translate very well to the FPV world.

Lacking a universally accepted coverage closure metric, FPV application tends to get tracked in terms of properties that have converged to proofs. Sometimes, a property may not converge to a proof. This can be frustrating to the verification engineer because there is no clear way in which the associated effort can be quantified in the project planning. In this sense, FPV almost becomes a hit/no-hit process that is so (correctly) abhorred by verification managers.

I think current notions of coverage, in the context of formal methods, can be considered in two dimensions -

Coverage metrics for pure formal analysis - some form of structural coverage or metrics for assertion completeness
Have formal methods contribute to simulation coverage

It is not a stretch of imagination to foresee a standard technology-independent notion of verification coverage emerging in the next few years.

In conclusion, the above is my Top-5 list of stumbling blocks in FPV adoption. There is a lot to be said about each of them and my intention is to delve further into each in future posts.

Please feel free to post your Top-5 in the comments section. I have done this exercise with those new and experienced in FPV and am almost always surprised by some of the things that get mentioned.

An informal introduction

FormalGuy — Fri, 03 Oct 2008 09:33:00 GMT

Formal verification can mean different things depending upon who you speak to. If I were blogging under Logic Design, it would probably indicate a series of loosely correlated opinions and observations on the topic of equivalency checking. However, this happens to be the Functional Verification forum and this blog about model-checking.

Model-checking: The process of checking whether a given structure is a model of a given logical formula. Or in engineer-speak, a way of automatically checking if your RTL implementation meets your design specification without a testbench.

Now that we have clearly and comprehensively established the technical context of this weekly bitstream, some disclaimers.

I am a self-confessed model-checking evangelist
It is my intention to convince you
- that model-checking might just be the most productivity-boosting tool you knew the least about
- that you do not need to be a formal methods PhD to apply it effectively
- that it is being used in the here and the now by your competition
- that it might just be the most intellectually satisfying verification experience
- that it will make you say at least once every morning - "How did it ever find that scenario?"

I will use facts, reasoning, dialog and weak puns like the title of this post, if necessary, to assimilate you

Next Week: Why simulation guys do not get model-checking.