aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile10
-rw-r--r--kernel/celltypes.h9
-rw-r--r--passes/opt/opt.cc8
-rw-r--r--passes/opt/opt_rmdff.cc109
-rwxr-xr-xtests/aiger/run-test.sh14
-rwxr-xr-xtests/memories/run-test.sh6
-rw-r--r--tests/opt/opt_ff_sat.v12
-rw-r--r--tests/opt/opt_ff_sat.ys5
-rwxr-xr-xtests/tools/autotest.sh7
9 files changed, 156 insertions, 24 deletions
diff --git a/Makefile b/Makefile
index 6c5a436c1..d33f27b63 100644
--- a/Makefile
+++ b/Makefile
@@ -666,6 +666,12 @@ else
SEEDOPT=""
endif
+ifneq ($(ABCEXTERNAL),)
+ABCOPT="-A $(ABCEXTERNAL)"
+else
+ABCOPT=""
+endif
+
test: $(TARGETS) $(EXTRA_TARGETS)
+cd tests/simple && bash run-test.sh $(SEEDOPT)
+cd tests/hana && bash run-test.sh $(SEEDOPT)
@@ -674,13 +680,13 @@ test: $(TARGETS) $(EXTRA_TARGETS)
+cd tests/share && bash run-test.sh $(SEEDOPT)
+cd tests/fsm && bash run-test.sh $(SEEDOPT)
+cd tests/techmap && bash run-test.sh
- +cd tests/memories && bash run-test.sh $(SEEDOPT)
+ +cd tests/memories && bash run-test.sh $(ABCOPT) $(SEEDOPT)
+cd tests/bram && bash run-test.sh $(SEEDOPT)
+cd tests/various && bash run-test.sh
+cd tests/sat && bash run-test.sh
+cd tests/svinterfaces && bash run-test.sh $(SEEDOPT)
+cd tests/opt && bash run-test.sh
- +cd tests/aiger && bash run-test.sh
+ +cd tests/aiger && bash run-test.sh $(ABCOPT)
+cd tests/arch && bash run-test.sh
+cd tests/simple_abc9 && bash run-test.sh $(SEEDOPT)
@echo ""
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 4e91eddda..758661c02 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -246,24 +246,24 @@ struct CellTypes
cell_types.clear();
}
- bool cell_known(RTLIL::IdString type)
+ bool cell_known(RTLIL::IdString type) const
{
return cell_types.count(type) != 0;
}
- bool cell_output(RTLIL::IdString type, RTLIL::IdString port)
+ bool cell_output(RTLIL::IdString type, RTLIL::IdString port) const
{
auto it = cell_types.find(type);
return it != cell_types.end() && it->second.outputs.count(port) != 0;
}
- bool cell_input(RTLIL::IdString type, RTLIL::IdString port)
+ bool cell_input(RTLIL::IdString type, RTLIL::IdString port) const
{
auto it = cell_types.find(type);
return it != cell_types.end() && it->second.inputs.count(port) != 0;
}
- bool cell_evaluable(RTLIL::IdString type)
+ bool cell_evaluable(RTLIL::IdString type) const
{
auto it = cell_types.find(type);
return it != cell_types.end() && it->second.is_evaluable;
@@ -482,4 +482,3 @@ extern CellTypes yosys_celltypes;
YOSYS_NAMESPACE_END
#endif
-
diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc
index a4aca2fee..e9a43e0f3 100644
--- a/passes/opt/opt.cc
+++ b/passes/opt/opt.cc
@@ -44,7 +44,7 @@ struct OptPass : public Pass {
log(" opt_muxtree\n");
log(" opt_reduce [-fine] [-full]\n");
log(" opt_merge [-share_all]\n");
- log(" opt_rmdff [-keepdc]\n");
+ log(" opt_rmdff [-keepdc] [-sat]\n");
log(" opt_clean [-purge]\n");
log(" opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
log(" while <changed design>\n");
@@ -54,7 +54,7 @@ struct OptPass : public Pass {
log(" do\n");
log(" opt_expr [-mux_undef] [-mux_bool] [-undriven] [-clkinv] [-fine] [-full] [-keepdc]\n");
log(" opt_merge [-share_all]\n");
- log(" opt_rmdff [-keepdc]\n");
+ log(" opt_rmdff [-keepdc] [-sat]\n");
log(" opt_clean [-purge]\n");
log(" while <changed design in opt_rmdff>\n");
log("\n");
@@ -112,6 +112,10 @@ struct OptPass : public Pass {
opt_rmdff_args += " -keepdc";
continue;
}
+ if (args[argidx] == "-sat") {
+ opt_rmdff_args += " -sat";
+ continue;
+ }
if (args[argidx] == "-share_all") {
opt_merge_args += " -share_all";
continue;
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index eeb992a3e..be6ac2d30 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -17,19 +17,24 @@
*
*/
+#include "kernel/log.h"
#include "kernel/register.h"
+#include "kernel/rtlil.h"
+#include "kernel/satgen.h"
#include "kernel/sigtools.h"
-#include "kernel/log.h"
-#include <stdlib.h>
#include <stdio.h>
+#include <stdlib.h>
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
SigMap assign_map, dff_init_map;
SigSet<RTLIL::Cell*> mux_drivers;
+dict<SigBit, RTLIL::Cell*> bit2driver;
dict<SigBit, pool<SigBit>> init_attributes;
+
bool keepdc;
+bool sat;
void remove_init_attr(SigSpec sig)
{
@@ -452,12 +457,84 @@ bool handle_dff(RTLIL::Module *mod, RTLIL::Cell *dff)
dff->unsetPort("\\E");
}
+ if (sat && has_init && (!sig_r.size() || val_init == val_rv))
+ {
+ bool removed_sigbits = false;
+
+ ezSatPtr ez;
+ SatGen satgen(ez.get(), &assign_map);
+ pool<Cell*> sat_cells;
+
+ std::function<void(Cell*)> sat_import_cell = [&](Cell *c) {
+ if (!sat_cells.insert(c).second)
+ return;
+ if (!satgen.importCell(c))
+ return;
+ for (auto &conn : c->connections()) {
+ if (!c->input(conn.first))
+ continue;
+ for (auto bit : assign_map(conn.second))
+ if (bit2driver.count(bit))
+ sat_import_cell(bit2driver.at(bit));
+ }
+ };
+
+ // For each register bit, try to prove that it cannot change from the initial value. If so, remove it
+ for (int position = 0; position < GetSize(sig_d); position += 1) {
+ RTLIL::SigBit q_sigbit = sig_q[position];
+ RTLIL::SigBit d_sigbit = sig_d[position];
+
+ if ((!q_sigbit.wire) || (!d_sigbit.wire))
+ continue;
+
+ if (!bit2driver.count(d_sigbit))
+ continue;
+
+ sat_import_cell(bit2driver.at(d_sigbit));
+
+ RTLIL::State sigbit_init_val = val_init[position];
+ if (sigbit_init_val != State::S0 && sigbit_init_val != State::S1)
+ continue;
+
+ int init_sat_pi = satgen.importSigSpec(sigbit_init_val).front();
+ int q_sat_pi = satgen.importSigBit(q_sigbit);
+ int d_sat_pi = satgen.importSigBit(d_sigbit);
+
+ // Try to find out whether the register bit can change under some circumstances
+ bool counter_example_found = ez->solve(ez->IFF(q_sat_pi, init_sat_pi), ez->NOT(ez->IFF(d_sat_pi, init_sat_pi)));
+
+ // If the register bit cannot change, we can replace it with a constant
+ if (!counter_example_found)
+ {
+ log("Setting constant %d-bit at position %d on %s (%s) from module %s.\n", sigbit_init_val ? 1 : 0,
+ position, log_id(dff), log_id(dff->type), log_id(mod));
+
+ SigSpec tmp = dff->getPort("\\D");
+ tmp[position] = sigbit_init_val;
+ dff->setPort("\\D", tmp);
+
+ removed_sigbits = true;
+ }
+ }
+
+ if (removed_sigbits) {
+ handle_dff(mod, dff);
+ return true;
+ }
+ }
+
+
return false;
delete_dff:
log("Removing %s (%s) from module %s.\n", log_id(dff), log_id(dff->type), log_id(mod));
remove_init_attr(dff->getPort("\\Q"));
mod->remove(dff);
+
+ for (auto &entry : bit2driver)
+ if (entry.second == dff)
+ bit2driver.erase(entry.first);
+
return true;
}
@@ -467,11 +544,15 @@ struct OptRmdffPass : public Pass {
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
- log(" opt_rmdff [-keepdc] [selection]\n");
+ log(" opt_rmdff [-keepdc] [-sat] [selection]\n");
log("\n");
log("This pass identifies flip-flops with constant inputs and replaces them with\n");
log("a constant driver.\n");
log("\n");
+ log(" -sat\n");
+ log(" additionally invoke SAT solver to detect and remove flip-flops (with \n");
+ log(" non-constant inputs) that can also be replaced with a constant driver\n");
+ log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
{
@@ -479,6 +560,7 @@ struct OptRmdffPass : public Pass {
log_header(design, "Executing OPT_RMDFF pass (remove dff with constant values).\n");
keepdc = false;
+ sat = false;
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
@@ -486,18 +568,22 @@ struct OptRmdffPass : public Pass {
keepdc = true;
continue;
}
+ if (args[argidx] == "-sat") {
+ sat = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
- for (auto module : design->selected_modules())
- {
+ for (auto module : design->selected_modules()) {
pool<SigBit> driven_bits;
dict<SigBit, State> init_bits;
assign_map.set(module);
dff_init_map.set(module);
mux_drivers.clear();
+ bit2driver.clear();
init_attributes.clear();
for (auto wire : module->wires())
@@ -522,17 +608,21 @@ struct OptRmdffPass : public Pass {
driven_bits.insert(bit);
}
}
- mux_drivers.clear();
std::vector<RTLIL::IdString> dff_list;
std::vector<RTLIL::IdString> dffsr_list;
std::vector<RTLIL::IdString> dlatch_list;
for (auto cell : module->cells())
{
- for (auto &conn : cell->connections())
- if (cell->output(conn.first) || !cell->known())
- for (auto bit : assign_map(conn.second))
+ for (auto &conn : cell->connections()) {
+ bool is_output = cell->output(conn.first);
+ if (is_output || !cell->known())
+ for (auto bit : assign_map(conn.second)) {
+ if (is_output)
+ bit2driver[bit] = cell;
driven_bits.insert(bit);
+ }
+ }
if (cell->type == "$mux" || cell->type == "$pmux") {
if (cell->getPort("\\A").size() == cell->getPort("\\B").size())
@@ -604,6 +694,7 @@ struct OptRmdffPass : public Pass {
assign_map.clear();
mux_drivers.clear();
+ bit2driver.clear();
init_attributes.clear();
if (total_count || total_initdrv)
diff --git a/tests/aiger/run-test.sh b/tests/aiger/run-test.sh
index 5246c1b48..deaf48a3d 100755
--- a/tests/aiger/run-test.sh
+++ b/tests/aiger/run-test.sh
@@ -2,6 +2,16 @@
set -e
+OPTIND=1
+abcprog="../../yosys-abc" # default to built-in version of abc
+while getopts "A:" opt
+do
+ case "$opt" in
+ A) abcprog="$OPTARG" ;;
+ esac
+done
+shift "$((OPTIND-1))"
+
# NB: *.aag and *.aig must contain a symbol table naming the primary
# inputs and outputs, otherwise ABC and Yosys will name them
# arbitrarily (and inconsistently with each other).
@@ -11,7 +21,7 @@ for aag in *.aag; do
# (which would have been created by the reference aig2aig utility,
# available from http://fmv.jku.at/aiger/)
echo "Checking $aag."
- ../../yosys-abc -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
+ $abcprog -q "read -c ${aag%.*}.aig; write ${aag%.*}_ref.v"
../../yosys -qp "
read_verilog ${aag%.*}_ref.v
prep
@@ -28,7 +38,7 @@ done
for aig in *.aig; do
echo "Checking $aig."
- ../../yosys-abc -q "read -c $aig; write ${aig%.*}_ref.v"
+ $abcprog -q "read -c $aig; write ${aig%.*}_ref.v"
../../yosys -qp "
read_verilog ${aig%.*}_ref.v
prep
diff --git a/tests/memories/run-test.sh b/tests/memories/run-test.sh
index d0537bb98..76acaa9cd 100755
--- a/tests/memories/run-test.sh
+++ b/tests/memories/run-test.sh
@@ -4,15 +4,17 @@ set -e
OPTIND=1
seed="" # default to no seed specified
-while getopts "S:" opt
+abcopt=""
+while getopts "A:S:" opt
do
case "$opt" in
+ A) abcopt="-A $OPTARG" ;;
S) seed="-S $OPTARG" ;;
esac
done
shift "$((OPTIND-1))"
-bash ../tools/autotest.sh $seed -G *.v
+bash ../tools/autotest.sh $abcopt $seed -G *.v
for f in `egrep -l 'expect-(wr-ports|rd-ports|rd-clk)' *.v`; do
echo -n "Testing expectations for $f .."
diff --git a/tests/opt/opt_ff_sat.v b/tests/opt/opt_ff_sat.v
new file mode 100644
index 000000000..5a0a6fe37
--- /dev/null
+++ b/tests/opt/opt_ff_sat.v
@@ -0,0 +1,12 @@
+module top (
+ input clk,
+ output reg [7:0] cnt
+);
+ initial cnt = 0;
+ always @(posedge clk) begin
+ if (cnt < 20)
+ cnt <= cnt + 1;
+ else
+ cnt <= 0;
+ end
+endmodule
diff --git a/tests/opt/opt_ff_sat.ys b/tests/opt/opt_ff_sat.ys
new file mode 100644
index 000000000..4e7cc6ca4
--- /dev/null
+++ b/tests/opt/opt_ff_sat.ys
@@ -0,0 +1,5 @@
+read_verilog opt_ff_sat.v
+prep -flatten
+opt_rmdff -sat
+synth
+select -assert-count 5 t:$_DFF_P_
diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index 96d9cdda9..7b64b357f 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -23,12 +23,13 @@ warn_iverilog_git=false
# The tests are skipped if firrtl2verilog is the empty string (the default).
firrtl2verilog=""
xfirrtl="../xfirrtl"
+abcprog="$toolsdir/../../yosys-abc"
if [ ! -f $toolsdir/cmp_tbdata -o $toolsdir/cmp_tbdata.c -nt $toolsdir/cmp_tbdata ]; then
( set -ex; ${CC:-gcc} -Wall -o $toolsdir/cmp_tbdata $toolsdir/cmp_tbdata.c; ) || exit 1
fi
-while getopts xmGl:wkjvref:s:p:n:S:I:-: opt; do
+while getopts xmGl:wkjvref:s:p:n:S:I:A:-: opt; do
case "$opt" in
x)
use_xsim=true ;;
@@ -65,6 +66,8 @@ while getopts xmGl:wkjvref:s:p:n:S:I:-: opt; do
include_opts="$include_opts -I $OPTARG"
xinclude_opts="$xinclude_opts -i $OPTARG"
minclude_opts="$minclude_opts +incdir+$OPTARG" ;;
+ A)
+ abcprog="$OPTARG" ;;
-)
case "${OPTARG}" in
xfirrtl)
@@ -147,7 +150,7 @@ do
if [[ "$ext" == "v" ]]; then
egrep -v '^\s*`timescale' ../$fn > ${bn}_ref.${ext}
elif [[ "$ext" == "aig" ]] || [[ "$ext" == "aag" ]]; then
- "$toolsdir"/../../yosys-abc -c "read_aiger ../${fn}; write ${bn}_ref.${refext}"
+ $abcprog -c "read_aiger ../${fn}; write ${bn}_ref.${refext}"
else
refext=$ext
cp ../${fn} ${bn}_ref.${refext}
generated by cgit v1.2.3 (git 2.25.1) at 2025-02-21 18:17:07 +0000