Antecedent must be Sig1. When Ever sig1 asserted, I have to load the the content of register to local data_load available in property.
the content of register must not change until Sig2 asserted, If it changes Sig3 must be asserted.
If Sig3 is not asserted, There is an error.Property must fail.
So I wrote my assertion like below:
property data_change_chk;
logic [31:0] local_data;
disable iff(reset)
(rose(sig1),local_data=data_load) ##[1:$] /I need to code here to check the data is changed/ $rose(sig2) /not sure how to check sig3 asserted or not/;
endpropery
assert property((@posedge clk) data_change_chk);
I am not sure how to write this kind of complex assertion, But In my verification environment, To check this scenario, It is convenient to add assertion.
If data changes, do you care if sig2 is asserted? When exactly does sig3 need to be asserted if data changes.
What are planning to do with local_data? if you are just looking to know if data_load is changing/not changing there is $changed(data_load) and $stable(load_data)
In reply to Verif_Learner_SG:
The best way to approach the definition of a property is to specify the desired “good/expected behavior”. This is my take on your requirements.
module top;
bit clk,reset;
bit sig1,sig2,sig3;
int data_load;
always #5 clk=!clk;
// If new sig1 then data_load will be stable starting from the next clock
// until sig2. At sig2 data_load is changed in value and in the next cycle sig3==1
property p_with_sig2;
int v;
@(posedge clk) disable iff(reset)
($rose(sig1), v=data_load) |-> ##1 first_match(data_load==v[*1:$] ##1 sig2)
##0 data_load !=v ##1 sig3;
endproperty
ap_with_sig2: assert property (p_with_sig2);
// if data_load changes between Sig1 and Sig2 posedges,
// then Sig3 must get asserted within let's say 1 to 10 clocks
property p_with_no_sig2;
int v;
@(posedge clk) disable iff(reset)
($rose(sig1), v=data_load) ##1 (data_load!=v && !sig2)[->1] |-> ##[1:10] sig3;
endproperty
ap_with_no_sig2: assert property (p_with_no_sig2);
initial begin
$dumpfile("dump.vcd");
$dumpvars(0,tb);
#200 $finish;
end
endmodule
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
Here, I am expecting if data_load changed between sig1 and sig2, If Sig3 is not asserted, It is an error.
Actually, I have different checkers to check, whether sig2 is asserted or not after sig1 is asserted.
I added your code in eda-playground and found that even though data_load changed, sig2 asserted but even though sign3 was not asserted, It is not throwing an error.
Thank you for your time, I am sure it is quite challenging to match the spec while reading my spec description.
Let me try to see while changing your property or other suggested implementation to achieve my check.
See (2) - EDA Playground
That seems to satisfy your requirement.
I added the pass1 and err1 signals used in the action block to help in the debugging and display. I also modified the range for sig3 for simplicity.
**($rose(sig1), v=data_load) ##1 (data_load!=v[=>1] intersect sig2[->1]) |->
##[1:5] sig3;
**
// Code your testbench here
// or browse Examples
module top;
bit clk,reset;
bit sig1,sig2,sig3;
int data_load=0, pass1, pass2, err1, err2;
always #5 clk=!clk;
// If new sig1 then data_load will be stable starting from the next clock
// until sig2. At sig2 data_load is changed in value and in the next cycle sig3==1
/*property p_with_sig2;
int v;
@(posedge clk) disable iff(reset)
($rose(sig1), v=data_load) |-> ##1 first_match(data_load==v[*1:$] ##1 sig2)
##0 data_load !=v ##1 sig3;
endproperty
ap_with_sig2: assert property (p_with_sig2);*/
// if data_load changes between Sig1 and Sig2 posedges,
// then Sig3 must get asserted within let's say 1 to 10 clocks
property p_with_no_sig2;
int v;
@(posedge clk) disable iff(reset)
//($rose(sig1), v=data_load) ##1 (data_load!=v[->1] intersect sig2[->1]) |->
// shOULD BE [=1]
($rose(sig1), v=data_load) ##1 (data_load!=v[=1] intersect sig2[->1]) |->
##[1:5] sig3;
endproperty
ap_with_no_sig2: assert property (p_with_no_sig2) pass1=pass1+1; else err1=err1+1;
initial begin
$dumpfile("dump.vcd");
$dumpvars(0);
#200 $finish;
end
initial begin
fork
#7 sig1<=1;
#23 sig2<=1;
#18 data_load<=10;
// #26 sig3<=1;
join
end
endmodule
Check1: Once after sig1 asserted If data_load is changed before sig2 asserts then If sig3 is not asserted.Assertion pass condition.
Check2: Once after sig1 is asserted, If data_load is changed,sig2 is not asserted then If sig3 asserted. It shows as vacuous success.
Check3: Once after sig1 is asserted, If data_load is changed,sig2 is not asserted then If sig3 not asserted. Here assertion is not exercised for complete check. No pass or fail.
My code is at below link:
Waveform’s for my checks:
Available code in EDA_playground.
I tried to modify but It’s not checkking check3 as above.I used the within construct as well.
Check1: Once after sig1 asserted If data_load is changed before sig2 asserts then If sig3 is not asserted.Assertion pass condition.
// Check1: Once after sig1 asserted, if data_load is changed before sig2
// asserts then If sig3 is not asserted in 1 cycle the assertion passes
property p_check1;
int v;
@(posedge clk) disable iff(reset)
($rose(sig1), v=data_load) ##1
(data_load!=v && !sig2)[->1] |-> ##1 !sig3;
endproperty
ap_check1: assert property (p_check1) pass1=pass1+1; else err1=err1+1;
Check2: Once after sig1 is asserted, If data_load is changed,sig2 is not asserted then If sig3 asserted. It shows as vacuous success.
In assertions, you write an assertion to check that a property is true or never true.
You do not write property to check if it is vacuous.
Check3: Once after sig1 is asserted, If data_load is changed,sig2 is not asserted then If sig3 not asserted. Here assertion is not exercised for complete check. No pass or fail.
In assertions, you write an assertion to check that a property is true or never true.
You do not write property to check if it is vacuous.
