Hi,
I want to write the assertion for checking the priority. Here is the scenario:
I have two masters and 1 slave. For master_0 having signal sel_0,addr_0,write_0, For master_1 having signal sel_1,addr_1, write_0 and for slave signals are sel, addr, write.
when sel_0, sel_1,write_0,write_1 is getting high at same time it means both are trying to access. But slave will take 1 request at 1 time and it will take for master_0. That means after asserting of masters signal 2 to 10 clock slave sel and write will get high and the addr of slave will be same as for master_0 and then after 2 to 5 clock again it sel and write signal get hign and addr will be for master_1.
I want to write an assertion for it to check that before serving addr for master_0, master_1 address should not has to come on slave.
I am writing as below but assertion is giving compilation error as Property operator usage is not allowed in sequence context. Implication used
in sequence context.
/* I have two masters and 1 slave.
* For master_0 having signal sel_0,addr_0,write_0,
* For master_1 having signal sel_1,addr_1, write_1
* and for slave signals are sel, addr, write.
when sel_0, sel_1,write_0,write_1 is getting high at same time
it means both are trying to access.
But slave will take 1 request at 1 time and it will take for master_0.
That means after asserting of masters signal
2 to 10 clock slave sel and write will get high and
the addr of slave will be same as for master_0 and
then after 2 to 5 clock again it sel and write signal get hign and addr will be for master_1.
I want to write an assertion for it to check that before serving addr for master_0,
master_1 address should not has to come on slave.
I am writing as below but assertion is giving compilation error as Property operator usage
is not allowed in sequence context. Implication used */
[Ben]
1) Your error is that you have an extra parenthesis
//##[1:8](((sel & write)&& (addr == l_addr_0)) |=> ##[0:2] ((sel & write) && (addr ==l_addr_1)));
//-------^ error on this parenthesis
2) Your usage of the 2nd implication operator is not justified and is incorrect.
When you say something like
a |=> b |=> c
You are stating that if b==0, then the property is vacuous. This is not your intent here.
What you want is a |=> b ##1 c, thus if b==0, the property is false.
3)When you say something like
a |=> ##[1:8]b |=> ##[1:2]c
You antecedent of property (##[1:8]b |=> ##[1:2]c) starts multiple threads,
and for that property to succeed, then all threads must succeed. Specifically,
##[1:8]b |=> ##[1:2]c // is same as
(##1 b |=> ##[1:2]c) or (##2 b |=> ##[1:2]c) or .. (##8 b |=> ##[1:2]c)
If you really want to use the range in an antecedent, then you should use the first_match()
a |=> first_match(##[1:8]b) |=> ##[1:2]c
4) You tend to use way too many parentheses!!!
5) for logical "and", use the && and not the &.
You did that in a few places, but you are not consistent
Thus, for your example:
module top;
bit clk, write_0, sel_0, sel_1, sel, write, write_1;
logic [31:0]addr_0, addr_1, addr;
default clocking @(posedge clk); endclocking
initial forever #10 clk=!clk;
property p_master_prop;
logic [31:0]l_addr_0,l_addr_1;
((write_0 && sel_0 && write_1 && sel_1),l_addr_0=addr_0,l_addr_1=addr_1) |=>
##[1:8] (sel && write) && (addr == l_addr_0) ##[1:2] (sel && write) && (addr ==l_addr_1);
endproperty
ap_master_prop: assert property(p_master_prop);
I have done the same in last as
logic [31:0]l_addr_0,l_addr_1;
((write_0 && sel_0 && write_1 && sel_1),l_addr_0=addr_0,l_addr_1=addr_1) |=>
##[1:8] (sel & write) && (addr == l_addr_0) ##[1:2](sel & write) && (addr ==l_addr_1);
But I had a doubt. I want that (sel & write) && (addr == l_addr_0)condition to get satisfied first and it can come at any clock from 1 to 8, just say at 3 and i want my condition (sel & write) && (addr ==l_addr_1) get checked from 3rd clock when 1st condition is satisfied by 1 to 2 clk after it. Will this assertion do the same check?
Will it check from 1 to 8 clk for first condition and after it 1 to 2 clk for second conditon?
In reply to ben@SystemVerilog.us:
Thanks Ben,
I have done the same in last as
logic [31:0]l_addr_0,l_addr_1;
((write_0 && sel_0 && write_1 && sel_1),l_addr_0=addr_0,l_addr_1=addr_1) |=>
##[1:8] (sel & write) && (addr == l_addr_0) ##[1:2](sel & write) && (addr ==l_addr_1);
But I had a doubt. I want that (sel & write) && (addr == l_addr_0)condition to get satisfied first and it can come at any clock from 1 to 8, just say at 3 and i want my condition (sel & write) && (addr ==l_addr_1) get checked from 3rd clock when 1st condition is satisfied by 1 to 2 clk after it. Will this assertion do the same check?
Will it check from 1 to 8 clk for first condition and after it 1 to 2 clk for second conditon?
Yes. The property a |=> ##[1:8]b ##[1:2] c does state that
if(a) then the sequence ##[1:8]b ##[1:2] c must match
and that sequence does indeed state that ##[1:8]b must occur first and then ##[1:2] c
I done below code:(display i added for just checking after wards), My assertion is not failing when even it get (sel & write)&& (addr == l_addr_0) satisfied but ##[0:4] ((sel & write) && (addr ==l_addr_1) didn’t get satisfied.
Even in display i am getting l_addr_1 and l_addr_0 as always 0 while in the waveform i checked at the same time stamp it is non zero.
Am i making any silly mistake?
I done below code:(display i added for just checking after wards), My assertion is not failing when even it get (sel & write)&& (addr == l_addr_0) satisfied but ##[0:4] ((sel & write) && (addr ==l_addr_1) didn’t get satisfied.
Even in display i am getting l_addr_1 and l_addr_0 as always 0 while in the waveform i checked at the same time stamp it is non zero.
Am i making any silly mistake?
In reply to myselfprakhar:
Did you provide enough clock cycles?
a |=> ##[1:8]b ##[1:2] c
/ is same as
a |=> (##1 b ##1 c) or
(##2 b ##1 c) or
..
(##8 b ##1 c) or
(##1 b ##2 c) or
##2 b ##2 c) or
(##3 b ##2 c) or
..
(##8 b ##2 c);
// A LOT OF POSSIBILITIES.
logic [31:0]l_addr_0,l_addr_1;
((write_0 && sel_0 && write_1 && sel_1),l_addr_0=addr_0,l_addr_1=addr_1) |=>
##[1:8] (sel & write) && (addr == l_addr_0)
##[1:2](sel & write) && (addr ==l_addr_1);
That's a 16 test cycles in the consequent. If at the end of the 16 cycles there is no match, the property will fail; at least is should.
Yes after antecedent got qualify, ##[1:8] (sel & write) && (addr == l_addr_0) condition came after 4 clk and ##[1:2](sel & write) && (addr ==l_addr_1) condition is coming after 15 clk which is not expected, but still my assertion is not throwing any error.
Are your select control signals single pulses? If not, you’ll need a $rose(sel_0), $rose(sel_1), or simply a
$rose(write_0 && sel_0 && write_1 && sel_1).
The way you have it, at every clock cycle where (write_0 && sel_0 && write_1 && sel_1) is true, you have a new attempt and a new thread, which is separate from other previous or future attempts.
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 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
In reply to ben@SystemVerilog.us:
Yes after antecedent got qualify, ##[1:8] (sel & write) && (addr == l_addr_0) condition came after 4 clk and ##[1:2](sel & write) && (addr ==l_addr_1) condition is coming after 15 clk which is not expected, but still my assertion is not throwing any error.
Thanks,
Prakher
// Code your testbench here
// or browse Examples
module m;
bit a, b, c, clk;
initial forever #5 clk=!clk;
ap1: assert property(@ (posedge clk)
$rose(a) |=> ##[1:8] b ##[1:2] c);
initial begin
@ (posedge clk)a <= 1'b1;
repeat(3) @ (posedge clk);
b <= 1'b1;
repeat(11) @ (posedge clk);
$stop;
end
endmodule
"testbench.sv", 7: m.ap1: started at 15ns failed at 125ns
Offending 'c'
$stop at time 145 Scope: m File: testbench.sv Line: 15