mmaroti

  module Blinker (
   input wire clock,
   output reg state
  );
  
  always @(posedge clock)
   state <= !state;
  
  `if FORMAL
  
  always @(posedge clock)
   assert ($past(state) != state);
  
  `endif
  
  endmodule
  
  module testbench (
   input wire clock,
   output wire state1,
   output wire state2
  );
  
  Blinker blinker1(clock, state1);
  Blinker blinker2(clock, state2);
  
  `if FORMAL
  
  # assume that they are different
  assume (state1 != state2);
  
  # then they stay different
  always @(posedge clock)
    assert (state1 != state2);
  
  `endif
  
  endmodule