tests/sva/sva_throughout.sv

   1 module top (
   2         input clk,
   3         input a, b, c, d
   4 );
   5         default clocking @(posedge clk); endclocking
   6
   7         assert property (
   8                 a |=> b throughout (c ##1 d)
   9         );
  10
  11 `ifndef FAIL
  12         assume property (
  13                 a |=> b && c
  14         );
  15         assume property (
  16                 b && c |=> b && d
  17         );
  18 `endif
  19 endmodule