// This is a testcase that shows false assertion firing,
// due to inter-timestep value fluxuations.
// Run this on your favorite SystemVerilog simulator.

module inter;

  reg rs1, rs1a, s2, s3;

  reg do, d1, d2;

  reg tmp, s1a;

  reg clk;
  initial
    begin
    clk = 1'b1;
    forever clk = #5 ~clk;
    end

  wire  s1  = rs1 | ~s1a;

initial $monitor($stime,, "s1 = %b, s2=%b", s1, s2);

  initial begin
    rs1  <= 1'b0;
    s1a  <= 1'b1;
    s2   <= 1'b0;

    @(posedge clk);
    s1a <= 1'b0;  // Turn on s1.

    @(posedge clk);
    s2  <=    1'b1;    // Oops, we have both selects set...
    s1a <= #1 1'b1;  // Model input delay (from different coding style block.)

    @(posedge clk);

    s2  <= 1'b0;

    repeat (5) @(posedge clk);
    $finish;
    end


  always @(s1 or s2 or d1 or d2)
    begin
    // This is how one prevents false firings due to intra/inter-timestep
    // value changes. By disabling a previously started assertion
    // it will not fail. NOTE: requiring this kills overlapping 
    // assertions, because disable stops all running blocks/assertions!

    disable checkit;  // disable any (ALL) previous assertions.

    // This is our model of the antecedent in more complex
    // assertions. This may have been several nested if()'s or
    // a case item, etc.
    // Check s2 at the end of the cycle - before the registers update to
    //   their new values. Wierd - yes!
    if (s1) checkit: assert (1;!s2) @@(posedge clk);

    // Our functionality that we are preventing.
    do = s1 & d1 | s2 & d2;
    end

endmodule