// SVA form of the end-to-end property (used by commercial formal tools):
//   a_sum: assert property (@(posedge clk) disable iff (rst) sum == n * (n + 1) / 2);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module src (input clk, input rst, input ready, output reg valid, output reg [7:0] data);
  // sends 1, 2, 3, ... on a valid/ready interface
  always @(posedge clk)
    if (rst) begin
      valid <= 1'b0; data <= 8'd1;
    end else begin
      valid <= 1'b1;
      if (valid) data <= data + 8'd1;        // bug: should advance only on valid && ready
    end
endmodule

module sink (input clk, input rst, input stall, input valid, input [7:0] data,
             output ready, output reg [7:0] n, output reg [15:0] sum);
  // adds up every word it receives
  assign ready = !stall;
  always @(posedge clk)
    if (rst) begin
      n <= 8'd0; sum <= 16'd0;
    end else if (valid && ready) begin
      n <= n + 8'd1; sum <= sum + data;
    end
endmodule

module link (input clk, input rst, input stall, output [7:0] n, output [15:0] sum);
  wire valid, ready;
  wire [7:0] data;
  src  u_src  (.clk(clk), .rst(rst), .ready(ready), .valid(valid), .data(data));
  sink u_sink (.clk(clk), .rst(rst), .stall(stall), .valid(valid), .data(data), .ready(ready), .n(n), .sum(sum));

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // end to end: after n words 1..n, the sum is n*(n+1)/2
  always @(posedge clk) if (!init) assert (sum == ({8'd0, n} * ({8'd0, n} + 16'd1)) / 16'd2);
`endif
endmodule