Can any one help me ?
In reply to dave_59:
Thanks Dave !
Actually I want to verify it via assertion/checker. Can you help me on this?
My first question was actually not proper.
In reply to Brijesh:
Hi Brijesh,
Its good to see that there is someone out there just like me,
Here is the link which gives you a very good idea on how you can get toward the solution,
https://verificationacademy.com/forums/systemverilog/round-robin-assertion#reply-55939
Note: the solution is not exactly for round robin arbitrator but its for a priority encoder.
I have tried 'n number of ways to verify using ‘generate’ and ‘genvar’ but was not successful but i could only verify individual scenario case by case (even though its not an efficient way i’m still looking for an efficient way to verify same.
Would welcome any kind of better solution than this.
Cheers,
MLearner
///////////////////////////////////////////////////////////////////////////////////////////
property onehot_0
@(posedge clk)
$onehot0(rr_if.GNT);
endproperty
///////////////////////////////////////////////////////////////////////////////////////////
property idle
@(posedge clk)
(rr_if.REQ === 'b0) |=> (rr_if.GNT === 'b0);
endproperty
///////////////////////////////////////////////////////////////////////////////////////////
property rst
@(posedge clk)
reset |-> (rr_if.GNT === 'b0);
endproperty
///////////////////////////////////////////////////////////////////////////////////////////
// Wake up from RESET |or| when REQ = 0000 and RESET = 0
///////////////////////////////////////////////////////////////////////////////////////////
property wakeup3
@(posedge clk) disable iff (!(reset === 0 && rr_if.GNT === 0))
(rr_if.REQ[3] === 1'b1 |=> (rr_if.REQ[3] === 1'b0 && rr_if.GNT[3] === 1'b1);
endproperty
property wakeup2
@(posedge clk) disable iff (!(reset === 0 && rr_if.GNT === 0))
(rr_if.REQ[3:2] === 2'b01 |=> (rr_if.REQ[2] === 1'b0 && rr_if.GNT[2] === 1'b1);
endproperty
property wakeup1
@(posedge clk) disable iff (!(reset === 0 && rr_if.GNT === 0))
(rr_if.REQ[3:1] === 3'b001 |=> (rr_if.REQ[1] === 1'b0 && rr_if.GNT[1] === 1'b1);
endproperty
property wakeup0
@(posedge clk) disable iff (!(reset === 0 && rr_if.GNT === 0))
rr_if.REQ[3:0] === 4'b0001 |=> (rr_if.REQ[0] === 1'b0 && rr_if.GNT[0] === 1'b1);
endproperty
///////////////////////////////////////////////////////////////////////////////////////////
property shift3_2
@(posedge clk)
(rr_if.GNT[3] === 1'b1 && rr_if.REQ[2] === 1'b1) |=> (rr_if.REQ[2] === 1'b0 && rr_if.GNT[2] === 1'b1);
endproperty
property shift2_1
@(posedge clk)
(rr_if.GNT[2] === 1'b1 && rr_if.REQ[1] === 1'b1) |=> (rr_if.REQ[1] === 1'b0 && rr_if.GNT[1] === 1'b1);
endproperty
property shift1_0
@(posedge clk)
(rr_if.GNT[1] === 1'b1 && rr_if.REQ[0] === 1'b1) |=> (rr_if.REQ[0] === 1'b0 && rr_if.GNT[0] === 1'b1);
endproperty
property shift0_3
@(posedge clk)
(rr_if.GNT[0] === 1'b1 && rr_if.REQ[3] === 1'b1) |=> (rr_if.REQ[3] === 1'b0 && rr_if.GNT[3] === 1'b1);
endproperty
///////////////////////////////////////////////////////////////////////////////////////////
property shift3_1
@(posedge clk)
(rr_if.GNT[3] === 1'b1 && rr_if.REQ[2:1] === 2'b01) |=> (rr_if.REQ[1] === 1'b0 && rr_if.GNT[1] === 1'b1);
endproperty
property shift2_0;
@(posedge clk)
(rr_if.GNT[2] === 1'b1 && rr_if.REQ[1:0] === 2'b01) |=> (rr_if.REQ[0] === 1'b0 && rr_if.GNT[0] === 1'b1);
endproperty
property shift1_3
@(posedge clk)
(rr_if.GNT[1] === 1'b1 && rr_if.REQ[0] === 1'b0 && rr_if.REQ[3] === 1'b1) |=> (rr_if.REQ[3] === 1'b0 && rr_if.GNT[3] === 1'b1);
endproperty
property shift0_2
@(posedge clk)
(rr_if.GNT[0] === 1'b1 && rr_if.REQ[2:1] === 2'b10) |=> (rr_if.REQ[2] === 1'b0 && rr_if.GNT[2] === 1'b1);
endproperty
///////////////////////////////////////////////////////////////////////////////////////////
property shift3_0
@(posedge clk)
(rr_if.GNT[3] === 1'b1 && rr_if.REQ[2:0] === 3'b001) |=> (rr_if.REQ[0] === 1'b0 && rr_if.GNT[0] === 1'b1);
endproperty
property shift2_3
@(posedge clk)
(rr_if.GNT[2] === 1'b1 && rr_if.REQ[1:0] === 2'b00 && rr_if.REQ[3] === 1'b1) |=> (rr_if.REQ[3] === 1'b0 && rr_if.GNT[3] === 1'b1);
endproperty
property shift1_2
@(posedge clk)
(rr_if.GNT[1] === 1'b1 && rr_if.REQ[3:2] === 2'b01 && rr_if.REQ[0] === 1'b0) |=> (rr_if.REQ[2] === 1'b0 && rr_if.GNT[2] === 1'b1);
endproperty
property shift0_1
@(posedge clk)
(rr_if.GNT[0] === 1'b1 && rr_if.REQ[3:2] === 3'b001) |=> (rr_if.REQ[1] === 1'b0 && rr_if.GNT[1] === 1'b1);
endproperty
///////////////////////////////////////////////////////////////////////////////////////////
property shift3_3
@(posedge clk)
(rr_if.GNT[3] === 1'b1 && rr_if.REQ[3:0] === 4'b1000) |=> ((rr_if.REQ[3] ==='b0) && $stable(rr_if.GNT));
endproperty
property shift2_2
@(posedge clk)
(rr_if.GNT[2] === 1'b1 && rr_if.REQ[3:0] === 4'b0100) |=> ((rr_if.REQ[2] ==='b0) && $stable(rr_if.GNT));
endproperty
property shift1_1
@(posedge clk)
(rr_if.GNT[1] === 1'b1 && rr_if.REQ[3:0] === 4'b0010) |=> ((rr_if.REQ[1] ==='b0) && $stable(rr_if.GNT));
endproperty
property shift0_0
@(posedge clk)
(rr_if.GNT[0] === 1'b1 && rr_if.REQ[3:0] === 4'b0001) |=> ((rr_if.REQ[0] ==='b0) && $stable(rr_if.GNT));
endproperty