How can you allow an SVA occur only once before checking again?
If I have assertion A and it takes 5 clocks to check, how can I make sure that during those 5 clocks assertion A will not get trigged?
In reply to VerifEx:
How can you allow an SVA occur only once before checking again?
If I have assertion A and it takes 5 clocks to check, how can I make sure that during those 5 clocks assertion A will not get trigged?
The following code is a slight variation from my “dictionary” of assertions chapter in my SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
The idea is to set a flag in the antecedent when the property is triggered. At the end of the assertion, with a pass or a fail, the flag is reset. You can decide if you want to reset that flag if the assertion fails; that depends upon your requirements. In this example, I have 2 assertions: ! to check that if sof, then within 5 clocks you get eof. The other detects that during that time no other sof is initiated. BTW, that 1st assertion wil not retrigger because of that flag (the busy_sof).
module thruout2;// /ch10/10.27/thruout2.sv
bit clk, sof, eof;
bit busy_sof;
default clocking @(posedge clk); endclocking
function void setval4busy(bit d);
busy_sof=d;
endfunction
// This is not catching multiple sof's and one eof within valid.
// It should check that for one sof, there should be only one eof.
ap_sof_eof: assert property(
// Once antecedent fires, no other one will fire again
(sof && busy_sof==1'b0, setval4busy(1'b1)) |->
##[1:5] (eof)) setval4busy(1'b0); // reset flag if property is true
else setval4busy(1'b0); // reset flag if property is false
ap_neversof_when_busy: assert property(not(sof && busy_sof));
endmodule
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
Hi Ben,
Suppose i need to trigger only when the ancedent is true .
suppose i have [3:0] a,
i need to trigger if it’s value is 'h8 and then wait for 30 to 32 clk edge to see if it’s value changes to 9 and then again see after 16 to 18 clock edge it value changes to a .
How can I do it if i only needs it to get triggered after it’s value to 8 but i donot want to triggered at all edges of clock i only needs at some that particular edge of clock
property check
@(posedge clk) a=='h 8|->##[30:32]a=='h9|->##[16:18]a=='ha;
end property
a:assert property (check);
In reply to bhajanpreetsinght:
If after you see a=='h 8 you want to lock out seeing another a=='h 8, then use the approach I previously showed.
I don’t particularly like multiple antecedents. It would be best if you wrote it as:
@(posedge clk) a=='h8 ##[30:32]a=='h9 |->##[16:18] a=='ha;
Hi Ben,
Thabks for the reply.I would like your expertise and help here in understanding
I found it hard to understand you approach can you please guide here
Improvising with my question and using your approach
I have three bit [3:0] a;
how to use it please let me know
i am replacing d with a
I understand your clock use ,
I am not clear why you use sof ,eof and how you control them.Suppose in my case i have only variable a[3:0] ;I need to check it value from ’ h8->'h9->'ha->'hb->'hf. All should be check after as and between after we get 'h8 we should get ’ h9 after 30:32 edge of clock, similarly 'ha after 20 to 26 ,'hb to get after 9-10 clock edge and then 'hf after 3-4 clock edge.
But the cache and additional requirement is that once we get 'h8 in first place at any posedge of clk the assertion should not trigger at all edge but it should wait and only triggered at specific edge as you mentioned.
I have tried to write the code using your reference can you help me correct it if you it wrong.
module thruout2;// /ch10/10.27/thruout2.sv
bit clk, sof, [3:0] eof;
bit [3:0] busy_sof;
default clocking @(posedge clk); endclocking
function void setval4busy(bit [3:0] a);
busy_sof=a;
endfunction
// This is not catching multiple sof's and one eof within valid.
// It should check that for one sof, there should be only one eof.
ap_sof_eof: assert property(
// Once antecedent fires, no other one will fire again
(sof && busy_sof==' h8, setval4busy(1'b1)) |->
##[30:32] (busy_sof=='h9) setval4busy(1'b1)|-> ##[20:22] (busy_sof == ' ha) setval4busy(1'b1) |= > ## [7:8] (busy_sof == ' hb) setval4busy(1'b1) ; // reset flag if property is true
else setval4busy(1'b0); // reset flag if property is false
ap_neversof_when_busy: assert property(not(sof && busy_sof));
endmodule
In reply to bhajanpreetsinght:
The concept o “LOCKs” is well known; we do that in public restrooms!
If the LOCK-TAB==UNLOCKED, any attempt into the room is acceptable.
Once in the room, we turn the lock into LOCKED.
Any other attempt in a future timestamp is rejected.
Once we are done, we turn the knob back to UNLOCKED.
I am using this concept in my assertion. I declare
bit lock=0;
In my assertion, I first check the lock and a=='h8:
(!lock && a=='h8, // If true then the function call is executed
set_lock(1'b1
Once in the locked position, the already attempted assertion continues the checking.
All other attempts are rejected and processed as vacuous because (!lock && a=='h8)==0.
I complete the antecedent with the other terms. ##[30:32] (a=='h9)
##[20:26] (a == 'ha) ## [9:10] (a == 'hb)).
If the antecedent is true you continue to the consequent where you check the a='hf.
I used the first_match function in the antecedent because the antecedent has many possible matches. See my paper (link in my signature) about understanding the SVA Engine.
If the antecedent is false, the assertion is true vacuously.
Thus, the assertion may PASS vacuously or non-vacuously or may fail.
Regardless of its outcome, once done, we need to UNLOCK.
I do this with the pass and fail action block
// https://www.edaplayground.com/x/8KA8
/* I am not clear why you use lock ,eof and how you control them.Suppose in my case
i have only variable a[3:0] ;I need to check it value from ' h8->'h9->'ha->'hb->'hf.
All should be checked after as and between after we get 'h8 we should get ' h9
after 30:32 edge of clock, similarly 'ha after 20 to 26 ,
'hb to get after 9-10 clock edge and then 'hf after 3-4 clock edge.
But the cache and additional requirement is that once we get 'h8 in first place
at any posedge of clk the assertion should not trigger at all edge but it
should wait and only triggered at specific edge as you mentioned.
I have tried to write the code using your reference can you help me correct it if you it wrong.*/
module thruout2;// /ch10/10.27/thruout2.sv
bit clk, lock=0;
// i have only variable a[3:0] ;I need to check it value from ' h8->'h9->'ha->'hb->'hf.
bit[3:0] a;
default clocking @(posedge clk); endclocking
function void set_lock(bit v);
lock=v;
endfunction
// This is not catching multiple lock's and one eof within valid. ????
// It should check that for one lock, there should be only one eof.
ap_lock_eof: assert property(first_match(
// Once antecedent fires, no other one will fire again
(!lock && a=='h8, set_lock(1'b1)) // if unlocked and a==8 the lock
##[30:32] (a=='h9)
##[20:26] (a == 'ha) ## [9:10] (a == 'hb)) |->
##[3:4] (a=='hF))
set_lock(0); else set_lock(0); // reset flag if property is false
ap_neverlock_when_busy: assert property(not(lock && a=='h8));
endmodule
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Cohen_Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to ben@SystemVerilog.us:
I would move the |-> after the a='h8 and remove the first_match.
This way the sequence that follows the first a=='h8 is necessary for verification
ap_lock_eof: assert property(
// Once antecedent fires, no other one will fire again
(!lock && a=='h8, set_lock(1'b1) |-> // if unlocked and a==8 the lock
##[30:32] (a=='h9)
##[20:26] (a == 'ha) ## [9:10] (a == 'hb))
##[3:4] (a=='hF))
set_lock(0); else set_lock(0); // reset flag if property is false
Ben
In reply to ben@SystemVerilog.us:
Hi Ben,
As checked and verified it’s show error
as the ## is able to detect transition and value but as value changes from 8 to 9 and 9to b it takes the leaft antecedent as one all together.and at every transition it shows athe same rather than taking it individually.
i thi k we have to use different properties to check.
please give your thoughts
module thruout2;// /ch10/10.27/thruout2.sv
bit clk, lock=0;
// i have only variable a[3:0] ;I need to check it value from ’ h8->'h9->'ha->'hb->'hf.
bit[3:0] a;
default clocking @(posedge clk); endclocking
function void set_lock(bit v);
lock=v;
endfunction
// This is not catching multiple lock’s and one eof within valid. ???
// It should check that for one lock, there should be only one eof.
ap_lock_eof: assert property(first_match(
// Once antecedent fires, no other one will fire again
(!lock && a=='h8, set_lock(1’b1)) // if unlocked and a==8 the lock
##[30:32] (a=='h9)
##[20:26] (a == 'ha) ## [9:10] (a == 'hb)) |->
##[3:4] (a=='hF))
set_lock(0); else set_lock(0); // reset flag if property is false
ap_neverlock_when_busy: assert property(not(lock && a=='h8));
endmodule
In reply to bhajanpreetsinght:
to clarify (!lock && a=='h8, set_lock(1’b1)) // if unlocked and a==8 the lock
##[30:32] (a=='h9)
##[20:26] (a == 'ha) ## [9:10] (a == 'hb)) |->
##[3:4] (a=='hF))
set_lock(0)
suppose at 12716 clock edge shows 8->9 it shows in annotation as 8->9 for all the expression on left side which is (!lock && a=='h8, set_lock(1’b1)) // if unlocked and a==8 the lock
##[30:32] (a=='h9)
##[20:26] (a == 'ha) ## [9:10] (a == 'hb))
similarly at 606 to 660 is shows 9->b
and same way so the assertions doesn’t gets triggered as at last it shows a->9 but right side is not triggered nor is lock changed to 0
In reply to bhajanpreetsinght:
I can’t follow your simulation.
However, this assertion says
ap_lock_eof: assert property(
// Once antecedent fires, no other one will fire again
// If (!lock && a=='h8) the set the lock and compute the consequent.
(!lock && a=='h8, set_lock(1'b1) |-> // if unlocked and a==8 the lock
// If in cycle 40, 31, or 32 after a matched antecedent a==9, you continue
// the evaluation. Else the assertion fails
##[30:32] (a=='h9) // same thing for this sequence
##[20:26] (a == 'ha)
## [9:10] (a == 'hb))
##[3:4] (a=='hF))
// you then reset the lock or a pass or a fail
set_lock(0); else set_lock(0); // reset flag if property is false
In reply to ben@SystemVerilog.us:
In reply to bhajanpreetsinght:
I can’t follow your simulation.
However, this assertion says
ap_lock_eof: assert property(
// Once antecedent fires, no other one will fire again
// If (!lock && a=='h8) the set the lock and compute the consequent.
(!lock && a=='h8, set_lock(1'b1) |-> // if unlocked and a==8 the lock
// If in cycle 40, 31, or 32 after a matched antecedent a==9, you continue
// the evaluation. Else the assertion fails
##[30:32] (a=='h9) // same thing for this sequence
##[20:26] (a == 'ha)
## [9:10] (a == 'hb))
##[3:4] (a=='hF))
// you then reset the lock or a pass or a fail
set_lock(0); else set_lock(0); // reset flag if property is false
let me take this example ,here in simulation checks for 8 and lock value and make lock value to 1.
but when the clock reaches 30 to 32 is shows a value as 8->9
in all value on left side which means and then when clock reaches another 20 to 26 clock edges i see again the value of a showing 9->a and then similarly after 9 and in between 9 to 10 edges when value changes a->b and then 3 to 4 clock edge it changes value to b->f after 3 to 4 clock edge
the problem is lock value is not changing to zero ,neither it shows pass nor it shows fail.Can you please suggest how to see the assertion is pass or fail.as i see simulation it show not attempted
In reply to bhajanpreetsinght:
If in any cycle of the consequent you want to unlock then use the sequence_match_item:
It has to be done before the a=='h8
for example … ##[30:32] (a == 'h9, set_lock(0))
I thought that the complete sequence had to be locked.
You should see a pass or a failure.
Do a test with a shorter consequent. The antecedent is
(!lock && a=='h8, set_lock(1’b1) |->
Perhaps you do not need the lock since at every a=='h8 you want to start a new thread?
// everytime a=='h8 then unlock
ap_lock_eof: assert property(
// Once antecedent fires, no other one will fire again
// If (!lock && a=='h8) the set the lock and compute the consequent.
(!lock && a=='h8, set_lock(1'b1) |-> // if unlocked and a==8 the lock
// If in cycle 40, 31, or 32 after a matched antecedent a==9, you continue
// the evaluation. Else the assertion fails
##[30:32] (a=='h9, set_lock(0)) // <<< UNLOCK HERE <<<<<<<<<<<
##[20:26] (a == 'ha)
## [9:10] (a == 'hb))
##[3:4] (a=='hF))
// you then reset the lock or a pass or a fail
set_lock(0); else set_lock(0); // reset flag if property is false
In reply to ben@SystemVerilog.us:
In reply to bhajanpreetsinght:
If in any cycle of the consequent you want to unlock then use the sequence_match_item:
It has to be done before the a=='h8
for example … ##[30:32] (a == 'h9, set_lock(0))
I thought that the complete sequence had to be locked.
You should see a pass or a failure.
Do a test with a shorter consequent. The antecedent is
(!lock && a=='h8, set_lock(1’b1) |->
Perhaps you do not need the lock since at every a=='h8 you want to start a new thread?
// everytime a=='h8 then unlock
ap_lock_eof: assert property(
// Once antecedent fires, no other one will fire again
// If (!lock && a=='h8) the set the lock and compute the consequent.
(!lock && a=='h8, set_lock(1'b1) |-> // if unlocked and a==8 the lock
// If in cycle 40, 31, or 32 after a matched antecedent a==9, you continue
// the evaluation. Else the assertion fails
##[30:32] (a=='h9, set_lock(0)) // <<< UNLOCK HERE <<<<<<<<<<<
##[20:26] (a == 'ha)
## [9:10] (a == 'hb))
##[3:4] (a=='hF))
// you then reset the lock or a pass or a fail
set_lock(0); else set_lock(0); // reset flag if property is false
I can try that but I wanted to ask our intention is correct to use lock when !lock && a == 'h8.
and indeed we need to check all antecedent as one that is 8-9-a-b-f and again to 9 ,but it should throw pass or fail only at lastb and atlast to 9
In reply to bhajanpreetsinght:
In reply to ben@SystemVerilog.us:
I can try that but I wanted to ask our intention is correct to use lock when !lock && a == 'h8.
and indeed we need to check all antecedent as one that is 8-9-a-b-f and again to 9 ,but it should throw pass or fail only at lastb and atlast to 9
In reply to bhajanpreetsinght:
There is a need to go back to the requirements.
MAybe all you need is a news a=='h8 with the use if $rose(a=='h8).
This looks you have an FSM. I would use the enumerated type.
Each enumeration can be attached to a specific value if you do not take the defaults.
Run a small test.
Ben
In reply to ben@SystemVerilog.us:
i need to check FSM THAT IS CORRECT.
SUPPOSE WE NEED TO CHECK FSM FROM 'h8->'h9-'hb->'hf->'ha->'h9
suppose the transition is happening after we get 'h8 and we need to after 12716 to 12718 value to 9 similarly to b at 20 to 30 edge and similarly to hf after 10 to 15 edge and then to ha after 5 clock edge and as a cycle we need to check at last 'h9 is coming just one clock edge [0:1] after 'ha->'hf
but the catch is we cannot afford to check at every clock edge that is why we used lock as suggested but it is not detecting lock =0 and consider all FSM value changing at all incedent value .
Can you please suggest the enumerated type codeusing this Ben
In reply to bhajanpreetsinght:
In reply to ben@SystemVerilog.us:
but the catch is we cannot afford to check at every clock edge that is why we used lock as suggested but it is not detecting lock =0 and consider all FSM value changing at all incedent value .
The lock just make all new attempts vacuous because the antecedent becomes zero.
The simulation does show pass and fail.
Checkout my papers, there is a lot of info about SVA.
The following example should make thing =s clear.
The “pass” “fail” signals are just for debugging.
module m;
enum integer {H0='h0, H8='h8, H9='h9, H10='h10} state;
bit clk, lock, pass, fail;
always #1 clk=!clk;
function automatic void set_lock(bit v, int p);
lock=v;
if(p==1) pass=1; else if(p==0) fail=1;
endfunction
ap_lock_eof: assert property(@(posedge clk)
(!lock && state==H8, set_lock(1'b1, 2)) |-> // if unlocked and a==8 the lock
##[1:2] state==H9 ##[1:2] state == H8 ##1 state==H10)
set_lock(0,1); else set_lock(0,0); // reset flag if property is false
initial begin
$dumpfile("dump.vcd"); $dumpvars;
@(posedge clk) state <= H8;
@(posedge clk) state <= H9;
@(posedge clk) state <= H8;
@(posedge clk) state <= H10;
@(posedge clk) state <= H0;
@(posedge clk) state <= H8;
@(posedge clk) state <= H9;
@(posedge clk) state <= H8;
@(posedge clk) state <= H8;
@(posedge clk) state <= H0;
#20 ; $finish();
end
endmodule
Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
or Links_to_papers_books - Google Docs
Getting started with verification with SystemVerilog
In reply to ben@SystemVerilog.us:
bit lock = 0;
bit [3:0] FSM;
default clocking @(posedge clk);
endclocking
function bit set_lock(bit v);
lock = v;
endfunction
property big_transition;
@(posedge clk)
disable iff(lock)
(lane0_lasm == 'h8) |->
(set_lock(1’b1) ##1 (FSM == 'h9)) ##[12716:12718]
(set_lock(1’b0) ##1 (FSM == 'hb)) ##[60:66]
(set_lock(1’b0) ##1 (FSM == 'hf)) ##[13:14]
(set_lock(1’b0) ##1 (FSM == 'ha)) ##[7:8]
(set_lock(1’b0) ##1 (FSM == 'h9)) ;
endproperty
transition:assert property (big_transition)
else
`uvm_error(“assertions failed”, $psprintf(“Big transition failed”))
here the observation in simulation once the lock is set to 1 it doesnot go to zero even if we try this ,please suggest and assertion as whole doesnot trigger false or true at any clock edge .
moreover if i take your suggestion and try to replicate, i cannot use module as i am trying to do in a interface.
enum integer {H0='h0, H8='h8, H9='h9, H10='h10,H11='h11,H15='hf} state;
bit lock = 0;
default clocking @(posedge clk);
endclocking
function automatic void set_lock(bit v, int p);
lock=v;
if(p==1) pass=1; else if(p==0) fail=1;
endfunction
ap_lock_eof: assert property(@(posedge clk)
(!lock && state==H8, set_lock(1’b1, 2)) |-> ##[12716:12718] state==H9 ##[60:66] state == H11 ##[13:14] state==H15 ##[7:8] state= H10 ##1 state=H9) set_lock(0,1); else set_lock(0,0);
this is your way ,
I donot think this below will be allowed in interface, i absolutely know this is only for showing and conceptual
initial begin
$dumpfile(“dump.vcd”); $dumpvars;
@(posedge clk) state <= H8;
@(posedge clk) state <= H9;
@(posedge clk) state <= H8;
@(posedge clk) state <= H10;
@(posedge clk) state <= H0;
@(posedge clk) state <= H8;
@(posedge clk) state <= H9;
@(posedge clk) state <= H8;
@(posedge clk) state <= H8;
@(posedge clk) state <= H0;
#20 ; $finish();
end
endmodule
as module is not allowed
so i wanted to confirm will this work,Ben
enum integer {H0='h0, H8='h8, H9='h9, H10='h10,H11='h11,H15='hf} state;
bit lock = 0;
default clocking @(posedge clk);
endclocking
function automatic void set_lock(bit v, int p);
lock=v;
if(p==1) pass=1; else if(p==0) fail=1;
endfunction
property big_transition;
@(posedge clk)
disable iff(lock)
(lane0_lasm == 'h8) |->
(set_lock(1’b0,1) ##1 (state == H9)) ##[12716:12718]
(set_lock(1’b0,1) ##1 (state == H11)) ##[60:66]
(set_lock(1’b0,1) ##1 (state == H15)) ##[13:14]
(set_lock(1’b0,1) ##1 (state == H10)) ##[7:8]
(set_lock(1’b0,1) ##1 (state == H9)) ;
endproperty
transition:assert property (big_transition)
else
`uvm_error(“assertions failed”, $psprintf(“Big transition failed”))
if any corrections is required please suggest,I request you to guide i am very close
In reply to bhajanpreetsinght:
I have no idea where this is coming from?
disable iff(lock)
(lane0_lasm == 'h8) |->
(set_lock(1'b1)
If this is your suggestion, then I recommend that you study the SVA syntax and the meaning of the disable iff.
I provided you with the methodology and examples to solve your assertion. The details are up to you.
From your model of verifying an FSM, it looks to me like you are using the wrong approach.
FSKs provide a way
to complete a service. For example, a traffic light controller (FSM) has inputs sensors and lights TO TURN on AND off for a duration. You check that based on inputs and conditions, the outputs are correct. The states of the FSM are not the things to check.
On this topic, I wish you the best Take from here.
Ben
In reply to ben@SystemVerilog.us:
In reply to bhajanpreetsinght:
If in any cycle of the consequent you want to unlock then use the sequence_match_item:
It has to be done before the a=='h8
for example … ##[30:32] (a == 'h9, set_lock(0))
I thought that the complete sequence had to be locked.
You should see a pass or a failure.
Do a test with a shorter consequent. The antecedent is
(!lock && a=='h8, set_lock(1’b1) |->
Perhaps you do not need the lock since at every a=='h8 you want to start a new thread?
// everytime a=='h8 then unlock
ap_lock_eof: assert property(
// Once antecedent fires, no other one will fire again
// If (!lock && a=='h8) the set the lock and compute the consequent.
(!lock && a=='h8, set_lock(1'b1) |-> // if unlocked and a==8 the lock
// If in cycle 40, 31, or 32 after a matched antecedent a==9, you continue
// the evaluation. Else the assertion fails
##[30:32] (a=='h9, set_lock(0)) // <<< UNLOCK HERE <<<<<<<<<<<
##[20:26] (a == 'ha)
## [9:10] (a == 'hb))
##[3:4] (a=='hF))
// you then reset the lock or a pass or a fail
set_lock(0); else set_lock(0); // reset flag if property is false
You are correct with respect to this reply we need to start a new thread at every a=='h8 a new thread so we donot need lock. But if we donot use lock and only use ancedent as
(a== 'h8) |-> ##[30:32] (a == 'h9) and so on will it not assert at every posedge of clk leading wrong assertion.
That was the reason we are trying lock concept in first place. But as a=='h8 comes and lock becomes 1 the consequent doesnot get triggered i have checked with shorter consequent with only
ap_lock_eof: assert property(
// Once antecedent fires, no other one will fire again
// If (!lock && a=='h8) the set the lock and compute the consequent.
(!lock && a=='h8, set_lock(1’b1) |-> // if unlocked and a==8 the lock
// If in cycle 40, 31, or 32 after a matched antecedent a==9, you continue
// the evaluation. Else the assertion fails
##[30:32] (a=='h9, set_lock(0)) ;
still lock doesnot becomes zero so how will one know the assertion actually gets triggered sir.
So needed your help