From: Clifford Wolf Date: Sat, 6 Sep 2014 17:44:11 +0000 (+0200) Subject: Added $macc SAT model X-Git-Tag: yosys-0.4~155 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa64942018a39085301d7f24832ad0ad7b0d22f1;p=yosys.git Added $macc SAT model --- diff --git a/kernel/satgen.h b/kernel/satgen.h index ae155a2eb..3429f8239 100644 --- 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 a = importDefSigSpec(cell->getPort("\\A"), timestep); + std::vector b = importDefSigSpec(cell->getPort("\\B"), timestep); + std::vector y = importDefSigSpec(cell->getPort("\\Y"), timestep); + + Macc macc; + macc.from_cell(cell); + + std::vector tmp(SIZE(y), ez->FALSE); + + for (auto &port : macc.ports) + { + std::vector in_a = importDefSigSpec(port.in_a, timestep); + std::vector 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 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 val(SIZE(y), ez->FALSE); + val.at(0) = b.at(i); + tmp = ez->vec_add(tmp, val); + } + + if (model_undef) + { + std::vector undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep); + std::vector 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 undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep); + ez->assume(ez->vec_eq(undef_y, std::vector(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 a = importDefSigSpec(cell->getPort("\\A"), timestep); diff --git a/passes/tests/test_cell.cc b/passes/tests/test_cell.cc index 96f08de4b..edab51eb2 100644 --- 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 eabd65951..b1f871d9b 100644 --- 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 8237a7372..f0397858f 100644 --- 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