I am trying to write assertion for round robin arbiter. In my case there are four request signals and one [3:0] grant signal. Random no of request signals will active afterthat when grant signal go low then on same clock request go low and then server for next grant signal i.e. like when $fell(gnt[2])|->$fell(req[2]) then check for next grant signal i.e grant[3] when it’s respective req is active then grant[0] then grant[1] and so on. I am facing to figure out logic if req[2] and gnt[2] is completed then check for req[3] and gnt[3] if req[3] is active.
In reply to yaten1993:
I do not like the idea that the arbitrations are not clocked, in the sense that in one clock cycle if you have multiple req and each req is immediately granted, then the next grant will occur immediately. Bad practice. In any case, here is an untested verification model:
/* 08/11/23 I am trying to write assertion for round robin arbiter.
In my case there are four request signals and one [3:0] grant signal.
Random no of request signals will active afterthat when grant signal
go low then on same clock request go low and then server for next grant signal i.e. like when
//
when it's respective req is active then grant[0] then grant[1] and so on.
I am facing to figure out logic if req[2] and gnt[2] is completed
then check for req[3] and gnt[3] if req[3] is active. */
//==========
module arbiter_check(input bit clk, reset_n,
input bit [3:0] req, // request, bit 3 starts as 1st priority, then round-robbin
input bit[3:0] grant);
bit[1:0] last_grant;
//function automatic grant_type grant_lower_bound(bit[3:0] prty, bit[15:0] rqst);
function automatic void do_grant();
bit[3:0] vgrant=0;
bit[1:0] next_grant;
if(last_grant==0) next_grant=3; else next_grant=last_grant-1;
//
for (int i = next_grant; i>= 0; i--) begin : forlp1
if(req[i]) begin
vgrant= i;
last_grant=i;
am_arb: assert #0 (req[i] && grant==vgrant);
end
end : forlp1
endfunction
// ----------------------------------------------
always_comb begin
if (!reset_n) last_grant=3;
else // $fell(gnt[2])|->$fell(req[2]) then check for grant[3]
if(req!=0 && grant==0) do_grant();
end
am_arb2: assert final ((req==0 && grant==0 ) || $onehot0(grant));
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
I tried by using the following supporting logic.
always@(posedge clk or negedge rst_n)begin
if(!rst_n)begin
req_ptr <= 0 ;
end
else begin
case(1'b1)
grant[0]: req_ptr <= 'd1;
grant[1]:req_ptr <= 'd2;
grant[2]:req_ptr <= 'd3;
grant[3]:req_ptr <= 'd0;
default : req_ptr <= req_ptr;
endcase
end
end
// shift request position based on req_ptr ;
// shift request will be feed to get priority mask for expected grant calculation.
always_comb begin
found = 0 ;
use_ptr = req_ptr ;
high_ptr = 3 ; // default to MAX number
for(int i = use_ptr ; i <= high_ptr ; i++) begin
if(req[i] && !found) begin
idx = i ;
found = 1 ;
end
end
if(found == 0 ) begin
for(int i = use_ptr ; i >= 0 ; i--) begin
if(req[i]) begin
idx = i ;
found = 1 ;
end
end
end
if(found) mask_req = 1 << idx ;
end
property check_req_gnt(i) ;
@(posedge clk ) disable iff (!rst_n)
req[i] && mask_req[i] |=> grant[i];
endproperty
property check_not_req_gnt(i) ;
@(posedge clk ) disable iff (!rst_n)
!req[i] && !mask_req[i] |=> !grant[i];
endproperty
property check_req_not_gnt(i) ;
@(posedge clk ) disable iff (!rst_n)
req[i] && !mask_req[i] |=> !grant[i];
endproperty
for(genvar i = 0 ; i <=3 ; i++)begin
ast_check_req_gnt : assert property(check_req_gnt(i));
end
for(genvar i = 0 ; i <=3 ; i++)begin
ast_check_not_req_gnt : assert property(check_not_req_gnt(i));
end
for(genvar i = 0 ; i <=3 ; i++)begin
ast_check_req_not_gnt : assert property(check_req_not_gnt(i));
end
property one_hot_gnt ;
@(posedge clk ) disable iff (!rst_n)
$onehot0(grant);
endproperty
ast_one_hot : assert property (one_hot_gnt);
In reply to kddholak:
Just looking at the properties, this is not meeting the unusal requirements that “grant signal go low then on same clock request go low and then server for next grant signal”.
Ben
Next grant will not come immediately. It is like all requests or random no of requests go high on same clock then check whose respective grant is getting low first on same clock their request go low then after check for next grant in ordered fashion like (2->3->0->1 or 1->2->3->0 or 3->0->1->2 and other possibilities) after multiple clock delays next grant go low on same clock their request also go low … I shared the image. In that all req are high at same time and after some delay or on same time gnt1 go low on same time req1 also go low, then after clock delays gnt2 go low on same time req2 go low, same for gnt3 and gnt0 . In $fell(gnt[i]) first value of i is random after that follow an order((2->3->0->1 or 1->2->3->0 or 3->0->1->2 and other possibilities) based on i value. And gnt will come only for those their req are high. 1st challenge is to detect which gnt is going low then after that follow an order(in image gnt1 go low then gnt2 then gnt3 then gnt0). Only one bit of gnt go high at a time.
Thank you Ben For giving me an idea. I am trying it
In reply to yaten1993:
This is a first-cut at a verifier where the arbiter switches the priority
from 3 to 2 to 1 to 0 and back to 3.
If priority is 3, but req[2]==1 then grant[2] should be asserted by the rtl.
My TB is primitive (see link).
The RTL should maintain the priority in a one-shot register.
Edit code - EDA Playground // code
EPWave Waveform Viewer // wave
module arbiter_check(input bit clk, reset_n,
input bit [3:0] req, // request, bit 3 starts as 1st priority,
input bit[3:0] grant);
bit[3:0] chkr_grant;
bit[1:0] next_grant;
int pass, fail;
let range(val, width) = (val & (2 << width) - 1);
// Extracts bits width:0 from val[n:0]
// the solution with a mask is the best, provided that the lower index bound is 0.
// Example if ((range(req, next_grant)) != 0) begin : within_the_low_bound
// if req[3:0]==1011, next_grant==1, the
// range(4'b1011, 2'b01)== 4'b1011 & (4'b0010 << 1)-1
// 4'b1011 & (4'b0100 -1) == 4'b1011 & 4'b0011) == 4'b0011
//
// task is called when there is a req
task automatic do_grant();
bit found=0;
bit[3:0] vgrant;
// maintain next_grant pointer
if(next_grant==0)
next_grant <=3;
else
next_grant <=next_grant-1;
// CHeck if the req is from next_grant to 0
if (range(req, next_grant) >0)
begin : lower_bound
for (int i = next_grant; i>= 0; i=i-1)
begin : forlp1
if(req[i])
begin
vgrant[i]=1; $display("vgrant=%b", vgrant);
found=1;
chkr_grant <= vgrant;
next_grant<=i-1;
break;
end
end : forlp1
end : lower_bound
//else if not found, check rea in range (req[3:next_grant+1],
else if (!found && range(req, next_grant) >0)
begin :upper_bound
for (int i = 3; i>= next_grant; i=i-1)
begin : forlp2
if(req[i])
begin
vgrant[i]=1;
found=1;
chkr_grant <= vgrant;
next_grant<=i-1;
break;
end
end : forlp2
end : upper_bound
endtask
// ----------------------------------------------
/* Highest priority pointer */
always @(posedge clk)
begin
if (!reset_n)
next_grant<=3;
else //
if(req!=0 && grant==0) // there is a req and no grant
do_grant();
end
ap_req_grant: assert property(@(posedge clk)
req>0 |-> @(negedge clk) grant==chkr_grant && $onehot(grant))
pass=pass+1; else fail=fail+1;
endmodule