Implemented same div-by-zero behavior as found in other synthesis tools

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 5b4abfc215023696ab65fd5d7f4a54f45a76d0db..27063776ebcff2b4cad3a6b4060797cde1560a98 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -300,20 +300,43 @@ struct SatGen
                                chain_buf.erase(chain_buf.begin() + a_u.size(), chain_buf.end());
                        }
 
+                       std::vector<int> y_tmp = ignore_div_by_zero ? y : ez->vec_var(y.size());
                        if (cell->type == "$div") {
                                if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
-                                       ez->assume(ez->vec_eq(y, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
+                                       ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(ez->XOR(a.back(), b.back()), ez->vec_neg(y_u), y_u)));
                                else
-                                       ez->assume(ez->vec_eq(y, y_u));
+                                       ez->assume(ez->vec_eq(y_tmp, y_u));
                        } else {
                                if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
-                                       ez->assume(ez->vec_eq(y, ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf)));
+                                       ez->assume(ez->vec_eq(y_tmp, ez->vec_ite(a.back(), ez->vec_neg(chain_buf), chain_buf)));
                                else
-                                       ez->assume(ez->vec_eq(y, chain_buf));
+                                       ez->assume(ez->vec_eq(y_tmp, chain_buf));
                        }
 
-                       if (ignore_div_by_zero)
+                       if (ignore_div_by_zero) {
                                ez->assume(ez->expression(ezSAT::OpOr, b));
+                       } else {
+                               std::vector<int> div_zero_result;
+                               if (cell->type == "$div") {
+                                       if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool()) {
+                                               std::vector<int> all_ones(y.size(), ez->TRUE);
+                                               std::vector<int> only_first_one(y.size(), ez->FALSE);
+                                               only_first_one.at(0) = ez->TRUE;
+                                               div_zero_result = ez->vec_ite(a.back(), only_first_one, all_ones);
+                                       } else {
+                                               div_zero_result.insert(div_zero_result.end(), cell->connections.at("\\A").width, ez->TRUE);
+                                               div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->FALSE);
+                                       }
+                               } else {
+                                       int copy_a_bits = std::min(cell->connections.at("\\A").width, cell->connections.at("\\B").width);
+                                       div_zero_result.insert(div_zero_result.end(), a.begin(), a.begin() + copy_a_bits);
+                                       if (cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool())
+                                               div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), div_zero_result.back());
+                                       else
+                                               div_zero_result.insert(div_zero_result.end(), y.size() - div_zero_result.size(), ez->FALSE);
+                               }
+                               ez->assume(ez->vec_eq(y, ez->vec_ite(ez->expression(ezSAT::OpOr, b), y_tmp, div_zero_result)));
+                       }
 
                        return true;
                }

diff --git a/techlibs/stdcells.v b/techlibs/stdcells.v
index c411ba35bb1bb82df10abe7c6a7b5f645f6f4df5..d861d796ef95d893276241f7f46b719be2c9aba2 100644 (file)
--- a/techlibs/stdcells.v
+++ b/techlibs/stdcells.v
@@ -1077,6 +1077,9 @@ input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
 output [Y_WIDTH-1:0] Y;
 
+wire [Y_WIDTH-1:0] Y_buf;
+wire [Y_WIDTH-1:0] Y_div_zero;
+
 \$div_mod #(
        .A_SIGNED(A_SIGNED),
        .B_SIGNED(B_SIGNED),
@@ -1086,9 +1089,20 @@ output [Y_WIDTH-1:0] Y;
 ) div_mod (
        .A(A),
        .B(B),
-       .Y(Y)
+       .Y(Y_buf)
 );
 
+// explicitly force the division-by-zero behavior found in other synthesis tools 
+generate begin
+       if (A_SIGNED && B_SIGNED) begin:make_div_zero
+               assign Y_div_zero = A[A_WIDTH-1] ? {Y_WIDTH{1'b0}} | 1'b1 : {Y_WIDTH{1'b1}};
+       end else begin:make_div_zero
+               assign Y_div_zero = {A_WIDTH{1'b1}};
+       end
+end endgenerate
+
+assign Y = B ? Y_buf : Y_div_zero;
+
 endmodule
 
 // --------------------------------------------------------
@@ -1105,6 +1119,9 @@ input [A_WIDTH-1:0] A;
 input [B_WIDTH-1:0] B;
 output [Y_WIDTH-1:0] Y;
 
+wire [Y_WIDTH-1:0] Y_buf;
+wire [Y_WIDTH-1:0] Y_div_zero;
+
 \$div_mod #(
        .A_SIGNED(A_SIGNED),
        .B_SIGNED(B_SIGNED),
@@ -1114,9 +1131,21 @@ output [Y_WIDTH-1:0] Y;
 ) div_mod (
        .A(A),
        .B(B),
-       .R(Y)
+       .R(Y_buf)
 );
 
+// explicitly force the division-by-zero behavior found in other synthesis tools 
+localparam div_zero_copy_a_bits = A_WIDTH < B_WIDTH ? A_WIDTH : B_WIDTH;
+generate begin
+       if (A_SIGNED && B_SIGNED) begin:make_div_zero
+               assign Y_div_zero = $signed(A[div_zero_copy_a_bits-1:0]);
+       end else begin:make_div_zero
+               assign Y_div_zero = $unsigned(A[div_zero_copy_a_bits-1:0]);
+       end
+end endgenerate
+
+assign Y = B ? Y_buf : Y_div_zero;
+
 endmodule
 
 /****