// SVA form of the properties (used by commercial formal tools):
//   a_zero: assert property (@(posedge clk) disable iff (rst) go && (a == 0 || b == 0) |=> $stable(acc));
//   a_ovf:  assert property (@(posedge clk) disable iff (rst) $rose(ovf) |-> $past(go && sum[2*W]));
// Add `define CUT_MULT as the first line to cut the multiplier.
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module mac_ctl #(parameter W = 12) (input clk, input rst, input go, input [W-1:0] a, input [W-1:0] b,
                                     output reg [2*W-1:0] acc, output reg ovf, output reg [3:0] ops);
  // multiply-accumulate with a sticky overflow flag and an operation counter
`ifdef CUT_MULT
  // cut point: the product is a free value, chosen by the tool in every cycle
  (* anyseq *) reg [2*W-1:0] prod;
`else
  wire [2*W-1:0] prod = a * b;
`endif
  wire [2*W:0]   sum  = {1'b0, acc} + {1'b0, prod};
  always @(posedge clk)
    if (rst) begin
      acc <= 0; ovf <= 1'b0; ops <= 4'd0;
    end else if (go) begin
      acc <= sum[2*W-1:0];
      if (sum[2*W]) ovf <= 1'b1;
      if (ops != 4'd15) ops <= ops + 4'd1;
    end

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  // a zero operand leaves the accumulator unchanged
  always @(posedge clk) if (!init && !$past(rst) && $past(go) && ($past(a) == 0 || $past(b) == 0)) assert (acc == $past(acc));
  // ovf never rises without a carry out of the accumulator
  always @(posedge clk) if (!init && !$past(rst) && ovf && !$past(ovf)) assert ($past(go) && $past(sum[2*W]));
`endif
endmodule