tests/regression/const_clocks.sby

   1 [tasks]
   2 btor
   3 smt
   4 btor_m btor multiclock
   5 smt_m smt multiclock
   6
   7 [options]
   8 mode bmc
   9
  10 multiclock: multiclock on
  11
  12 [engines]
  13 #smtbmc
  14 btor: btor btormc
  15 smt: smtbmc boolector
  16
  17 [script]
  18 read_verilog -formal const_clocks.sv
  19 prep -flatten -top top
  20
  21 [file const_clocks.sv]
  22 module top(
  23     input clk,
  24     input [7:0] d
  25 );
  26
  27     (* keep *)
  28     wire [7:0] some_const = $anyconst;
  29
  30     wire [7:0] q;
  31
  32     ff ff1(.clk(1'b0), .d(d), .q(q));
  33
  34     initial assume (some_const == q);
  35     initial assume (q != 0);
  36
  37
  38     always @(posedge clk) assert(some_const == q);
  39 endmodule
  40
  41 module ff(input clk, input [7:0] d, (* keep *) output reg [7:0] q);
  42     always @(posedge clk) q <= d;
  43 endmodule