frame should go low within 2 to 5 clocks
a)frame_|->##[2:5] $fell(frame_)
b)s_eventually[2:5] $fell(frame_)
Does both the properties(a ,b) are same ? if yes then that is the importance of S_eventually operator apart from strong property.
request must be true until grant is true (non overlapping)
req until gnt; == req[*1:$]##1gnt; ?
request must be true until and including clock tick grant is true (overlapping)
req until_with gnt; == req[*1:$]##0gnt;?
If the above properties are correct then what is the importance of eventually,until,until_with operator.
Please guide me.
In reply to Mechanic:
I’ll take these questions as a teaching moment opportunity by asking you questions to reflect on the answers. You may use 1800’2017 and possibly a simulator to arrive at the answers you’ll learn more by digging through the language than for me to just feeding you the answers. Don’t take this as mean, but rather a teaching moment.
frame should go low within 2 to 5 clocks
a)frame_|->##[2:5] $fell(frame_)
b)s_eventually[2:5] $fell(frame_)
Does both the properties(a ,b) are same ? if yes then that is the importance of S_eventually operator apart from strong property.
what is the purpose of an antecedent?
what is the definition of the s_eventually?
Is it a sequence or a property?
what is the meaning of the “s_”
when is it desirable to define a consequent as “strong”?
request must be true until grant is true (non overlapping)
req until gnt; == req[*1:$]##1gnt; ?
what is the definition of the “until”?
request must be true until and including clock tick grant is true (overlapping)
req until_with gnt; == req[*1:$]##0gnt;?
look it up.
If the above properties are correct then what is the importance of eventually,until,until_with operator.
what is the purpose of an antecedent? Antecedent acts as an enabling condition for the assertion. In case of Implication operator (a|->b)if we dont get the enbling condition then we will end-up with vacuous pass.But in case of clock delay operator if the antecedent fails then the property will fail (a ##0 b).
what is the definition of the s_eventually?
Is it a sequence or a property? S_eventually [cyclle delay constant range] property_expression (strong form with unbounded range).
I am not clear with eventually definition.
what is the meaning of the “s_” It is a strong property operator which means if we run out of simulation tics then the property will fail
when is it desirable to define a consequent as “strong”? a|->##[1:$]b if b is not true until the end the simulation then the assertion wont fail.But if we use strong then the assertion will fail.
what is the definition of the “until”?
*A property “property_expression_1 until property_expression_2” (req until gnt)evaluates to true if and only if req must be true until gnt is true. req need not be true at the clock tick when gnt is true.
[quote]
Yes, SVA is rich in options i would like to know whether the above manipulated assertions for S_eventually and until are correct.
As for my understanding instead of walk-around with manipulated assertions we simply use the latest features that is the only advantage of the “eventually and until…nexttime…so onn…”.
what is the purpose of an antecedent?
*Antecedent acts as an enabling condition for the assertion. In case of Implication operator (a|->b)if we don’t get the enabling condition then we will end-up with vacuous pass.
True. The antecedent is a sequence of one or more terms.
But in case of clock delay operator if the antecedent fails then the property will fail (a ##0 b).*
In
ap: assert property(@ (posedge clk) (a ##0 b) );
there is NO antecedent. (a ##0 b) is a sequence. An assertion of a property that is a sequence can never be vacuous; its evaluation is either true or false.
what is the definition of the s_eventually?
Is it a sequence or a property? S_eventually [cyclle delay constant range] property_expression (strong form with unbounded range).
I am not clear with eventually definition.
1800 defines s_eventually as:
(s_eventually p) equivalent to (not (always(not p))
This means that it is NOT the case that the property p is always FALSE; it can be true. If I use the assert statement using the s_eventually property operator, then I am saying that there must be a case hen the property is true. See
If the property is a sequence then
req |-> s_eventually ack // equivalent to
req |-> strong(##[*0:$] ack) // Terminates or error if incomplete
req |-> s_eventually[1:5] ack // equivalent to
req |-> strong (##[1:5] ack)
It is used for formal verification.
]3) what is the meaning of the “s_” It is a strong property operator which means if we run out of simulation tics then the property will fail
when is it desirable to define a consequent as “strong”? a|->##[1:$]b if b is not true until the end the simulation then the assertion wont fail.But if we use strong then the assertion will fail.
Correct
what is the definition of the “until”?
*A property “property_expression_1 until property_expression_2” (req until gnt)evaluates to true if and only if req must be true until gnt is true. req need not be true at the clock tick when gnt is true.
correct
*
Yes, SVA is rich in options i would like to know whether the above manipulated assertions for S_eventually and until are correct.
As for my understanding instead of walk-around with manipulated assertions we simply use the latest features that is the only advantage of the “eventually and until…nexttime…so onn…”.
I would not call it the latest features. I see it as expressing assertions in more readable options. Many of these properties express safety and livneess. see slide 22 of
req until gnt; == req[*1:]##1gnt;? or req until gnt == req[*0:] ##1gnt?
This is the equivalent when the properties are sequences
req until gnt == req[*0:$] ##1 gnt
req until_with gnt; == req[*1:]##0gnt;? or req until_with gnt; == req[*0:]##0gnt?
I am bit confused in using [*1:] and [*0:] please let me know
(p until_with q) is equivalent to ((p until (p and q)).
Thus,
req until_with gnt; == req[*0:$] ##1 req && gnt
NOTE: a[*0:2] |-> b; // This is equivalent to
a[*0] or // a_sequence[*0] is called an empty match
a[*1] or a[*2] |=> (b ##1 c);
a[*0] is the empty match, it is not repeated, it does not exist. SVA defines the zero repetition
Also, a[*0] ##0 1 is equivalent to
empty_match ##0 1, and that results to zero (or empty).
enpty cannot be immediately followed at the same sample by anything, even true. It results in zero
a[*0] ##1 b is equivalent to b
could you please let me know is there any practical scenario where constraint random tests failed to catch the bug,But Assertions will help to find that bug in design.
In reply to ben@SystemVerilog.us:
Thanks Ben.
could you please let me know is there any practical scenario where constraint random tests failed to catch the bug,But Assertions will help to find that bug in design.
I don’t quite understand the question. Constrained-random tests is used to drive the DUT with various scenarios, but that can also be driven by directed tests. CRT is usually better as it covers scenarios that one may not have thought of, but you still need to control the constraints. Assertion addresses the verification aspects and has nothing to do with how the DUT is driven. SVA is one method to verify that the design meets the requirements. But there are other methods; for example, to assert that the DUT works correctly you can visually go cycle by cycle that it works. Don’t laugh, but in the early days, that was one of the methods, sometimes supported by RTL to flag errors. SVA is just a nation to express the requirements in a more readable manner; of course, it is processed by tools to do the checking. But one can use RTL to do what SVA does. I am working on a paper that actually shows how; it will be published soon.
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr