Urgent - Liveness of an assertion in Verification , Rulebase

[Vaibhav Singh]

Hi I need help with this question:

if i have an assertion

if a is true b is true eventually

My question is -- till what time will my Rulebase check this assertion and say if it passed or failed.That is for how many cycles will it check for this assertion to pass if a never became true.
Also please tell me what is the disadvantage of writing such assertions in formal verification when using a tool like Rulebase or System Verilog assertions.


Also please clarify - what does it mean when i say an assertion passed in a Formal Verification tool in terms how does it reach this conclusion and how many cycles or states does it take

Your help is greatly appreciated

 

[aji_vlsi]

Re: Urgent - Liveness of an assertion in Verification , Rule

Hi Vaibhav,
Liveness properties are checked by modelchecker such as Rulebase for "exhaustive" or "unbounded proof". But for large designs this may not be feaisble due to state space explosion and hence tools may provide a bounded proof wherein the "depth" maybe provided to you.

HTH
Ajeetha, CVC
Next SV course starting in Feb 09 end. See:
https://sv-verif.blogspot.com for details