tests/unsorted/floor_divmod.sby

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