System verilog assertion for round robin arbiter

SystemVerilog
, ,
1

Now, REQ1 and REQ2 asserted in the same clock cycle.
So, GNT1 will come at same clock cycle and if REQ1 and REQ2 asserted in the next clock cycle，GNT2 will come in next clock cycle.

2

I used perplexity.ai to hange your Requirements into PPT points.
I then asked it to create SVA Assertions.
It got the right concepts, but made some errors. I corrected those errors.
/* https://www.perplexity.ai/search/Make-this-in-2dZD8FcWThSglJbVcqN.zg
Make this in bullet points.
Now, REQ1 and REQ2 asserted in the same clock cycle.
So, GNT1 will come at same clock cycle and if REQ1 and REQ2 asserted in the next clock cycle，GNT2 will come in next clock cycle.
perplexity.ai: Here are the key points in bullet form:

  1. REQ1 and REQ2 are asserted in the same clock cycle
  2. GNT1 will be granted in the same clock cycle as REQ1 and REQ2
  3. If REQ1 and REQ2 are asserted again in the next clock cycle
    GNT2 will be granted in the next clock cycle */
module top_module(
    input clk,
    input req1,
    input req2,
    output gnt1,
    output gnt2
);
// Assertion for REQ1 and REQ2 asserted in the same cycle
property req1_req2_same_cycle;
    @(posedge clk) (req1 && req2) |-> (gnt1); //|=> (gnt1);  ERROR in perplexity
endproperty

// Assertion for GNT2 in the next cycle if REQ1 and REQ2 are asserted again
property req1_req2_next_cycle;
    @(posedge clk) (req1 && req2) ##1 (req1 && req2) |-> ##1 gnt2; //  |=> ##1 gnt2;  ERROR in perplexity
endproperty


    // Assumptions (if any)
    // ...

    // Assertions
    assert property (req1_req2_same_cycle)
        else $error("REQ1 and REQ2 asserted in the same cycle, but GNT1 not granted");

    assert property (req1_req2_next_cycle)
        else $error("REQ1 and REQ2 asserted in consecutive cycles, but GNT2 not granted in the next cycle");

    // Design under test
    // ...

endmodule

Ben Cohen
Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.

3

// Assertion for REQ1 and REQ2 asserted in the same cycle
property req1_req2_same_cycle;
@(posedge clk) ($rose(req1) && $rose(req2)) |-> $rose(gnt1) && !gnt2 ##1 !gnt1; //This condition will check , first time req1 and req2 are changed from 0 to 1 only gnt1 is asserted and gnt2 is zero in the same cycle and in next cycle gnt1 is asserted.
endproperty

// Assertion for GNT2 in the next cycle if REQ1 and REQ2 are asserted again
property req1_req2_next_cycle;
@(posedge clk) (req1 && req2) ##1 (req1 && req2) |-> ##1 (gnt2 && !gnt1); //This property will make sure only gnt2 is asserted when req1 and req2 asserted for 2 clock cycles.
endproperty

Note: Please let me know if my understanding is correct for arbiter logic.

4

There may be some ambiguity. For example, the first clock. When both req0 and req1 are 1, the next clock may have req0 and req1 being 1 at the same time. When the auction authorization is gnt1 (or perhaps only req1 is authorized as gnt1, or only req0 is authorized as gnt0)

5
clk 1 2 3 4 5 6 7
req0 1 1 1 1 1 1 0
req1 0 0 1 1 0 1 1
gnt0 1 1 0 1 1 0 0
gnt1 0 0 1 0 0 1 1

Here is the result of requesting arbitration。In fact, in addition to arbitration with 2 inputs, there is also arbitration with 3 inputs.

6
  1. I am not clear about your requirements. I also do not want to guess or extrct them from
    tables and timing diagrams.
  2. I am giving you a paper I wrote about arbiters. Though it is not quite what you are looking for, it may help you with some issues, or see ways to implement the verification environment.
    PAPER:. SVA for statistical analysis of a weighted work-conserving
    prioritized round-robin arbiter
    SystemVerilog can perform statistical analysis of computer systems, though it is rarely used in this manner. That kind of performance analysis is very important because it reaffirms the needed system-level requirements.
    http://systemverilog.us/vf/arbiter427.pdf
    http://systemverilog.us/vf/arbiterv422.sv
7

There may be some ambiguity. For example, the first clock. When both req0 and req1 are 1, the next clock may have req0 and req1 being 1 at the same time. When the auction authorization is gnt1 (or perhaps only req1 is authorized as gnt1, or only req0 is authorized as gnt0)