tests/unsorted/smtlib2_module.sby

   1 [options]
   2 mode bmc
   3 depth 1
   4
   5 [engines]
   6 smtbmc
   7
   8 [script]
   9 read_verilog -formal test.v
  10 prep -top top
  11
  12 [file test.v]
  13 (* blackbox *)
  14 (* smtlib2_module *)
  15 module submod(a, b);
  16         input [7:0] a;
  17         (* smtlib2_comb_expr = "(bvnot a)" *)
  18         output [7:0] b;
  19 endmodule
  20
  21 module top;
  22         wire [7:0] a = $anyconst, b;
  23
  24         submod submod(
  25                 .a(a),
  26                 .b(b)
  27         );
  28
  29         always @* begin
  30                 assert(~a == b);
  31         end
  32 endmodule