// SVA form of the properties (used by commercial formal tools):
//   m_nostart: assume property (@(posedge clk) disable iff (rst) busy |-> !start);
//   a_lat:     assert property (@(posedge clk) disable iff (rst) start |-> ##[1:3] done);
// The open-source engine in ChipVerify Lab reads the equivalent block below.
module delay_unit (input clk, input rst, input start, input long, output done, output busy);
  // a short job takes 1 cycle, a long job takes 3 cycles
  reg [2:0] cnt;
  assign busy = (cnt != 3'd0);
  assign done = (cnt == 3'd1);
  always @(posedge clk)
    if (rst)                 cnt <= 3'd0;
    else if (start && !busy) cnt <= long ? 3'd4 : 3'd1;   // bug: a long job should load 3
    else if (busy)           cnt <= cnt - 3'd1;

`ifdef FORMAL
  reg init = 1'b1;
  always @(posedge clk) init <= 1'b0;
  always @(*) if (init) assume (rst);
  always @(*) if (busy) assume (!start);           // no new job while busy
  // start |-> ##[1:3] done, written with a helper counter: cycles waited since the start
  reg [2:0] waited = 3'd0;
  always @(posedge clk)
    if (rst || done)           waited <= 3'd0;
    else if (start || waited)  waited <= waited + 3'd1;
  always @(posedge clk) if (!init) assert (waited <= 3'd3);
  // done never comes without a job
  always @(posedge clk) if (!init && done) assert (waited != 3'd0);
`endif
endmodule