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
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126

// PacketFIFO checker: handshake holds, occupancy limits and packet rules on the ports of packet_fifo.
// BUG selects a planted design bug: 0 none, 1 in_ready stuck high (overflow), 2 out_valid stuck high (underflow).
module packet_fifo #(
  parameter WIDTH = 9,
  parameter DEPTH = 4,
  parameter AW    = 2,
  parameter BUG   = 0
) (
  input  wire             clk,
  input  wire             rst_n,
  input  wire             in_valid,
  output wire             in_ready,
  input  wire [WIDTH-1:0] in_data,
  output wire             out_valid,
  input  wire             out_ready,
  output wire [WIDTH-1:0] out_data
);
  reg [WIDTH-1:0] mem [0:DEPTH-1];
  reg [AW-1:0]    wptr, rptr;
  reg [AW:0]      count;
  wire push = in_valid && in_ready;
  wire pop  = out_valid && out_ready;

  assign in_ready  = (BUG == 1) ? 1'b1 : (count != DEPTH);
  assign out_valid = (BUG == 2) ? 1'b1 : (count != 0);
  assign out_data  = mem[rptr];

  always @(posedge clk or negedge rst_n)
    if (!rst_n) begin
      wptr  <= 0;
      rptr  <= 0;
      count <= 0;
    end else begin
      if (push) begin
        mem[wptr] <= in_data;
        wptr <= wptr + 1'b1;
      end
      if (pop) rptr <= rptr + 1'b1;
      case ({push, pop})
        2'b10:   count <= count + 1'b1;
        2'b01:   count <= count - 1'b1;
        default: count <= count;
      endcase
    end
endmodule

module pf_checker #(
  parameter int DEPTH = 4
) (
  input logic       clk, rst_n,
  input logic       in_valid, in_ready,
  input logic [8:0] in_data,
  input logic       out_valid, out_ready,
  input logic [8:0] out_data
);
  int n_fail = 0, n_in_stall = 0, n_out_stall = 0, n_full = 0, n_pkt = 0;
  function automatic void fail(string msg);
    n_fail++;
    $display("[%0t] pf_checker: %s", $time, msg);
  endfunction

  // Modeling code: occupancy, and where we are inside the current packet.
  wire push = in_valid && in_ready;
  wire pop  = out_valid && out_ready;
  int         occ = 0;
  logic       hdr = 1'b1;       // next accepted byte is a header
  logic [4:0] left = 5'd0;      // bytes still to come in this packet, check byte included
  logic [7:0] xr = 8'h00;       // XOR of the bytes accepted so far in this packet
  always_ff @(posedge clk or negedge rst_n)
    if (!rst_n) begin
      occ <= 0; hdr <= 1'b1; left <= 5'd0; xr <= 8'h00;
    end else begin
      occ <= occ + (push ? 1 : 0) - ((pop && occ > 0) ? 1 : 0);
      if (push) begin
        if (hdr) begin
          hdr <= 1'b0; left <= in_data[3:0] + 5'd1; xr <= in_data[7:0];
        end else begin
          xr <= xr ^ in_data[7:0]; left <= left - 5'd1;
          if (left == 5'd1) hdr <= 1'b1;
        end
      end
    end

  // Step 1: an offer is held, with the same byte, until it is accepted (both ports).
  a_in_valid_hold: assert property (@(posedge clk) disable iff (!rst_n)
    (in_valid && !in_ready) |-> ##1 in_valid)
    else fail("in_valid dropped before in_ready");
  a_in_data_hold: assert property (@(posedge clk) disable iff (!rst_n)
    (in_valid && !in_ready) |-> ##1 $stable(in_data))
    else fail("in_data changed while stalled");
  a_out_valid_hold: assert property (@(posedge clk) disable iff (!rst_n)
    (out_valid && !out_ready) |-> ##1 out_valid)
    else fail("out_valid dropped before out_ready");
  a_out_data_hold: assert property (@(posedge clk) disable iff (!rst_n)
    (out_valid && !out_ready) |-> ##1 $stable(out_data))
    else fail("out_data changed while stalled");

  // Step 2: never accept into a full FIFO, never hand out from an empty one.
  a_no_overflow: assert property (@(posedge clk) disable iff (!rst_n)
    (occ == DEPTH) |-> !push)
    else fail("overflow: byte accepted while full");
  a_no_underflow: assert property (@(posedge clk) disable iff (!rst_n)
    (occ == 0) |-> !pop)
    else fail("underflow: byte taken while empty");

  // Step 3: packet rules on the accepted bytes.
  a_len_legal: assert property (@(posedge clk) disable iff (!rst_n)
    (push && hdr) |-> (in_data[3:0] inside {[1:8]} && !in_data[8]))
    else fail("header: len outside 1 to 8, or last set");
  a_last_on_check: assert property (@(posedge clk) disable iff (!rst_n)
    (push && !hdr) |-> (in_data[8] == (left == 5'd1)))
    else fail("last is not on the check byte");
  a_check_xor: assert property (@(posedge clk) disable iff (!rst_n)
    (push && !hdr && left == 5'd1) |-> ((xr ^ in_data[7:0]) == 8'h00))
    else fail("check byte is not the XOR of the packet");

  // Step 4: covers prove the antecedents were reached.
  c_in_stall: cover property (@(posedge clk) disable iff (!rst_n)
    (in_valid && in_ready == 1'b0) ##1 (in_valid && in_ready)) n_in_stall++;
  c_out_stall: cover property (@(posedge clk) disable iff (!rst_n)
    (out_valid && out_ready == 1'b0) ##1 (out_valid && out_ready)) n_out_stall++;
  c_full: cover property (@(posedge clk) disable iff (!rst_n)
    occ == DEPTH) n_full++;
  c_packet: cover property (@(posedge clk) disable iff (!rst_n)
    push && in_data[8]) n_pkt++;
endmodule