aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/smt2/smt2.cc15
-rw-r--r--passes/pmgen/Makefile.inc4
-rw-r--r--passes/pmgen/pmgen.py6
-rw-r--r--passes/sat/Makefile.inc1
-rw-r--r--passes/sat/supercover.cc92
-rw-r--r--passes/techmap/dfflibmap.cc4
-rw-r--r--passes/techmap/flowmap.cc4
-rw-r--r--techlibs/ecp5/cells_sim.v4
-rw-r--r--techlibs/greenpak4/cells_map.v44
9 files changed, 138 insertions, 36 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 418f8d766..7f3cc94ca 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1103,20 +1103,27 @@ struct Smt2Worker
break;
Const initword = init_data.extract(i*width, width, State::Sx);
+ Const initmask = initword;
bool gen_init_constr = false;
- for (auto bit : initword.bits)
- if (bit == State::S0 || bit == State::S1)
+ for (int k = 0; k < GetSize(initword); k++) {
+ if (initword[k] == State::S0 || initword[k] == State::S1) {
gen_init_constr = true;
+ initmask[k] = State::S1;
+ } else {
+ initmask[k] = State::S0;
+ initword[k] = State::S0;
+ }
+ }
if (gen_init_constr)
{
if (statebv)
/* FIXME */;
else
- init_list.push_back(stringf("(= (select (|%s#%d#0| state) #b%s) #b%s) ; %s[%d]",
+ init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
get_id(module), arrayid, Const(i, abits).as_string().c_str(),
- initword.as_string().c_str(), get_id(cell), i));
+ initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
}
}
}
diff --git a/passes/pmgen/Makefile.inc b/passes/pmgen/Makefile.inc
index 33baaca30..b9682612b 100644
--- a/passes/pmgen/Makefile.inc
+++ b/passes/pmgen/Makefile.inc
@@ -4,5 +4,5 @@ passes/pmgen/ice40_dsp.o: passes/pmgen/ice40_dsp_pm.h
EXTRA_OBJS += passes/pmgen/ice40_dsp_pm.h
.SECONDARY: passes/pmgen/ice40_dsp_pm.h
-passes/pmgen/ice40_dsp_pm.h: passes/pmgen/ice40_dsp.pmg passes/pmgen/pmgen.py
- $(P) cd passes/pmgen && python3 pmgen.py ice40_dsp
+passes/pmgen/ice40_dsp_pm.h: passes/pmgen/pmgen.py passes/pmgen/ice40_dsp.pmg
+ $(P) mkdir -p passes/pmgen && cd passes/pmgen && python3 $^
diff --git a/passes/pmgen/pmgen.py b/passes/pmgen/pmgen.py
index e688a4567..166d3963a 100644
--- a/passes/pmgen/pmgen.py
+++ b/passes/pmgen/pmgen.py
@@ -6,7 +6,9 @@ import pprint
pp = pprint.PrettyPrinter(indent=4)
-prefix = sys.argv[1]
+pmgfile = sys.argv[1]
+prefix = pmgfile.split("/")[-1]
+prefix = prefix.split(".")[0]
state_types = dict()
udata_types = dict()
@@ -73,7 +75,7 @@ def rewrite_cpp(s):
return "".join(t)
-with open("%s.pmg" % prefix, "r") as f:
+with open(pmgfile, "r") as f:
while True:
line = f.readline()
if line == "": break
diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc
index 8ab0280c0..6cb1ea644 100644
--- a/passes/sat/Makefile.inc
+++ b/passes/sat/Makefile.inc
@@ -8,4 +8,5 @@ OBJS += passes/sat/expose.o
OBJS += passes/sat/assertpmux.o
OBJS += passes/sat/clk2fflogic.o
OBJS += passes/sat/async2sync.o
+OBJS += passes/sat/supercover.o
diff --git a/passes/sat/supercover.cc b/passes/sat/supercover.cc
new file mode 100644
index 000000000..ba44f02d8
--- /dev/null
+++ b/passes/sat/supercover.cc
@@ -0,0 +1,92 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct SupercoverPass : public Pass {
+ SupercoverPass() : Pass("supercover", "add hi/lo cover cells for each wire bit") { }
+ void help() YS_OVERRIDE
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" supercover [options] [selection]\n");
+ log("\n");
+ log("This command adds two cover cells for each bit of each selected wire, one\n");
+ log("checking for a hi signal level and one checking for lo level.\n");
+ log("\n");
+ }
+ void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
+ {
+ // bool flag_noinit = false;
+
+ log_header(design, "Executing SUPERCOVER pass.\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++)
+ {
+ // if (args[argidx] == "-noinit") {
+ // flag_noinit = true;
+ // continue;
+ // }
+ break;
+ }
+ extra_args(args, argidx, design);
+
+ for (auto module : design->selected_modules())
+ {
+ SigMap sigmap(module);
+ pool<SigBit> handled_bits;
+
+ int cnt_wire = 0, cnt_bits = 0;
+ log("Adding cover cells to module %s.\n", log_id(module));
+ for (auto wire : module->selected_wires())
+ {
+ bool counted_wire = false;
+ std::string src = wire->get_src_attribute();
+
+ for (auto bit : sigmap(SigSpec(wire)))
+ {
+ if (bit.wire == nullptr)
+ continue;
+
+ if (handled_bits.count(bit))
+ continue;
+
+ SigSpec inv = module->Not(NEW_ID, bit);
+ module->addCover(NEW_ID, bit, State::S1, src);
+ module->addCover(NEW_ID, inv, State::S1, src);
+
+ handled_bits.insert(bit);
+ if (!counted_wire) {
+ counted_wire = false;
+ cnt_wire++;
+ }
+ cnt_bits++;
+ }
+ }
+ log(" added cover cells to %d wires, %d bits.\n", cnt_wire, cnt_bits);
+ }
+ }
+} SupercoverPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc
index b0528d473..274177a68 100644
--- a/passes/techmap/dfflibmap.cc
+++ b/passes/techmap/dfflibmap.cc
@@ -660,8 +660,8 @@ struct DfflibmapPass : public Pass {
map_adff_to_dff("$_DFF_PP0_", "$_DFF_P_");
map_adff_to_dff("$_DFF_PP1_", "$_DFF_P_");
- log(" final dff cell mappings:\n");
- logmap_all();
+ log(" final dff cell mappings:\n");
+ logmap_all();
for (auto &it : design->modules_)
if (design->selected(it.second) && !it.second->get_bool_attribute("\\blackbox"))
diff --git a/passes/techmap/flowmap.cc b/passes/techmap/flowmap.cc
index ddbd7bf5d..0b7931e48 100644
--- a/passes/techmap/flowmap.cc
+++ b/passes/techmap/flowmap.cc
@@ -132,9 +132,9 @@ static void dump_dot_graph(string filename,
pool<RTLIL::SigBit> nodes, dict<RTLIL::SigBit, pool<RTLIL::SigBit>> edges,
pool<RTLIL::SigBit> inputs, pool<RTLIL::SigBit> outputs,
std::function<GraphStyle(RTLIL::SigBit)> node_style =
- [](RTLIL::SigBit) { return GraphStyle{}; },
+ [](RTLIL::SigBit) { return GraphStyle{}; },
std::function<GraphStyle(RTLIL::SigBit, RTLIL::SigBit)> edge_style =
- [](RTLIL::SigBit, RTLIL::SigBit) { return GraphStyle{}; },
+ [](RTLIL::SigBit, RTLIL::SigBit) { return GraphStyle{}; },
string name = "")
{
FILE *f = fopen(filename.c_str(), "w");
diff --git a/techlibs/ecp5/cells_sim.v b/techlibs/ecp5/cells_sim.v
index 507ab1beb..f27540bd7 100644
--- a/techlibs/ecp5/cells_sim.v
+++ b/techlibs/ecp5/cells_sim.v
@@ -57,7 +57,7 @@ module TRELLIS_RAM16X2 (
input RAD0, RAD1, RAD2, RAD3,
output DO0, DO1
);
- parameter WCKMUX = "WCK";
+ parameter WCKMUX = "WCK";
parameter WREMUX = "WRE";
parameter INITVAL_0 = 16'h0000;
parameter INITVAL_1 = 16'h0000;
@@ -104,7 +104,7 @@ module TRELLIS_DPR16X4 (
input [3:0] RAD,
output [3:0] DO
);
- parameter WCKMUX = "WCK";
+ parameter WCKMUX = "WCK";
parameter WREMUX = "WRE";
parameter [63:0] INITVAL = 64'h0000000000000000;
diff --git a/techlibs/greenpak4/cells_map.v b/techlibs/greenpak4/cells_map.v
index b971a51fa..51c85183d 100644
--- a/techlibs/greenpak4/cells_map.v
+++ b/techlibs/greenpak4/cells_map.v
@@ -112,14 +112,14 @@ module GP_OBUFT(input IN, input OE, output OUT);
endmodule
module \$lut (A, Y);
- parameter WIDTH = 0;
- parameter LUT = 0;
+ parameter WIDTH = 0;
+ parameter LUT = 0;
- input [WIDTH-1:0] A;
- output Y;
+ input [WIDTH-1:0] A;
+ output Y;
- generate
- if (WIDTH == 1) begin
+ generate
+ if (WIDTH == 1) begin
if(LUT == 2'b01) begin
GP_INV _TECHMAP_REPLACE_ (.OUT(Y), .IN(A[0]) );
end
@@ -127,22 +127,22 @@ module \$lut (A, Y);
GP_2LUT #(.INIT({2'b00, LUT})) _TECHMAP_REPLACE_ (.OUT(Y),
.IN0(A[0]), .IN1(1'b0));
end
- end else
- if (WIDTH == 2) begin
- GP_2LUT #(.INIT(LUT)) _TECHMAP_REPLACE_ (.OUT(Y),
- .IN0(A[0]), .IN1(A[1]));
- end else
- if (WIDTH == 3) begin
- GP_3LUT #(.INIT(LUT)) _TECHMAP_REPLACE_ (.OUT(Y),
- .IN0(A[0]), .IN1(A[1]), .IN2(A[2]));
- end else
- if (WIDTH == 4) begin
- GP_4LUT #(.INIT(LUT)) _TECHMAP_REPLACE_ (.OUT(Y),
- .IN0(A[0]), .IN1(A[1]), .IN2(A[2]), .IN3(A[3]));
- end else begin
- wire _TECHMAP_FAIL_ = 1;
- end
- endgenerate
+ end else
+ if (WIDTH == 2) begin
+ GP_2LUT #(.INIT(LUT)) _TECHMAP_REPLACE_ (.OUT(Y),
+ .IN0(A[0]), .IN1(A[1]));
+ end else
+ if (WIDTH == 3) begin
+ GP_3LUT #(.INIT(LUT)) _TECHMAP_REPLACE_ (.OUT(Y),
+ .IN0(A[0]), .IN1(A[1]), .IN2(A[2]));
+ end else
+ if (WIDTH == 4) begin
+ GP_4LUT #(.INIT(LUT)) _TECHMAP_REPLACE_ (.OUT(Y),
+ .IN0(A[0]), .IN1(A[1]), .IN2(A[2]), .IN3(A[3]));
+ end else begin
+ wire _TECHMAP_FAIL_ = 1;
+ end
+ endgenerate
endmodule
module \$__COUNT_ (CE, CLK, OUT, POUT, RST, UP);
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-23 00:38:06 +0000