CODEWITHSUNDEEP
system-verilogformal-verification
kkdev
kkdev

Reputation: 117

Significance of time taken to generate a cover

I am formally verifying a small module in a big design.

I have analyzed and elaborated the design(using Jaspergold -fpv).

I wrote a very simple cover property(SVA) as:

    cover_property1:cover property(@(posedge clk) $fell(signalA));

It takes around 5300 seconds to find the cover. I noticed that "Bound" is 143.

So why does this take so long to generate the cover and what does this signify(time taken and bound)?

Is it because the tool has to look deep into the design states to generate the cover and COI is large? Or some other reason?

Thanks for your help.

Upvotes: 2

Views: 212

Answers (2)

kkdev
kkdev

Reputation: 117

I found out the reason for long processing time to generate the cover. The reason for long delay is that the Formal engines try to (ideally) find the shortest path to match the particular cover/sequence. Hence, in many real scenarios the shortest path may not be the fastest for the formal engine. This is because, formal engine may have to toggle lots of flip-flops to reach that particular cover state.

In my particular case, a flip-flop by name 'scan_mode' was dependednt on several preceeding flip-flops. And, hence the tool had to flip lots of flip-flops to make 'scan_mode' asserted. Hence, an assume property on the flip-flop (1'b1) drastically reduced the cover generation time. Cover generation time without the assume property: 150seconds. Cover generation time with assume property: 2 seconds.

Upvotes: 1

Mithun Guddethota
Mithun Guddethota

Reputation: 56

Tries to get all scenarios which can end up with signalA de-asserting on rising edge of Clk & hence the time taken depending on COI

"Bound" indicates that all the combinations tried to hit de-asserting signalA are done in less than 143 Cycles.

Overall these signify in how many ways & how fast is the property hit.

Upvotes: 1

Related Questions