module demo (rst, clk, in0, out0, out1);

   input rst;
   input clk;
   input in0;
   output out0;
   output out1;

   reg out0;
   reg out1;



   // if out1 is asserted then next cycle it is de-asserted
   p1: assert property ( @(posedge clk) out1 |-> ##1 ~out1);

   // if out1 is asserted then next cycle it is de-asserted and next cycle it is asserted again
   p2: assert property ( @(posedge clk) out1 |-> ##1 ~out1 ##1 out1);

   // on any posedge the value of out1
   // is an inverse of its value in the previous cycle
   p3: assert property ( @(posedge clk) ($past(out1) == ~out1));

   // out0 is in0 inversed and delayed by 1 cycle
   p4: assert property ( @(posedge clk) (out0 == ~($past(in0))) || $past(rst));



   // out0 is always asserted
   //p5: assert property ( @(posedge clk) ~($past(rst)) |-> out0 == 1'b1);                   

   // constraint:
   //c1: assert property ( @(posedge clk) in0 == 1'b0);

   always @(posedge clk)
         out0 <= ~in0;


   always @(posedge clk)
      begin
      if (rst)
         out1 <= 1'b0;
      else
         out1 <= ~out1;
      end

endmodule