aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGELOG1
-rw-r--r--backends/smt2/Makefile.inc2
-rw-r--r--misc/launcher.c8
-rw-r--r--passes/equiv/equiv_opt.cc12
-rw-r--r--passes/opt/opt_share.cc7
-rw-r--r--passes/techmap/dff2dffs.cc29
-rw-r--r--tests/ice40/div_mod.ys2
-rw-r--r--tests/techmap/dff2dffs.ys50
-rw-r--r--tests/various/equiv_opt_multiclock.ys12
9 files changed, 110 insertions, 13 deletions
diff --git a/CHANGELOG b/CHANGELOG
index 50c611b8d..8d7dd3e19 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -39,6 +39,7 @@ Yosys 0.9 .. Yosys 0.9-dev
- Added "xilinx_srl" for Xilinx shift register extraction
- Removed "shregmap -tech xilinx" (superseded by "xilinx_srl")
- Added "_TECHMAP_WIREINIT_*_" attribute and "_TECHMAP_REMOVEINIT_*_" wire for "techmap" pass
+ - Added "-match-init" option to "dff2dffs" pass
- Added +/mul2dsp.v for decomposing wide multipliers to custom-sized ones
- Added "xilinx_dsp" for Xilinx DSP packing
- "synth_xilinx" to now infer DSP blocks (-nodsp to disable)
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index 92941d4cf..68394a909 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -16,7 +16,7 @@ yosys-smtbmc-script.py: backends/smt2/smtbmc.py
-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
- $(P) gcc -DGUI=0 -O -s -o $@ $<
+ $(P) $(CXX) -DGUI=0 -O -s -o $@ $<
# Other targets
else
TARGETS += yosys-smtbmc
diff --git a/misc/launcher.c b/misc/launcher.c
index e0d8208f1..49d6414e7 100644
--- a/misc/launcher.c
+++ b/misc/launcher.c
@@ -65,7 +65,7 @@ SOFTWARE. */
int child_pid=0;
-int fail(char *format, char *data) {
+int fail(const char *format, const char *data) {
/* Print error message to stderr and return 2 */
fprintf(stderr, format, data);
return 2;
@@ -76,7 +76,7 @@ char *quoted(char *data) {
/* We allocate twice as much space as needed to deal with worse-case
of having to escape everything. */
- char *result = calloc(ln*2+3, sizeof(char));
+ char *result = (char *)calloc(ln*2+3, sizeof(char));
char *presult = result;
*presult++ = '"';
@@ -120,7 +120,7 @@ char *loadable_exe(char *exename) {
if (!hPython) return NULL; */
/* Return the absolute filename for spawnv */
- result = calloc(MAX_PATH, sizeof(char));
+ result = (char *)calloc(MAX_PATH, sizeof(char));
strncpy(result, exename, MAX_PATH);
/*if (result) GetModuleFileNameA(hPython, result, MAX_PATH);
@@ -158,7 +158,7 @@ char **parse_argv(char *cmdline, int *argc)
{
/* Parse a command line in-place using MS C rules */
- char **result = calloc(strlen(cmdline), sizeof(char *));
+ char **result = (char **)calloc(strlen(cmdline), sizeof(char *));
char *output = cmdline;
char c;
int nb = 0;
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
index 19d1c25ac..d4c7f7953 100644
--- a/passes/equiv/equiv_opt.cc
+++ b/passes/equiv/equiv_opt.cc
@@ -46,6 +46,9 @@ struct EquivOptPass:public ScriptPass
log(" -assert\n");
log(" produce an error if the circuits are not equivalent.\n");
log("\n");
+ log(" -multiclock\n");
+ log(" run clk2fflogic before equivalence checking.\n");
+ log("\n");
log(" -undef\n");
log(" enable modelling of undef states during equiv_induct.\n");
log("\n");
@@ -55,7 +58,7 @@ struct EquivOptPass:public ScriptPass
}
std::string command, techmap_opts;
- bool assert, undef;
+ bool assert, undef, multiclock;
void clear_flags() YS_OVERRIDE
{
@@ -63,6 +66,7 @@ struct EquivOptPass:public ScriptPass
techmap_opts = "";
assert = false;
undef = false;
+ multiclock = false;
}
void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
@@ -92,6 +96,10 @@ struct EquivOptPass:public ScriptPass
undef = true;
continue;
}
+ if (args[argidx] == "-multiclock") {
+ multiclock = true;
+ continue;
+ }
break;
}
@@ -146,6 +154,8 @@ struct EquivOptPass:public ScriptPass
}
if (check_label("prove")) {
+ if (multiclock || help_mode)
+ run("clk2fflogic", "(only with -multiclock)");
run("equiv_make gold gate equiv");
if (help_mode)
run("equiv_induct [-undef] equiv");
diff --git a/passes/opt/opt_share.cc b/passes/opt/opt_share.cc
index c53fb3113..2c456705c 100644
--- a/passes/opt/opt_share.cc
+++ b/passes/opt/opt_share.cc
@@ -108,12 +108,13 @@ bool cell_supported(RTLIL::Cell *cell)
return false;
}
-std::map<IdString, IdString> mergeable_type_map{
- {ID($sub), ID($add)},
-};
+std::map<IdString, IdString> mergeable_type_map;
bool mergeable(RTLIL::Cell *a, RTLIL::Cell *b)
{
+ if (mergeable_type_map.empty()) {
+ mergeable_type_map.insert({ID($sub), ID($add)});
+ }
auto a_type = a->type;
if (mergeable_type_map.count(a_type))
a_type = mergeable_type_map.at(a_type);
diff --git a/passes/techmap/dff2dffs.cc b/passes/techmap/dff2dffs.cc
index 0ea033513..3fa1ed5cf 100644
--- a/passes/techmap/dff2dffs.cc
+++ b/passes/techmap/dff2dffs.cc
@@ -34,11 +34,16 @@ struct Dff2dffsPass : public Pass {
log("Merge synchronous set/reset $_MUX_ cells to create $__DFFS_[NP][NP][01], to be run before\n");
log("dff2dffe for SR over CE priority.\n");
log("\n");
+ log(" -match-init\n");
+ log(" Disallow merging synchronous set/reset that has polarity opposite of the\n");
+ log(" output wire's init attribute (if any).\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
log_header(design, "Executing dff2dffs pass (merge synchronous set/reset into FF cells).\n");
+ bool match_init = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
@@ -46,6 +51,10 @@ struct Dff2dffsPass : public Pass {
// singleton_mode = true;
// continue;
// }
+ if (args[argidx] == "-match-init") {
+ match_init = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
@@ -96,9 +105,6 @@ struct Dff2dffsPass : public Pass {
SigBit bit_b = sigmap(mux_cell->getPort(ID::B));
SigBit bit_s = sigmap(mux_cell->getPort(ID(S)));
- log(" Merging %s (A=%s, B=%s, S=%s) into %s (%s).\n", log_id(mux_cell),
- log_signal(bit_a), log_signal(bit_b), log_signal(bit_s), log_id(cell), log_id(cell->type));
-
SigBit sr_val, sr_sig;
bool invert_sr;
sr_sig = bit_s;
@@ -113,6 +119,23 @@ struct Dff2dffsPass : public Pass {
invert_sr = false;
}
+ if (match_init) {
+ SigBit bit_q = cell->getPort(ID(Q));
+ if (bit_q.wire) {
+ auto it = bit_q.wire->attributes.find(ID(init));
+ if (it != bit_q.wire->attributes.end()) {
+ auto init_val = it->second[bit_q.offset];
+ if (init_val == State::S1 && sr_val != State::S1)
+ continue;
+ if (init_val == State::S0 && sr_val != State::S0)
+ continue;
+ }
+ }
+ }
+
+ log(" Merging %s (A=%s, B=%s, S=%s) into %s (%s).\n", log_id(mux_cell),
+ log_signal(bit_a), log_signal(bit_b), log_signal(bit_s), log_id(cell), log_id(cell->type));
+
if (sr_val == State::S1) {
if (cell->type == ID($_DFF_N_)) {
if (invert_sr) cell->type = ID($__DFFS_NN1_);
diff --git a/tests/ice40/div_mod.ys b/tests/ice40/div_mod.ys
index 21cac7144..821d6c301 100644
--- a/tests/ice40/div_mod.ys
+++ b/tests/ice40/div_mod.ys
@@ -4,6 +4,6 @@ flatten
equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check
design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design)
cd top # Constrain all select calls below inside the top module
-select -assert-count 62 t:SB_LUT4
+select -assert-count 59 t:SB_LUT4
select -assert-count 41 t:SB_CARRY
select -assert-none t:SB_LUT4 t:SB_CARRY %% t:* %D
diff --git a/tests/techmap/dff2dffs.ys b/tests/techmap/dff2dffs.ys
new file mode 100644
index 000000000..13f1a3cf3
--- /dev/null
+++ b/tests/techmap/dff2dffs.ys
@@ -0,0 +1,50 @@
+read_verilog << EOT
+module top(...);
+input clk;
+input d;
+input sr;
+output reg q0, q1, q2, q3, q4, q5;
+
+initial q0 = 1'b0;
+initial q1 = 1'b0;
+initial q2 = 1'b1;
+initial q3 = 1'b1;
+initial q4 = 1'bx;
+initial q5 = 1'bx;
+
+always @(posedge clk) begin
+ q0 <= sr ? 1'b0 : d;
+ q1 <= sr ? 1'b1 : d;
+ q2 <= sr ? 1'b0 : d;
+ q3 <= sr ? 1'b1 : d;
+ q4 <= sr ? 1'b0 : d;
+ q5 <= sr ? 1'b1 : d;
+end
+
+endmodule
+EOT
+
+proc
+simplemap
+design -save ref
+
+dff2dffs
+clean
+
+select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q1 %x t:$__DFFS_PP1_ %i
+select -assert-count 1 w:q2 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i
+select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i
+
+design -load ref
+dff2dffs -match-init
+clean
+
+select -assert-count 1 w:q0 %x t:$__DFFS_PP0_ %i
+select -assert-count 0 w:q1 %x t:$__DFFS_PP1_ %i
+select -assert-count 0 w:q2 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q3 %x t:$__DFFS_PP1_ %i
+select -assert-count 1 w:q4 %x t:$__DFFS_PP0_ %i
+select -assert-count 1 w:q5 %x t:$__DFFS_PP1_ %i
diff --git a/tests/various/equiv_opt_multiclock.ys b/tests/various/equiv_opt_multiclock.ys
new file mode 100644
index 000000000..81e36d018
--- /dev/null
+++ b/tests/various/equiv_opt_multiclock.ys
@@ -0,0 +1,12 @@
+read_verilog <<EOT
+module top(input clk, pre, d, output reg q);
+ always @(posedge clk, posedge pre)
+ if (pre)
+ q <= 1'b1;
+ else
+ q <= d;
+endmodule
+EOT
+
+prep
+equiv_opt -assert -multiclock -map +/simcells.v synth
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-03 13:46:58 +0000