Hi All,
What assertion should be used in order to check that a Signal was NEVER HIGH or NEVER RISE during the whole simulation?
Thank you!
What assertion should be used in order to check that a Signal was NEVER HIGH or NEVER RISE during the whole simulation?
ap_xLOW: assert property(@(posedge clk)
not(x ||$rose(x));
// updated code
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 0-9705394-2-8
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
Thanks!
I meant I want to get a notification if the signal was never HIGH during the whole simulation.
As far as I understand, the assert property(@(posedge clk)(not(x))or(not($rose(x)))) issues a notification when the signal is HIGH/raised on any posedge clk;
Actually I need an assertion, which will issue a notification in the END of SIMULATION if the assertion’s condition was not fulfilled.
Thank you!
In reply to dmitryl:
First, I made an error in my original reply. the correct assertion with a message when the error occurs is
ap_xLOW: assert property(@(posedge clk)
not(x ||$rose(x)) else $display("error in signal x");
Now that is not what you really want. You want an assertion, which will issue a notification in the END of SIMULATION if the assertion’s condition was not fulfilled.
There are 2 answers, and both deal with the final. Keeping in mind that an assertion is a statement or directive that a given property is required to hold. A property is a collection of logical and temporal relationships between and among subordinate Boolean expressions, sequential expressions, and other properties that in aggregate represent a behavior. Thus, and assertion can be expressed in many ways, include plain code, instead of SVA. SVA is just a language to facilitate the expression of an assertion. In this case, code would be easier to write.
I am also using the procedure “final”; a final procedure executes when simulation ends due to an explicit or implicit call to $finish.
int x_glitched =0;
bit x; the signal that must stay at 0 the whole time
// Option 1
always @ (posedge clk)
if (x ||$rose(x)) x_glitched <= x_glitched + 1'b1;
// Option 2
ap_xLOW: assert property(@(posedge clk)
not(x ||$rose(x)) else x_glitched = x_glitched + 1'b1;
final
begin
if(x_glitched > 0)
$display("x has glitched %d times", x_glitched);
else $display("no glitch in x");
end
Ben,
My TestBench in VHDL. So, I end it not with Verilog’s $finish, but with the following VHDL statement: report “END OF SIMULATION” severity failure;.
So, will the final procedure work in this case? If it will not, what’s its equivalent for VHDL? How should I end VHDL simulation so that the final procedure will work there as well?
Thank you
In reply to dmitryl:
First, I prefer SystemVerilog over VHDL because it is a much richer language that supports, among other things, associative arrays, dynamic arrays, classes, constraint randomization of variables, RNG (random number generator) stability, see WWW.TESTBENCH.IN - Systemverilog Randomization , and UVM (or a UVM-like) verification environment. It also supports SVA, which I feel is better than PSL. Anyway, you are stuck with VHDL for now.
I have not kept up with the enhancements to VHDL, but they seem slow at being introduced and implemented. Thus, I don’t know if VHDL has a “final”; anyone knows? In any case, why don’t you do your check of (x_glitched > 0) just before you do your report “END OF SIMULATION” severity failure;?
You could use mixed-mode simulation with the testbench in SystemVerilog; however, that signal x has to be visible in the SystemVerilog world; I don’t believe (but I am not sure) if you can poke into a vhdl component from SystemVerilog; perhaps someone can shed light on this.
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
Thanks Ben! Will update you how will solve it in the VHDL env. Thanks again, you posted a very helpful solution!
First of all - the benefit of ABV is to catch errors early. Not sure why you would want to wait till end of sim to report the error. But I believe you have a reason, but do revisit that at your end.
Moving to the coding front, do you want PSL or SVA? Assuming SVA, you will anyway be using “bind” to bind the SVA module/interface to the VHDL entity. In that case, best is to add the “final block” into the SVA module itself. So Ben’s code snippet should work even in a Mixed language scenario.
VHDL does have an equivalent to $finish, env.finish; - strongly recommend you use that than the “severity” route (old approach).
Good Luck
Srini
www.verifworks.com
In reply to dmitryl:
Hi Ben,
Finally I took your advise and toggle some signal in my TB just before the simulation ends. I use this signal in the SVA module in order to perform end-of-simulation checks. Thanks!
Hello Everyone,
My apologies for revisiting this - I have a question that’s closely related to this so I figured I won’t open a new topic.
I want to ensure that a certain signal never goes high, just as Ben first assumed in this topic. In fact my property code is pretty much identical :
property check_encoder();
@(posedge byte_complete) disable iff (!stream_synchronised) not(dec_error || $rose(dec_error));
endproperty
Now, the issue is that I spotted that this is only checked once upon the enabling of the assertion (i.e. when stream_synchronised == 1) and it then goes to a “finnished” state and never transitions to “inactive”. Is this because the signal never changes? Can I rely on this?
Further, this issue lead me to revisit all my use of properties. Whilst most behaved as expected, some were exhibiting an odd behaviour. For example, the cover property:
property triggers_sent;
@(posedge CLK) (physics_event.triggered) |-> (send_trigger.triggered);
endproperty
cover property(triggers_sent);
Only gets triggered once and then disables itself (i.e. state goes to “off” rather than inactive) and does not count any of the other occurrences of the above sequence.
Since I am rather inexperienced at SVA, I’m guessing I am making a systematic error. Can someone please illuminate me? :)
Svet
On your Q1 - as such it should work, do you not see a failure if the “dec_error” goes HIGH (when the stream_synchronised == 1)? I presume you’ve an assert around this property.
A general comment on this property - you seem to be using the “disable iff” for “triggering condition” (antecedent).
property check_encoder();
@(posedge byte_complete) stream_synchronised |-> not(dec_error || $rose(dec_error));
endproperty
Also your clocking is little uncommon, though perfectly fine if this is what you want.
On your Q2 - it is tool specific optimization typically. Some tools turn off (internally) a cover once covered one time. There are tool options to disable that optimization. Check your tool doc and/or tell the tool options you use for more help.
On a coding guideline note again - avoid implication with cover as vacuous success might well be treated as “covered” (In SVA 2012 there are specific system tasks to turn them off, though your tool maynot support)
HTH
Srini
http://www.verifworks.com
ap_check_encoder: assert property(
@(posedge byte_complete) disable iff (!stream_synchronised)
not(dec_error || $rose(dec_error)));
Now, the issue is that I spotted that this is only checked once upon the enabling of the assertion (i.e. when stream_synchronised == 1) and it then goes to a “finnished” state and never transitions to “inactive”. Is this because the signal never changes? Can I rely on this?
when the assertion (assert property or cover property or assume property) is enabled, at every clocking event (posedge byte_complete)) the assertion is tested. If the assertion lasts one cycle (like this one), then if can only succeed or fail for that attempt. At the next clocking event, the assertion is retested.
If the assertion is temporal (lasting over multiple cycles, e.g., a ##1 |-> c) then if it has an implication operator and the first element (the “a”) is false, then the resulting assertion for that individual attempt is vacuous. Else, a new thread is started for that attempt. EVERY attempt, and its resulting thread and computation is INDEPENDENT from previous or future attempts. Thus, I don’t understand your statement: never transitions to “inactive”.
property triggers_sent;
@(posedge CLK) (physics_event.triggered) |-> (send_trigger.triggered);
endproperty
cover property(triggers_sent);
Only gets triggered once and then disables itself (i.e. state goes to “off” rather than inactive) and does not count any of the other occurrences of the above sequence.
Same story here for the attempts. Since you’re using .triggered, physics_event and send_trigger are sequences defined in sequence declarations. Srini answered the cover issue.
Ben SystemVerilog.us
In reply to Srini @ CVCblr.com:
Hi,
Firstly, thank you for the prompt reply.
I want to use “stream_synchronised” as a neg edge reset signal i.e. I believe I have the correct use (I can never be sure! :). The “dec_error” signal is all but certain to go high if my “stream_synchronised” signal goes low. However, I don’t want the assertion to produce an error in that case. I do want it to produce one if I dec_error == 1 whilst the stream_synchronised == 1.
As for clocking, I presume you refer to the lack of clocking block in that property - all other properties use a defined clocking but this is a slightly odd one.
Regarding the cover property - thanks for the tip and I will look into the documentation.
Thanks for you help!
Svet
In reply to ben@SystemVerilog.us:
Hi,
Firstly, thank you for your reply.
I may have confused you with my question but you certainly made things clearer for me. I somehow assumed that retests of the assertion would be marked on the waveform viewer (by an assertion state transition from finished/failed to inactive). I suppose this is not the case since the assertion is tested every clock AND it only lasts one clock. Weirdly, the coverage report also indicates that the assertion was only triggered once.
I will investigate the cover issue further.
Again, thank you for you reply.
Svet
In reply to ben@SystemVerilog.us:
Hi ben ,
what could be the assertion …to see that a signal was high throughout the simulation and if it goes low then there should be an error.
In reply to prashantk:
In reply to ben@SystemVerilog.us:
what could be the assertion …to see that a signal was high throughout the simulation and if it goes low then there should be an error.
assert final (sig) else $display("error message here"); // unclocked, constantly checked
//error message in the Postponed region
assert property (@(posedge clk) sig) else $display("error message here");
// Checked at posedge of clk
Ben
In reply to ben@SystemVerilog.us:
Thanks Ben for the reply.I was looking for first code snippet.(Not looking for the signal for every posedge).It should be constant throughout which the fist code snippet fulfills.
In reply to prashantk:
But the thing is final keyword is not compliant with 1800-2009 LRM so I used the later code.One more thing is I want my assertion to starts only after certain time stamp … Is there any way to do that ?.
The use case is that I am applying my assertion to a signal that rises in the initial , but its natural behavior starts from its second rising edge (so on…) , so I want to skip this signal’s first edge and apply my assertion throughout the simulation for all other edges of this signal , otherwise I am keep getting error for the first edge of this signal itself.
See the code below : -
$rose(signal[a]) && $rose(signal[b]) |-> $fell(signal[c]);
But the catch is …at the start of the simulation , after the reset is deserted …signal[a] and signal[b] rises simultaneously and at that time signal[c] doesn’t rise …but for the lateral edges this code works fine.(That is when edges of a and b are in sync.)
In reply to prashantk:
But the thing is final keyword is not compliant with 1800-2009 LRM so I used the later code.One more thing is I want my assertion to starts only after certain time stamp … Is there any way to do that ?.
SO your time stamp is $rose(signal[a]) && $rose(signal[b])
If that is your timestamp you can use something like.
initial begin :b1
wait($rose(signal[a]) && $rose(signal[b])); // waiting for the timestamp
// that timestamp can also be generation from an assertion action block or from a
// a function call from within a concurrent assertion in a sequence_match_item
// See below
//@(posedge clk); // another wait if that s what you want
forever assert #0 (sig) else $display("error message here"); // unclocked, constantly checked
//error message in the Reactive region
end : b1
// Other option
bit timestamp;
function void set_timestamp(int a);
timestamp=a;
endfunction : invert_auto
ap_gen_timestamp1: cover property(@(posedge clk)
($rose(signal[a]) && $rose(signal[b]), set_timestamp(1'b1) ) );
// Another option, you define that time region
// ap_gen_timestamp1: cover property(@(posedge clk)
$rose(signal[a]) && $rose(signal[b]) ##1 (1'b1, set_timestamp(1'b1)) );
initial begin :b1
wait (timestamp);
forever ...
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
- Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
- Component Design by Example ", 2001 ISBN 0-9705394-0-1
- VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
- VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115
In reply to ben@SystemVerilog.us:
Hi BEN actually these two signals “a” and “b” rises simultaneouly just after the reset , but at that time (where I dont want to apply my assertion) , but for every next time when their posedge are in sync I want to apply my assertion.
Actually the first time they are in sync does not rises signal “c” So I dont need an assertion for the first sync.