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