1
2
3
4
5
6
7
8

`ifdef FORMAL
  // Designer properties (R1, R2), checked by formal tools only: occupancy never exceeds the
  // depth, and the count agrees with the pointers (the invariant that makes induction work).
  always @(posedge clk) if (!rst) begin
    assert (count <= 4'd8);
    assert (count[2:0] == 3'(wp - rp));
  end
`endif

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39

`ifdef FORMAL
  // Designer properties (R3, R6, R7), checked by formal tools only (read_verilog -formal
  // defines FORMAL; simulators never see this block). A wrapper supplies the environment.
  logic f_past = 1'b0;
  always @(posedge clk) f_past <= 1'b1;

  // R7: an output's credits plus the flits its sink still holds always total 4
  logic [2:0] f_held [0:3];
  always @(posedge clk)
    for (int o = 0; o < 4; o++)
      f_held[o] <= rst ? 3'd0 : f_held[o] + (send[o] ? 3'd1 : 3'd0) - (out_crd[o] ? 3'd1 : 3'd0);
  // environment: a sink returns a credit only for a flit it holds
  always @(*) for (int o = 0; o < 4; o++) if (out_crd[o]) assume (f_held[o] != 3'd0);

  // R6: the specification's choice of winner for each free output: the first requester at or
  // after the round-robin pointer, among high-priority requesters if prio_en is set and any exist
  logic [3:0] f_any, f_hi;
  logic [1:0] f_win [0:3];
  always_comb
    for (int o = 0; o < 4; o++) begin
      f_any[o] = 1'b0; f_hi[o] = 1'b0; f_win[o] = 2'd0;
      for (int i = 0; i < 4; i++) if (req[i] && head[i][15:14] == 2'(o)) begin
        f_any[o] = 1'b1;
        if (head[i][13]) f_hi[o] = 1'b1;
      end
      for (int k = 3; k >= 0; k--) begin
        logic [1:0] i;
        i = 2'(rr[o] + 2'(k));
        if (req[i] && head[i][15:14] == 2'(o) && (!(prio_en && f_hi[o]) || head[i][13])) f_win[o] = i;
      end
    end

  always @(posedge clk) if (f_past && !rst)
    for (int o = 0; o < 4; o++) begin
      assert ({1'b0, credits[o]} + {1'b0, f_held[o]} == 4'd4);                  // R7
      if (!lock[o] && !sleeping && f_any[o]) assert (grant[o] && gidx[o] == f_win[o]);   // R6, R3
      if ($past(grant[o] && !rst)) assert (rr[o] == $past(gidx[o]) + 2'd1);    // R6 rotation
    end
`endif

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

// formal: prove 4
// uses: dcrouter
// DCRouter step 9: a formal harness. Every input is free: any packets, any APB traffic, any
// timing; the only environment rules are reset in the first cycle and, inside DCRouter's
// property block, that a sink returns a credit only for a flit it holds. The properties
// themselves are the designer's, in dcrouter.sv under `ifdef FORMAL`: FIFO occupancy and
// pointers (R1, R2), the arbiter's choice and rotation (R3, R6), and credits (R7).
// `prove 4`: a bounded check of 4 cycles, then a 4-step induction, so a pass holds at every depth.
module dcr_formal (
  input logic clk, rst,
  input logic [3:0]  in_vld, in_last, out_crd,
  input logic [63:0] in_data,
  input logic psel, penable, pwrite,
  input logic [7:0]  paddr,
  input logic [31:0] pwdata
);
  logic [3:0]  in_rdy, out_vld, out_last, out_err;
  logic [63:0] out_data;
  logic [31:0] prdata;
  logic        pready, pslverr, sleeping;
  dcrouter dut (.*);
  logic past = 1'b0;
  always @(posedge clk) past <= 1'b1;
  always @(*) assume (rst == !past);               // reset in the first cycle only
endmodule

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25

// formal: bmc 7 expect fail
// uses: dcrouter BUG_5
// DCRouter step 9: a formal harness. Every input is free: any packets, any APB traffic, any
// timing; the only environment rules are reset in the first cycle and, inside DCRouter's
// property block, that a sink returns a credit only for a flit it holds. The properties
// themselves are the designer's, in dcrouter.sv under `ifdef FORMAL`: FIFO occupancy and
// pointers (R1, R2), the arbiter's choice and rotation (R3, R6), and credits (R7).
// With BUG_5 (the round-robin pointer never moves) the bounded check must find a counterexample.
module dcr_formal_bug5 (
  input logic clk, rst,
  input logic [3:0]  in_vld, in_last, out_crd,
  input logic [63:0] in_data,
  input logic psel, penable, pwrite,
  input logic [7:0]  paddr,
  input logic [31:0] pwdata
);
  logic [3:0]  in_rdy, out_vld, out_last, out_err;
  logic [63:0] out_data;
  logic [31:0] prdata;
  logic        pready, pslverr, sleeping;
  dcrouter dut (.*);
  logic past = 1'b0;
  always @(posedge clk) past <= 1'b1;
  always @(*) assume (rst == !past);               // reset in the first cycle only
endmodule