Assertions for a Priority Arbiter

SystemVerilog
, ,
1

I am trying to jot down assertions for a given specification of a priority arbiter.

interface: mem-arbiter( input r1, r2, clk, output g1, g2 )

r1 and r2 are the request lines, g1 and g2 are the corresponding grant lines, and clk is the clock on which the arbiter samples its inputs and performs the arbitration. We assume that the arbitration decision for the inputs at one cycle is reflected by the status of the grant lines in the next cycle. Let us suppose that the specification of the arbiter contains the following requirements:

  1. Request line r1 has higher priority than request line r2. Whenever r1 goes high, the grant line g1 must be asserted for the next two cycles.

  2. The grant lines, g1 and g2, are mutually exclusive.

property grant;
always@(posedge clk) $isonehot0({g1,g2});
endproperty

Property r1;
always@(posedge clk) r1 |=> g1[*2]; 
endproperty

Property r2;
always@(posedge clk) (r2 && !r1) |=> g2[*2]; 
endproperty

Do these assertions seem to be correct? Is there anything I am missing.

2

FIrst, you do not need the “always”, it is implicit.

[center]assert property( @(posedge clk) $isonehot0({g1,g2});[/center]
  ap_0r1_20g1: assert property(@(posedge clk) !r1 |-> ##2 !g1};
  ap_0r2_20g2: assert property(@(posedge clk) !r2 |-> ##2 !g2};
  ap_0g22_1r1: assert property(@(posedge clk) !g2[*2] ##0 r1 |=> g1[*2]);
  ap_0g12_1r2: assert property(@(posedge clk) !g1[*2] ##0 !r1 && r2 |=> g2[*2]);
 

r1    0 0 1 1 0 0 1 0
r2    0 0 x 1 1 1 0 1
g1    0 0 0 1 1 1 0 0 0
g2    0 0 0 0 0 0 1 1 1 1

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

1 Like
3

You should also write assertions where the antecedents are the requests and the consequent are the grants. You’ll need to consider the past requests. This makes the assertions non-dependents on the design.

4

SVA: Assertions should NOT depend on outputs that need verification as requirement inputs. Instead, use support logic to create those needed signals.

E. G., I fell into this trap with this example (link below) :
!g2[*2] ##0 r1 |=> g1[*2];
!g1[*2] ##0 !r1 && r2 |=> g2[*2];
// g1, g2 are signals to be verified
// should use support logic signals that compute the expected values of g1, g2
[

Dr. Tobias Ludwig

That’s very important. No assumptions on outputs