// SVA form of the property (used by commercial formal tools):
//   a_prod: assert property (@(posedge clk) disable iff (rst) done |-> p == ra * rb);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module seqmul #(parameter W = 6) (input clk, input rst, input start, input [W-1:0] a, input [W-1:0] b,
                                     output reg done, output reg [2*W-1:0] p);
  // shift-and-add multiplier: one bit of b per cycle
  reg [2*W-1:0] ma;
  reg [W-1:0]   mb;
  reg [7:0]     n;
  reg           busy;
  always @(posedge clk)
    if (rst) begin
      busy <= 1'b0; done <= 1'b0;
    end else if (start && !busy) begin
      ma <= a; mb <= b; p <= 0; n <= 0; busy <= 1'b1; done <= 1'b0;
    end else if (busy) begin
      if (mb[0]) p <= p + ma;
      ma <= ma << 1; mb <= mb >> 1; n <= n + 8'd1;
      if (n == W - 1) begin busy <= 1'b0; done <= 1'b1; end
    end else
      done <= 1'b0;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // remember the operands of the job
  reg [W-1:0] ra, rb;
  always @(posedge clk) if (start && !busy && !rst) begin ra <= a; rb <= b; end
  // when done, the product is a * b
  always @(posedge clk) if (!init && done) assert (p == ra * rb);
`endif
endmodule