Hi,
If I have to test a priority encoded arbiter with say, 4-inputs (request signals) and 4-outputs (grant signals), What assertions are required for verifying this arbiter?
The following is a generalized solution for a large vector up to 30 bits (i.e., 29:0]).
The concern for 32 bits is that setting v[31]to 1’b1 creates a negative number and would cause error in my req < v. One solution for larger vectors would be to use time data type, which is a 4-state data type, 64-bit unsigned integer.
module arbiter;
//If I have to test a arbiter encoded arbiter with say, 4-inputs (request signals) and 4-outputs (grant signals),
//What assertions are required for verifying this arbiter?
bit[15:0] req, grnt;
bit clk;
generate for (genvar i=0; i<=15; i++)
begin
property p_arbiter;
bit[16:0] v;
(req[i]==1'b1, v=0, v[i+1]=1'b1) ##0 req < v |->
grnt[i]==1'b1 ##0 $onehot(grnt);
endproperty : p_arbiter
ap_arbiter: assert property(@(posedge clk) p_arbiter);
end
endgenerate
ap_zero_req: assert property(@(posedge clk) req==0 |-> grnt==0);
endmodule
// bit 1111 11
// 5432 1098 7654 3210
//-----------------------------------
// req = 0000_0000_0011_1011
// grnt= 0000_0000_0010_0000
// v = 0000_0000_0000_0010 -- i==0 req[0]==1, req > v, thus vacuous
// v = 0000_0000_0000_0100 -- i==1 req[1]==1, req > v, thus vacuous
// v = 0000_0000_0000_1000 -- i==2 req[2]==0, thus vacuous
// v = 0000_0000_0001_0000 -- i==3 req[3]==1, req > v, thus vacuous
// v = 0000_0000_0010_0000 -- i==4 req[4]==1, req > v, thus vacuous
// v = 0000_0000_0100_0000 -- i==5 req[5]==1, req < v, thus nonvacuous
// v = 0000_0000_1000_0000 -- i==6 req[6]==0, thus vacuous
// v = 0000_0001_0000_0000 -- i==7 req[7]==0, thus vacuous
Note: I did not test this code, but I believe that it should work. Compiles OK.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
- A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
- SystemVerilog Assertions Handbook 3rd Edition, 2013 ISBN 878-0-9705394-3-6
- 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:
Note: the v=0 (below) is not really necessary and can be deleted since v is initialized to 0 anyway.
Making v=0 clarifies the intent.
(req[i]==1’b1, v=0, v[i+1]=1’b1) ##0 req < v |->
Thus, this would be OK too
(req[i]==1’b1, v[i+1]=1’b1) ##0 req < v |->
Ben
In reply to ben@SystemVerilog.us:
Hi Ben,
The above logic seems ok to verify a priority-encoded arbiter.
- Only 1 grant is active in a clock cycle.
- The active grant corresponds to the (higher numbered bit in) active request.
- No grant is issued if no request is active.
Here, a particular active request will remain active until it sees a corresponding active grant in the sampling clock edge.
As I understand, Since at every sampling clock, the local variable v to the property is created newly and used for asserting if the property holds, hence, v will be initialised to 0 when bit[16:0] v; statement is executed. By default, SV assigns ‘0’ to 2-state variables (here, bit[16:0] v).
Is that the reason behind why we can ignore v=0 in the property expression?
In reply to Vignesh Raghavan:
As I understand, Since at every sampling clock, the local variable v to the property is created newly and used for asserting if the property holds, hence, v will be initialised to 0 when bit[16:0] v; statement is executed. By default, SV assigns ‘0’ to 2-state variables (here, bit[16:0] v).
Is that the reason behind why we can ignore v=0 in the property expression?
The short answer is YES.
The formal answer is from 1800, specifically,
16.8.2 Local variable formal arguments in sequence declarations
In general, a local variable formal argument behaves in the same way as a local variable declared in an
assertion_variable_declaration. The rules in 16.10 for assigning to and referencing local variables,
including the rules of local variable flow, apply to local variable formal arguments with the following
provisions:
Without further specification, the term local variable shall mean either a local variable formal
argument or a local variable declared in an assertion_variable_declaration.
— At the beginning of each evaluation attempt of an instance of a named sequence, a new copy of each
of its local variable formal arguments shall be created.
Ben Cohen
SystemVerilog.us
In reply to Vignesh Raghavan:
Another solution, simpler, but without concurrent assertions.
module arbiter;
//If I have to test a arbiter encoded arbiter with say, 4-inputs (request signals) and 4-outputs (grant signals),
//What assertions are required for verifying this arbiter?
bit[15:0] req, grnt;
bit clk;
always @(posedge clk) begin
for (int i=15; i< 0; i--) begin
if (req[i])
begin
assert(grnt[i]==1'b1 && $onehot(grnt)); // immediate assertion
break;
end
end
end
ap_zero_req: assert property(@(posedge clk) req==0 |-> grnt==0);
In reply to ben@SystemVerilog.us:
Hi Ben,
This looks great. I guess there is no necessity for a break statement inside the begin…end block.
Because we are checking grnt[i] == 1’b1 and at the same time, if gnt itself is one-hot encoded. So, Even if other iterations run, I hope it should not affect our results. Or does it?
In reply to Vignesh Raghavan:
I guess there is no necessity for a break statement inside the begin…end block.
You’re correct, however, the break gives you the following advantages:
- It clarifies the requirements in that once you find the high bit being true, the lower order bits are irrelevant, or don’t care.
- Efficiency.
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
So True, Ben.
One more important reason to add break statement is, which i didn’t think of before -
if more than 1 request is asserted simultaneously, the assertion in begin…end block will pass for highest priority request. But, If break statement is not used, the assertion will fail for the lower priority requests (which is valid but we do not want to see redundant errors), as the grant is high only corresponding to highest priority request.
Thanks,
Vignesh
Another Solution from SVA cookbook videos. Adding so that it is indexed.
SVA Cookbook Link
Assumes the fixed priority 0 > 1 > 2 > 3 > 4 > 5
If a high priority req[i] is asserted then gnt[i] is not seen before the low priority gnt[j], such a sequence should not be seen.
property priority_arb(i,j);
@(posedge clk) disable iff(rst)
not( ((j>i) && req[i]) ##1 ( !gnt[i] throughout (gnt[j][->1]) ) );
endproperty
generate
genvar i,j;
for(i=0; i<6; i++)
for(j=0; j<6; j++)
assert property(priority_arb(i,j));
end
end
endgenerate
Have not tested it though!!!
In reply to devil47:
Tested your code with the generate. It failed to verify a $onehot(gnt). See
property priority_arb(i,j); // BAD by itself, needs ap_gnt
@(posedge clk) // disable iff(rst)
not( ((j>i) && req[i]) ##1 ( !gnt[i] throughout (gnt[j] && $countones(gnt)==1[->1]) ) );
endproperty
generate begin
genvar i, j;
for (i = 0; i<=2; i++) begin
for (j = 0; j<=2; j++) begin
assert property (priority_arb(i,j));
end
end
end
endgenerate
In general, I prefer to use the not operator on a property of a single simple expression rather than a sequence because it is harder to understand. Also, the not says that something should Not happen, but it does not express what you expect to happen.
bit[2:0] req, gnt; // req[0] is high priority *****
// the following assertions seem to work
ap000: assert property(req[0] |=> gnt== 3'b000 [*0:$] ##1 $onehot(gnt) && gnt[0]);
ap010: assert property(req[1] |=> gnt<= 3'b010 || gnt==3'b000 [*0:$] ##1 $onehot(gnt) && gnt[1]);
// No higher priority gnt provided after req[1]
ap100: assert property(req[2] |=> gnt<=3'b100 || gnt==3'b000 [*0:$] ##1 $onehot(gnt) && gnt[2]);
// No higher priority gnt provided after req[2]
In the above assertions, the higher priority fails when gnt is given to a lower priority
// my testbench
http://systemverilog.us/vf/priority03.sv
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact http://cvcblr.com/home
- 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
- SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue - SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
- SVA in a UVM Class-based Environment
https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment
Hi ,
In addition to the above scenario if i want to check for other requests also gnt is asserted or not ?is it possible using assertions?
scenario: Once after servicing the priority interrupts i need to check other interrupts also got serviced or not.
generate for (genvar i=0; i<=15; i++)
begin
property p_arbiter;
bit[16:0] v;
(req[i]==1’b1, v=0, v[i+1]=1’b1) ##0 req < v |->
grnt[i]==1’b1 ##0 ($countones(req)==$countones(gnt));
endproperty : p_arbiter
ap_arbiter: assert property(@(posedge clk) p_arbiter);
end
endgenerate
Please let me know
Thanks in advance