tests/autotune/autotune_div.sby

   1 [tasks]
   2 bmc
   3 cover
   4 prove
   5
   6 [options]
   7 bmc: mode bmc
   8 cover: mode cover
   9 prove: mode prove
  10 expect pass
  11
  12 [engines]
  13 smtbmc boolector
  14
  15 [script]
  16 read -sv autotune_div.sv
  17 prep -top top
  18
  19 [file autotune_div.sv]
  20 module top #(
  21     parameter WIDTH = 4 // Reduce this if it takes too long on CI
  22 ) (
  23     input clk,
  24     input load,
  25     input [WIDTH-1:0] a,
  26     input [WIDTH-1:0] b,
  27     output reg [WIDTH-1:0] q,
  28     output reg [WIDTH-1:0] r,
  29     output reg done
  30 );
  31
  32     reg [WIDTH-1:0] a_reg = 0;
  33     reg [WIDTH-1:0] b_reg = 1;
  34
  35     initial begin
  36         q <= 0;
  37         r <= 0;
  38         done <= 1;
  39     end
  40
  41     reg [WIDTH-1:0] q_step = 1;
  42     reg [WIDTH-1:0] r_step = 1;
  43
  44     // This is not how you design a good divider circuit!
  45     always @(posedge clk) begin
  46         if (load) begin
  47             a_reg <= a;
  48             b_reg <= b;
  49             q <= 0;
  50             r <= a;
  51             q_step <= 1;
  52             r_step <= b;
  53             done <= b == 0;
  54         end else begin
  55             if (r_step <= r) begin
  56                 q <= q + q_step;
  57                 r <= r - r_step;
  58
  59                 if (!r_step[WIDTH-1]) begin
  60                     r_step <= r_step << 1;
  61                     q_step <= q_step << 1;
  62                 end
  63             end else begin
  64                 if (!q_step[0]) begin
  65                     r_step <= r_step >> 1;
  66                     q_step <= q_step >> 1;
  67                 end else begin
  68                     done <= 1;
  69                 end
  70             end
  71         end
  72     end
  73
  74     always @(posedge clk) begin
  75         assert (r_step == b_reg * q_step); // Helper invariant
  76
  77         assert (q * b_reg + r == a_reg); // Main invariant & correct output relationship
  78         if (done) assert (r <= b_reg - 1); // Output range
  79
  80         cover (done);
  81         cover (done && b_reg == 0);
  82         cover (r != a_reg);
  83         cover (r == a_reg);
  84     end
  85 endmodule