tests/unsorted/floor_divmod.sby

   1 [options]
   2 mode bmc
   3
   4 [engines]
   5 smtbmc
   6
   7 [script]
   8 read_verilog -icells -formal test.v
   9 prep -top top
  10
  11 [file test.v]
  12 module top;
  13         wire [7:0] a = $anyconst, b = $anyconst, fdiv, fmod, a2;
  14         assign a2 = b * fdiv + fmod;
  15
  16         \$divfloor #(
  17                 .A_WIDTH(8),
  18                 .B_WIDTH(8),
  19                 .A_SIGNED(1),
  20                 .B_SIGNED(1),
  21                 .Y_WIDTH(8),
  22         ) fdiv_m (
  23                 .A(a),
  24                 .B(b),
  25                 .Y(fdiv)
  26         );
  27
  28         \$modfloor #(
  29                 .A_WIDTH(8),
  30                 .B_WIDTH(8),
  31                 .A_SIGNED(1),
  32                 .B_SIGNED(1),
  33                 .Y_WIDTH(8),
  34         ) fmod_m (
  35                 .A(a),
  36                 .B(b),
  37                 .Y(fmod)
  38         );
  39
  40         always @* begin
  41                 assume(b != 0);
  42                 assert(a == a2);
  43         end
  44 endmodule