// SVA form of the properties (used by commercial formal tools):
//   a_valid_hold: assert property (@(posedge clk) disable iff (rst) valid && !ready |=> valid);
//   a_data_hold:  assert property (@(posedge clk) disable iff (rst) valid && !ready |=> $stable(data));
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module vr_sender (input clk, input rst, input go, input ready,
                  output reg valid, output reg [7:0] data);
  // sends the words 0, 1, 2, ... one per handshake (valid && ready)
  always @(posedge clk)
    if (rst) begin
      valid <= 1'b0;
      data  <= 8'd0;
    end else begin
      if (go)                valid <= 1'b1;
      else if (ready)        valid <= 1'b0;
      if (valid)             data  <= data + 8'd1;   // bug: should be (valid && ready)
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // valid is not withdrawn before the handshake
  always @(posedge clk) if (!init && !$past(rst) && $past(valid) && !$past(ready)) assert (valid);
  // data stays stable while waiting
  always @(posedge clk) if (!init && !$past(rst) && $past(valid) && !$past(ready)) assert (data == $past(data));
`endif
endmodule