Added $macc SAT model

diff --git a/kernel/satgen.h b/kernel/satgen.h
index ae155a2eb9fe8cc0ae97b4cb5fc79eaf1454bbbe..3429f8239acb100472134deb15138cc82c7ea382 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -23,6 +23,7 @@
 #include "kernel/rtlil.h"
 #include "kernel/sigtools.h"
 #include "kernel/celltypes.h"
+#include "kernel/macc.h"
 
 #include "libs/ezsat/ezminisat.h"
 typedef ezMiniSAT ezDefaultSAT;
@@ -762,6 +763,76 @@ struct SatGen
                        return true;
                }
 
+               if (cell->type == "$macc")
+               {
+                       std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
+                       std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
+                       std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
+
+                       Macc macc;
+                       macc.from_cell(cell);
+
+                       std::vector<int> tmp(SIZE(y), ez->FALSE);
+
+                       for (auto &port : macc.ports)
+                       {
+                               std::vector<int> in_a = importDefSigSpec(port.in_a, timestep);
+                               std::vector<int> in_b = importDefSigSpec(port.in_b, timestep);
+
+                               while (SIZE(in_a) < SIZE(y))
+                                       in_a.push_back(port.is_signed && !in_a.empty() ? in_a.back() : ez->FALSE);
+                               in_a.resize(SIZE(y));
+
+                               if (SIZE(in_b))
+                               {
+                                       while (SIZE(in_b) < SIZE(y))
+                                               in_b.push_back(port.is_signed && !in_b.empty() ? in_b.back() : ez->FALSE);
+                                       in_b.resize(SIZE(y));
+
+                                       for (int i = 0; i < SIZE(in_b); i++) {
+                                               std::vector<int> shifted_a(in_a.size(), ez->FALSE);
+                                               for (int j = i; j < int(in_a.size()); j++)
+                                                       shifted_a.at(j) = in_a.at(j-i);
+                                               if (port.do_subtract)
+                                                       tmp = ez->vec_ite(in_b.at(i), ez->vec_sub(tmp, shifted_a), tmp);
+                                               else
+                                                       tmp = ez->vec_ite(in_b.at(i), ez->vec_add(tmp, shifted_a), tmp);
+                                       }
+                               }
+                               else
+                               {
+                                       if (port.do_subtract)
+                                               tmp = ez->vec_sub(tmp, in_a);
+                                       else
+                                               tmp = ez->vec_add(tmp, in_a);
+                               }
+                       }
+
+                       for (int i = 0; i < SIZE(b); i++) {
+                               std::vector<int> val(SIZE(y), ez->FALSE);
+                               val.at(0) = b.at(i);
+                               tmp = ez->vec_add(tmp, val);
+                       }
+
+                       if (model_undef)
+                       {
+                               std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
+                               std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
+
+                               int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);
+                               int undef_any_b = ez->expression(ezSAT::OpOr, undef_b);
+
+                               std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
+                               ez->assume(ez->vec_eq(undef_y, std::vector<int>(SIZE(y), ez->OR(undef_any_a, undef_any_b))));
+
+                               undefGating(y, tmp, undef_y);
+                       }
+                       else
+                               ez->assume(ez->vec_eq(y, tmp));
+
+                       return true;
+               }
+
                if (cell->type == "$div" || cell->type == "$mod")
                {
                        std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);

diff --git a/passes/tests/test_cell.cc b/passes/tests/test_cell.cc
index 96f08de4b49b41db3f91d3a532189618136b3bdb..edab51eb2f1c1c9dc46c4345b226660fceb99028 100644 (file)
--- a/passes/tests/test_cell.cc
+++ b/passes/tests/test_cell.cc
@@ -42,9 +42,9 @@ static void create_gold_module(RTLIL::Design *design, RTLIL::IdString cell_type,
        if (cell_type == "$macc")
        {
                Macc macc;
-               int width = 1 + xorshift32(16);
+               int width = 1 + xorshift32(8);
                int depth = 1 + xorshift32(6);
-               int mulbits = 0;
+               int mulbits_a = 0, mulbits_b = 0;
 
                RTLIL::Wire *wire_a = module->addWire("\\A");
                wire_a->width = 0;
@@ -55,10 +55,11 @@ static void create_gold_module(RTLIL::Design *design, RTLIL::IdString cell_type,
                        int size_a = xorshift32(width) + 1;
                        int size_b = xorshift32(width) + 1;
 
-                       if (mulbits + size_a*size_b > 256 || xorshift32(2) == 1)
+                       if (mulbits_a + size_a*size_b <= 96 && mulbits_b + size_a + size_b <= 16 && xorshift32(2) == 1) {
+                               mulbits_a += size_a * size_b;
+                               mulbits_b += size_a + size_b;
+                       } else
                                size_b = 0;
-                       else
-                               mulbits += size_a*size_b;
 
                        Macc::port_t this_port;
 

diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index eabd6595177e664f801724864184e708086a9708..b1f871d9b8685f6ff804cefc6312790d72b36b36 100644 (file)
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -771,16 +771,16 @@ module \$macc (A, B, Y);
        localparam integer num_abits = $clog2(A_WIDTH);
 
        function [2*num_ports*num_abits-1:0] get_port_offsets;
-               input [CONFIG_WIDTH-1:0] CONFIG;
+               input [CONFIG_WIDTH-1:0] cfg;
                integer i, cursor;
                begin
                        cursor = 0;
                        get_port_offsets = 0;
                        for (i = 0; i < num_ports; i = i+1) begin
                                get_port_offsets[(2*i + 0)*num_abits +: num_abits] = cursor;
-                               cursor = cursor + CONFIG[4 + i*(2 + 2*num_bits) + 2 +: num_bits];
+                               cursor = cursor + cfg[4 + i*(2 + 2*num_bits) + 2 +: num_bits];
                                get_port_offsets[(2*i + 1)*num_abits +: num_abits] = cursor;
-                               cursor = cursor + CONFIG[4 + i*(2 + 2*num_bits) + 2 + num_bits +: num_bits];
+                               cursor = cursor + cfg[4 + i*(2 + 2*num_bits) + 2 + num_bits +: num_bits];
                        end
                end
        endfunction

diff --git a/techlibs/common/techmap.v b/techlibs/common/techmap.v
index 8237a737295284375518a7ff310abd891251b834..f0397858f98d69d7262bb2707a204e55efe8aa21 100644 (file)
--- a/techlibs/common/techmap.v
+++ b/techlibs/common/techmap.v
@@ -597,16 +597,16 @@ module \$macc (A, B, Y);
        localparam integer num_abits = $clog2(A_WIDTH);
 
        function [2*num_ports*num_abits-1:0] get_port_offsets;
-               input [CONFIG_WIDTH-1:0] CONFIG;
+               input [CONFIG_WIDTH-1:0] cfg;
                integer i, cursor;
                begin
                        cursor = 0;
                        get_port_offsets = 0;
                        for (i = 0; i < num_ports; i = i+1) begin
                                get_port_offsets[(2*i + 0)*num_abits +: num_abits] = cursor;
-                               cursor = cursor + CONFIG[4 + i*(2 + 2*num_bits) + 2 +: num_bits];
+                               cursor = cursor + cfg[4 + i*(2 + 2*num_bits) + 2 +: num_bits];
                                get_port_offsets[(2*i + 1)*num_abits +: num_abits] = cursor;
-                               cursor = cursor + CONFIG[4 + i*(2 + 2*num_bits) + 2 + num_bits +: num_bits];
+                               cursor = cursor + cfg[4 + i*(2 + 2*num_bits) + 2 + num_bits +: num_bits];
                        end
                end
        endfunction