// SVA form of the properties (used by commercial formal tools):
//   a_from_input: assert property (@(posedge clk) disable iff (rst) out_valid |-> $past(in_valid, 2));
//   a_after_rst:  assert property (@(posedge clk) $fell(rst) |-> !out_valid);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module valid_pipe (input clk, input rst, input in_valid, input [7:0] in_data,
                   output out_valid, output [7:0] out_data);
  // two-stage pipeline; the valid bits travel with the data
  reg       v1, v2;
  reg [7:0] d1, d2;
  always @(posedge clk) begin
    if (rst) v1 <= 1'b0;                       // bug: v2 is not reset
    else     v1 <= in_valid;
    v2 <= v1;
    d1 <= in_data;
    d2 <= d1;
  end
  assign out_valid = v2;
  assign out_data  = d2;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // an output word is always one that came in two cycles earlier
  always @(posedge clk)
    if (!init && !$past(rst) && !$past(rst, 2) && out_valid) assert ($past(in_valid, 2));
  // no output in the cycle after reset
  always @(posedge clk) if (!init && $past(rst)) assert (!out_valid);
`endif
endmodule