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);