I have written the below assertion in which I want to a reset a bit when the signal named write_cycle goes high.
But the issue is that the bit is getting reset at the next positive edge of the clock and not on the same edge on which the signal write_cycle goes high. The subroutine reset_match_found() resets the bit.
You cannot know that write_cycle has risen until after the clock edge has passed in an assertion. There’s no way to go back in time to set match_found.
You need to explain what you are attempting to accomplish with match_found before anyone can suggest a workaround.
The match_found bit should be set whenever a first match occurs depending upon the comparison statement in the consequent expression. The bit should be reset again when a write_cycle is detected. This is the behaviour that I want. The match_found bit is used to check that the comparison statement that was used inside the first_match() remains valid as long as next write_cycle is detected. That bit is used in an always_comb procedural block.
Your function changes the value of your variable in the Observed region, way past the Preponed region where the signals are sampled.
I didn’t understand your last explanation.
Ben systemverilog.us
You cannot use an assertion for this. Assertions are meant to be passive and mot modify signals going back into your design. Your explanation is still not clear enough to know what you plan to do with the match_found bit. How is an alaways_comb involved with clock cycles??
I agree with Dave in that assertions are meant to be passive and not modify design signals.
However, SVA can be used to modify support verification variables.
I went through the discussion in the threads. Understood that the $rose(write_cycle) is being sampled in the preponed region and evaluated in the observed region, hence the behaviour. I am not trying to modify any DUT signal in the assertion. match_found is Not a DUT signal but a verification support signal whose scope is limited to the checker block in which the assertion is written. Actually the entire code is written inside a checker block. Extremely sorry for not being able to convey my intent clearly. Below is my intent.
Bit write_cycle goes HIGH whenever an APB write cycle is detected. When a write_cycle is detected, within 0 to 2 APB clocks first match occurs according to the comparison statement written inside first_match() construct. So when the first match occurs a bit match_found is set HIGH. This match_found bit remains HIGH until the next write_cycle is detected. On detection of a write_cyle the match_found is reset. Also this match_found bit is used in a always_comb to check that comparison which was written inside the first_match() remains valid until the next write_cycle is detected.
The intent of using an always_comb block is to ensure the comparison happens independent of any clock.
You have a clocked system. There is NO treason to have a continuous check between clocking events.
// Check that comparison which was written inside the first_match()
// remains valid until the next write_cycle is detected
ap_found_compare: assert property(@ (posedge clk)
(match_found) |-> comparision_statemen );
I understood your point and I definitely agree with it. But the issue is that in my project there are multiple clock domains that are being used. There are internal registers that are written via the APB interface. There is one to one mapping of those registers with RTL’s output signals. The output is sampled at a clock which runs at a much higher frequency than that of the APB. So the issue is that if there is some glitch sampled by the RTL at that high frequency clock, I fear that the assertion wont be able to catch it. Hence to make it fool proof I am using the always_comb block for the data check.
So the issue is that if there is some glitch sampled by the RTL at that high frequency clock, I fear that the assertion wont be able to catch it. Hence to make it fool proof I am using the always_comb block for the data check.
I don’t see how the always_comb prevents any glitch in the signal from triggering a false error. Maybe I am missing something here. SVA allows for multiclocking. For example:
In your testbench environment you could construct a safe clk2 to do your sampling of the comparision_statement. That build of clk2 could be combinational logic, or simply a delayed (e.g., # 2ns) off a known clock.
an always_comb triggers at every change of signals in the block, including glitches.
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr
Basically I want that when the bit write_cycle goes high, the check should begin when the first match occurs and should continue till the next rise of the bit write_cycle.
To check the assertion I forced “signal_to_check” to be zero. Still the assertion passes. Seems to be a vacuous pass. What could be the reason here?
you don’t need the |-> after the 1st rose because if there is no match then the assertion is vacuous.
##[1:5] first_match(expr) is same as
##[1:5] expr because expr sequence is of one cycle.
Actually it is ##1 first_match(expr) or ##2 first_match(expr) or…
Whereas first_match(##[1:5] expr) picks the 1st match of the sequence (##[1:5] expr)
Thus, it picks the first_match of the sequence
##1 expr or ##2 expr or… ##5 expr.
Ended up with Assertion errors at every point of time. Why does it happen? Also I need some fundamental understanding regarding the working of |-> , ##0 and #-#. Is there any relevant article for this? That shall be of great help for me.
You really need to understand vacuity in SVA. Of course,my book explains all these concepts and operators with lots of examples. If you are in India,
contact Home - My cvcblr for a better price.
You can also study 1800’2017 and do searches on Sva, there are many articles and training sites.
If you understand the fork join_any and tasks, then you’ll understand the modeling of an assertion, including the concept of antecedent / consequent and why you have errors without the implication operator.
Ben Ben@systemverilog.us
In reply to ben@SystemVerilog.us:
// another option
property data_check;
@(clk) @rose(write_cycle) |->
first_match(##[1:5] signal_to_check == write_data) ##1
((signal_to_check == write_data)[*1:$] ##1 $rose(write_cycle));
endproperty
Ben systemverilog.us
Hi Ben,
I intentionally rewrote the assertion as below:
property data_check;
@(clk) @rose(write_cycle) |->
first_match(##[1:5] signal_to_check == write_data) |->
((signal_to_check == write_data) until $rose(write_cycle));
endproperty
**initial $assertvacuousoff(0);**
**assert property (data_check) $display ("Assertion Pass") else $error();**
**and forced the "signal_to_check" to 0** in the testcase. Now this is a case of vacuous success and the pass block should have been turned off. But still the pass block remains on. Why this kind of behaviour?
In reply to ben@SystemVerilog.us:
To avoid vacuity after the rise of the write, use the followed-by operator that represents a sequence followed by a property
But the pass statement is not showing up on each and every clock edge at which the assertion passes. Instead it shows up only once. Dont know the reason for this.
and forced the “signal_to_check” to 0 in the testcase. Now this is a case of vacuous success and the pass block should have been turned off. But still the pass block remains on. Why this kind of behaviour?
In simulation the PASS action block is not displayed, even with the $assertvacuousoff(0); commented out. Users do not want the pass action block on vacuity. I believe that tools autmatically set a switch to do that. If the use of $assertvacuousoff(0); does not turn off the pass acton on vacuity, you’ll need to contact your vendor.
But the pass statement is not showing up on each and every clock edge at which the assertion passes. Instead it shows up only once. Dont know the reason for this.