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.
// property ::=
// if (expression_or_dist) property_expr1
//. else property_expr2
// **** following is illegal
// you have
A_property |-> b_property
// above is not a property.
// study the syntax and operators for properties & sequences
property data_check; // **** following is illegal
logic [15:0] temp_data1, temp_data2;
@(clk) (@rose(write_cycle),
if (condition1)
temp_data1 = //something
else if (condition2)
temp_data2 = //something
else
//something else
) |->
first_match(##[1:5] signal_to_check == write_data) ##1
((signal_to_check == write_data)[*1:$] ##1 $rose(write_cycle));
endproperty
I have the below assertion for signals that checks that the value of a signal corresponding to an address remains same until next write to the same address is detected:
Now we have some registers which appear as single registers but the can have 2 types of data namely FSP0 data and FSP1 data. On the top module this appears as an 8bit signal but it can either have FSP0 or FSP1 data. This selection is done by specifying the FSP from another register. Suppose we have an FSP0 data currently in the register but if I select FSP1, then immediately FSP1 data will appear on that 16 bit register. So I have modified the above assertion as shown below:
address1 and address2 are the addresses for FSP0 and FSP1 data respectively which can appear in signal_to_check_temp based on what is selected with the fsp_select register. But this assertion fails. As shown above I am trying to store the FSP0 and FSP1 data in local variables so that I can compare with them.
In reply to atanu.biswas:
I generally provide guidelines. Your issue is too specific for me to follow. I suggest that you discuss this with a colleague in your organization.
Ben