From f81bf9bdea7f99602bc2c7f0d43f1058a716508e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 12 Aug 2015 12:56:20 +0200 Subject: [PATCH 1/6] Added SMV back-end 'test_cells.sh' script --- backends/smv/test_cells.sh | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 backends/smv/test_cells.sh diff --git a/backends/smv/test_cells.sh b/backends/smv/test_cells.sh new file mode 100644 index 000000000..63de465c0 --- /dev/null +++ b/backends/smv/test_cells.sh @@ -0,0 +1,33 @@ +#!/bin/bash + +set -ex + +rm -rf test_cells.tmp +mkdir -p test_cells.tmp +cd test_cells.tmp + +# don't test $mul to reduce runtime +# don't test $div and $mod to reduce runtime and avoid "div by zero" message +../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$macc /$mul /$div /$mod' + +cat > template.txt << "EOT" +%module main + INVARSPEC ! bool(_trigger); +EOT + +for fn in test_*.il; do + ../../../yosys -p " + read_ilang $fn + rename gold gate + synth + + read_ilang $fn + miter -equiv -flatten gold gate main + hierarchy -top main + write_smv -tpl template.txt ${fn#.il}.smv + " + nuXmv -dynamic ${fn#.il}.smv > ${fn#.il}.out +done + +grep '^-- invariant .* is false' *.out || echo 'All OK.' + From bc468cb6f2846919d84e7586c5551c94d3234f6d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 12 Aug 2015 13:37:09 +0200 Subject: [PATCH 2/6] Fixed hashlib for 64 bit int keys --- kernel/hashlib.h | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/kernel/hashlib.h b/kernel/hashlib.h index 2f8479502..f94945eca 100644 --- a/kernel/hashlib.h +++ b/kernel/hashlib.h @@ -58,17 +58,23 @@ template struct hash_ops { } }; -template<> struct hash_ops { +struct hash_int_ops { template static inline bool cmp(T a, T b) { return a == b; } - template - static inline unsigned int hash(T a) { + static inline unsigned int hash(int32_t a) { return a; } + static inline unsigned int hash(int64_t a) { + return mkhash(a, a >> 32); + } }; +template<> struct hash_ops : hash_int_ops {}; +template<> struct hash_ops : hash_int_ops {}; +template<> struct hash_ops : hash_int_ops {}; + template<> struct hash_ops { static inline bool cmp(const std::string &a, const std::string &b) { return a == b; From c43f38c81be830469eb1536c073c519b25e18f4e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 12 Aug 2015 14:10:14 +0200 Subject: [PATCH 3/6] Improved handling of "keep" attributes in hierarchical designs in opt_clean --- passes/opt/opt_clean.cc | 82 ++++++++++++++++++++++++++------------ techlibs/ice40/cells_sim.v | 3 +- 2 files changed, 58 insertions(+), 27 deletions(-) diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index bb2f77069..e6de9d3c8 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -30,7 +30,55 @@ PRIVATE_NAMESPACE_BEGIN using RTLIL::id2cstr; -CellTypes ct, ct_reg, ct_all; +struct keep_cache_t +{ + Design *design; + dict cache; + + void reset(Design *design = nullptr) + { + this->design = design; + cache.clear(); + } + + bool query(Module *module) + { + log_assert(design != nullptr); + + if (module == nullptr) + return false; + + if (cache.count(module)) + return cache.at(module); + + cache[module] = true; + if (!module->get_bool_attribute("\\keep")) { + bool found_keep = false; + for (auto cell : module->cells()) + if (query(cell)) found_keep = true; + cache[module] = found_keep; + } + + return cache[module]; + } + + bool query(Cell *cell) + { + if (cell->type.in("$memwr", "$meminit", "$assert", "$assume")) + return true; + + if (cell->has_keep_attr()) + return true; + + if (cell->module && cell->module->design) + return query(cell->module->design->module(cell->type)); + + return false; + } +}; + +keep_cache_t keep_cache; +CellTypes ct_reg, ct_all; int count_rm_cells, count_rm_wires; void rmunused_module_cells(Module *module, bool verbose) @@ -42,12 +90,12 @@ void rmunused_module_cells(Module *module, bool verbose) for (auto &it : module->cells_) { Cell *cell = it.second; for (auto &it2 : cell->connections()) { - if (!ct.cell_input(cell->type, it2.first)) + if (!ct_all.cell_input(cell->type, it2.first)) for (auto bit : sigmap(it2.second)) if (bit.wire != nullptr) wire2driver[bit].insert(cell); } - if (cell->type.in("$memwr", "$meminit", "$assert", "$assume") || cell->has_keep_attr()) + if (keep_cache.query(cell)) queue.insert(cell); else unused.insert(cell); @@ -67,7 +115,7 @@ void rmunused_module_cells(Module *module, bool verbose) pool bits; for (auto cell : queue) for (auto &it : cell->connections()) - if (!ct.cell_output(cell->type, it.first)) + if (!ct_all.cell_output(cell->type, it.first)) for (auto bit : sigmap(it.second)) bits.insert(bit); @@ -193,7 +241,7 @@ void rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos for (auto &it2 : cell->connections_) { assign_map.apply(it2.second); used_signals.add(it2.second); - if (!ct.cell_output(cell->type, it2.first)) + if (!ct_all.cell_output(cell->type, it2.first)) used_signals_nodrivers.add(it2.second); } } @@ -345,15 +393,7 @@ struct OptCleanPass : public Pass { } extra_args(args, argidx, design); - ct.setup_internals(); - ct.setup_internals_mem(); - ct.setup_stdcells(); - ct.setup_stdcells_mem(); - - for (auto module : design->modules()) { - if (module->get_bool_attribute("\\blackbox")) - ct.setup_module(module); - } + keep_cache.reset(design); ct_reg.setup_internals_mem(); ct_reg.setup_stdcells_mem(); @@ -370,7 +410,7 @@ struct OptCleanPass : public Pass { design->sort(); design->check(); - ct.clear(); + keep_cache.reset(); ct_reg.clear(); ct_all.clear(); log_pop(); @@ -409,15 +449,7 @@ struct CleanPass : public Pass { if (argidx < args.size()) extra_args(args, argidx, design); - ct.setup_internals(); - ct.setup_internals_mem(); - ct.setup_stdcells(); - ct.setup_stdcells_mem(); - - for (auto module : design->modules()) { - if (module->get_bool_attribute("\\blackbox")) - ct.setup_module(module); - } + keep_cache.reset(design); ct_reg.setup_internals_mem(); ct_reg.setup_stdcells_mem(); @@ -440,7 +472,7 @@ struct CleanPass : public Pass { design->sort(); design->check(); - ct.clear(); + keep_cache.reset(); ct_reg.clear(); ct_all.clear(); } diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v index ed7c7cd2d..17b6be9ce 100644 --- a/techlibs/ice40/cells_sim.v +++ b/techlibs/ice40/cells_sim.v @@ -866,8 +866,7 @@ endmodule // SiliconBlue Device Configuration Cells -(* blackbox *) -(* keep *) +(* blackbox, keep *) module SB_WARMBOOT ( input BOOT, input S1, From e4ef000b703080131f4608f8bdcbe108a9b30b51 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 12 Aug 2015 15:04:44 +0200 Subject: [PATCH 4/6] Adjust makefiles to work with out-of-tree builds This is based on work done by Larry Doolittle --- Makefile | 26 +++++++++++++++----------- frontends/ilang/Makefile.inc | 6 ++++-- frontends/ilang/ilang_lexer.l | 2 +- frontends/ilang/ilang_parser.y | 2 +- frontends/verilog/Makefile.inc | 6 ++++-- frontends/verilog/verilog_lexer.l | 2 +- frontends/verilog/verilog_parser.y | 2 +- passes/techmap/Makefile.inc | 2 ++ techlibs/common/Makefile.inc | 7 ------- techlibs/common/blackbox.sed | 5 ----- techlibs/ice40/Makefile.inc | 5 +---- techlibs/xilinx/Makefile.inc | 8 ++------ 12 files changed, 32 insertions(+), 41 deletions(-) delete mode 100644 techlibs/common/blackbox.sed diff --git a/Makefile b/Makefile index f5a61b131..3fb9c5703 100644 --- a/Makefile +++ b/Makefile @@ -36,8 +36,10 @@ SMALL = 0 all: top-all -YOSYS_SRC := $(shell pwd) -CXXFLAGS = -Wall -Wextra -ggdb -I"$(YOSYS_SRC)" -MD -D_YOSYS_ -fPIC -I$(DESTDIR)/include +YOSYS_SRC := $(dir $(firstword $(MAKEFILE_LIST))) +VPATH := $(YOSYS_SRC) + +CXXFLAGS = -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -D_YOSYS_ -fPIC -I$(DESTDIR)/include LDFLAGS = -L$(DESTDIR)/lib LDLIBS = -lstdc++ -lm SED = sed @@ -190,7 +192,7 @@ define add_share_file EXTRA_TARGETS += $(subst //,/,$(1)/$(notdir $(2))) $(subst //,/,$(1)/$(notdir $(2))): $(2) $$(P) mkdir -p $(1) - $$(Q) cp $(2) $(subst //,/,$(1)/$(notdir $(2))) + $$(Q) cp "$(YOSYS_SRC)"/$(2) $(subst //,/,$(1)/$(notdir $(2))) endef define add_include_file @@ -250,10 +252,10 @@ OBJS += libs/minisat/SimpSolver.o OBJS += libs/minisat/Solver.o OBJS += libs/minisat/System.o -include frontends/*/Makefile.inc -include passes/*/Makefile.inc -include backends/*/Makefile.inc -include techlibs/*/Makefile.inc +include $(YOSYS_SRC)/frontends/*/Makefile.inc +include $(YOSYS_SRC)/passes/*/Makefile.inc +include $(YOSYS_SRC)/backends/*/Makefile.inc +include $(YOSYS_SRC)/techlibs/*/Makefile.inc else @@ -297,20 +299,22 @@ libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) $(P) $(CXX) -o libyosys.so -shared -Wl,-soname,libyosys.so $(LDFLAGS) $^ $(LDLIBS) %.o: %.cc + $(Q) mkdir -p $(dir $@) $(P) $(CXX) -o $@ -c $(CXXFLAGS) $< %.o: %.cpp + $(Q) mkdir -p $(dir $@) $(P) $(CXX) -o $@ -c $(CXXFLAGS) $< -kernel/version_$(GIT_REV).cc: Makefile +kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile $(P) rm -f kernel/version_*.o kernel/version_*.d kernel/version_*.cc - $(Q) echo "namespace Yosys { extern const char *yosys_version_str; const char *yosys_version_str=\"Yosys $(YOSYS_VER) (git sha1 $(GIT_REV), $(notdir $(CXX)) ` \ + $(Q) mkdir -p kernel && echo "namespace Yosys { extern const char *yosys_version_str; const char *yosys_version_str=\"Yosys $(YOSYS_VER) (git sha1 $(GIT_REV), $(notdir $(CXX)) ` \ $(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1` $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS)))\"; }" > kernel/version_$(GIT_REV).cc yosys-config: misc/yosys-config.in - $(P) $(SED) -e 's,@CXXFLAGS@,$(subst -I"$(YOSYS_SRC)",-I"$(TARGET_DATDIR)/include",$(CXXFLAGS)),;' \ + $(P) $(SED) -e 's,@CXXFLAGS@,$(subst -I. -I"$(YOSYS_SRC)",-I"$(TARGET_DATDIR)/include",$(CXXFLAGS)),;' \ -e 's,@CXX@,$(CXX),;' -e 's,@LDFLAGS@,$(LDFLAGS),;' -e 's,@LDLIBS@,$(LDLIBS),;' \ - -e 's,@BINDIR@,$(TARGET_BINDIR),;' -e 's,@DATDIR@,$(TARGET_DATDIR),;' < misc/yosys-config.in > yosys-config + -e 's,@BINDIR@,$(TARGET_BINDIR),;' -e 's,@DATDIR@,$(TARGET_DATDIR),;' < $< > yosys-config $(Q) chmod +x yosys-config abc/abc-$(ABCREV)$(EXE): diff --git a/frontends/ilang/Makefile.inc b/frontends/ilang/Makefile.inc index c15e2cc47..e2a476c93 100644 --- a/frontends/ilang/Makefile.inc +++ b/frontends/ilang/Makefile.inc @@ -5,13 +5,15 @@ GENFILES += frontends/ilang/ilang_parser.output GENFILES += frontends/ilang/ilang_lexer.cc frontends/ilang/ilang_parser.tab.cc: frontends/ilang/ilang_parser.y - $(P) $(BISON) -d -r all -b frontends/ilang/ilang_parser frontends/ilang/ilang_parser.y + $(Q) mkdir -p $(dir $@) + $(P) $(BISON) -d -r all -b frontends/ilang/ilang_parser $< $(Q) mv frontends/ilang/ilang_parser.tab.c frontends/ilang/ilang_parser.tab.cc frontends/ilang/ilang_parser.tab.h: frontends/ilang/ilang_parser.tab.cc frontends/ilang/ilang_lexer.cc: frontends/ilang/ilang_lexer.l - $(P) flex -o frontends/ilang/ilang_lexer.cc frontends/ilang/ilang_lexer.l + $(Q) mkdir -p $(dir $@) + $(P) flex -o frontends/ilang/ilang_lexer.cc $< OBJS += frontends/ilang/ilang_parser.tab.o frontends/ilang/ilang_lexer.o OBJS += frontends/ilang/ilang_frontend.o diff --git a/frontends/ilang/ilang_lexer.l b/frontends/ilang/ilang_lexer.l index 57296403c..415de74eb 100644 --- a/frontends/ilang/ilang_lexer.l +++ b/frontends/ilang/ilang_lexer.l @@ -29,7 +29,7 @@ #pragma clang diagnostic ignored "-Wdeprecated-register" #endif -#include "ilang_frontend.h" +#include "frontends/ilang/ilang_frontend.h" #include "ilang_parser.tab.h" USING_YOSYS_NAMESPACE diff --git a/frontends/ilang/ilang_parser.y b/frontends/ilang/ilang_parser.y index 2139f91fa..6090fabe5 100644 --- a/frontends/ilang/ilang_parser.y +++ b/frontends/ilang/ilang_parser.y @@ -24,7 +24,7 @@ %{ #include -#include "ilang_frontend.h" +#include "frontends/ilang/ilang_frontend.h" YOSYS_NAMESPACE_BEGIN namespace ILANG_FRONTEND { std::istream *lexin; diff --git a/frontends/verilog/Makefile.inc b/frontends/verilog/Makefile.inc index 92cbd0b87..a06c1d5ab 100644 --- a/frontends/verilog/Makefile.inc +++ b/frontends/verilog/Makefile.inc @@ -5,13 +5,15 @@ GENFILES += frontends/verilog/verilog_parser.output GENFILES += frontends/verilog/verilog_lexer.cc frontends/verilog/verilog_parser.tab.cc: frontends/verilog/verilog_parser.y - $(P) $(BISON) -d -r all -b frontends/verilog/verilog_parser frontends/verilog/verilog_parser.y + $(Q) mkdir -p $(dir $@) + $(P) $(BISON) -d -r all -b frontends/verilog/verilog_parser $< $(Q) mv frontends/verilog/verilog_parser.tab.c frontends/verilog/verilog_parser.tab.cc frontends/verilog/verilog_parser.tab.h: frontends/verilog/verilog_parser.tab.cc frontends/verilog/verilog_lexer.cc: frontends/verilog/verilog_lexer.l - $(P) flex -o frontends/verilog/verilog_lexer.cc frontends/verilog/verilog_lexer.l + $(Q) mkdir -p $(dir $@) + $(P) flex -o frontends/verilog/verilog_lexer.cc $< OBJS += frontends/verilog/verilog_parser.tab.o OBJS += frontends/verilog/verilog_lexer.o diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l index 480391532..bd7837b3a 100644 --- a/frontends/verilog/verilog_lexer.l +++ b/frontends/verilog/verilog_lexer.l @@ -40,7 +40,7 @@ #endif #include "kernel/log.h" -#include "verilog_frontend.h" +#include "frontends/verilog/verilog_frontend.h" #include "frontends/ast/ast.h" #include "verilog_parser.tab.h" diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 0a6a6111e..708ac7627 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -36,7 +36,7 @@ %{ #include #include -#include "verilog_frontend.h" +#include "frontends/verilog/verilog_frontend.h" #include "kernel/log.h" USING_YOSYS_NAMESPACE diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc index e39d5c5c2..f1c987ccd 100644 --- a/passes/techmap/Makefile.inc +++ b/passes/techmap/Makefile.inc @@ -24,6 +24,7 @@ endif GENFILES += passes/techmap/techmap.inc passes/techmap/techmap.inc: techlibs/common/techmap.v + $(Q) mkdir -p $(dir $@) $(P) echo "// autogenerated from $<" > $@.new $(Q) echo "static char stdcells_code[] = {" >> $@.new $(Q) od -v -td1 -An $< | $(SED) -e 's/[0-9][0-9]*/&,/g' >> $@.new @@ -37,6 +38,7 @@ TARGETS += yosys-filterlib$(EXE) EXTRA_OBJS += passes/techmap/filterlib.o yosys-filterlib$(EXE): passes/techmap/filterlib.o + $(Q) mkdir -p $(dir $@) $(P) $(CXX) -o yosys-filterlib$(EXE) $(LDFLAGS) $^ $(LDLIBS) endif diff --git a/techlibs/common/Makefile.inc b/techlibs/common/Makefile.inc index d2ce61cf6..f222a0289 100644 --- a/techlibs/common/Makefile.inc +++ b/techlibs/common/Makefile.inc @@ -3,16 +3,9 @@ ifneq ($(SMALL),1) OBJS += techlibs/common/synth.o endif -EXTRA_TARGETS += techlibs/common/blackbox.v - -techlibs/common/blackbox.v: techlibs/common/blackbox.sed techlibs/common/simlib.v techlibs/common/simcells.v - $(P) cat techlibs/common/simlib.v techlibs/common/simcells.v | $(SED) -rf techlibs/common/blackbox.sed > techlibs/common/blackbox.v.new - $(Q) mv techlibs/common/blackbox.v.new techlibs/common/blackbox.v - $(eval $(call add_share_file,share,techlibs/common/simlib.v)) $(eval $(call add_share_file,share,techlibs/common/simcells.v)) $(eval $(call add_share_file,share,techlibs/common/techmap.v)) -$(eval $(call add_share_file,share,techlibs/common/blackbox.v)) $(eval $(call add_share_file,share,techlibs/common/pmux2mux.v)) $(eval $(call add_share_file,share,techlibs/common/adff2dff.v)) $(eval $(call add_share_file,share,techlibs/common/cells.lib)) diff --git a/techlibs/common/blackbox.sed b/techlibs/common/blackbox.sed deleted file mode 100644 index db8900344..000000000 --- a/techlibs/common/blackbox.sed +++ /dev/null @@ -1,5 +0,0 @@ -#!/bin/sed -r -/^(wire|assign|reg|event|integer|localparam|\/\/|[\/ ]\*| *$|`)/ d; -/^(genvar|generate|always|initial|task|function)/,/^end/ d; -/^endmodule/ s/$/\n/; -s/ reg / /; diff --git a/techlibs/ice40/Makefile.inc b/techlibs/ice40/Makefile.inc index a9d2f2369..6907f0a0e 100644 --- a/techlibs/ice40/Makefile.inc +++ b/techlibs/ice40/Makefile.inc @@ -11,7 +11,7 @@ EXTRA_OBJS += techlibs/ice40/brams_init.mk .SECONDARY: techlibs/ice40/brams_init.mk techlibs/ice40/brams_init.mk: techlibs/ice40/brams_init.py - $(P) cd techlibs/ice40 && python brams_init.py + $(P) cd share/ice40 && python $< $(Q) touch techlibs/ice40/brams_init.mk techlibs/ice40/brams_init1.vh: techlibs/ice40/brams_init.mk @@ -23,7 +23,4 @@ $(eval $(call add_share_file,share/ice40,techlibs/ice40/cells_map.v)) $(eval $(call add_share_file,share/ice40,techlibs/ice40/cells_sim.v)) $(eval $(call add_share_file,share/ice40,techlibs/ice40/brams.txt)) $(eval $(call add_share_file,share/ice40,techlibs/ice40/brams_map.v)) -$(eval $(call add_share_file,share/ice40,techlibs/ice40/brams_init1.vh)) -$(eval $(call add_share_file,share/ice40,techlibs/ice40/brams_init2.vh)) -$(eval $(call add_share_file,share/ice40,techlibs/ice40/brams_init3.vh)) diff --git a/techlibs/xilinx/Makefile.inc b/techlibs/xilinx/Makefile.inc index a8f5416e3..c6cf1a7d3 100644 --- a/techlibs/xilinx/Makefile.inc +++ b/techlibs/xilinx/Makefile.inc @@ -10,8 +10,8 @@ EXTRA_OBJS += techlibs/xilinx/brams_init.mk .SECONDARY: techlibs/xilinx/brams_init.mk techlibs/xilinx/brams_init.mk: techlibs/xilinx/brams_init.py - $(P) cd techlibs/xilinx && python brams_init.py - $(Q) touch techlibs/xilinx/brams_init.mk + $(P) cd share/xilinx && python $< + $(Q) touch $@ techlibs/xilinx/brams_init_36.vh: techlibs/xilinx/brams_init.mk techlibs/xilinx/brams_init_32.vh: techlibs/xilinx/brams_init.mk @@ -22,10 +22,6 @@ $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/cells_map.v)) $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/cells_sim.v)) $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/brams.txt)) $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/brams_map.v)) -$(eval $(call add_share_file,share/xilinx,techlibs/xilinx/brams_init_36.vh)) -$(eval $(call add_share_file,share/xilinx,techlibs/xilinx/brams_init_32.vh)) -$(eval $(call add_share_file,share/xilinx,techlibs/xilinx/brams_init_18.vh)) -$(eval $(call add_share_file,share/xilinx,techlibs/xilinx/brams_init_16.vh)) $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/brams_bb.v)) $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/drams.txt)) $(eval $(call add_share_file,share/xilinx,techlibs/xilinx/drams_map.v)) From fc20b1c3d210ff1821d6c56fb0b8c9c6ba625aa5 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 12 Aug 2015 16:54:30 +0200 Subject: [PATCH 5/6] Fixed "make clean" for out-of-tree builds --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 3fb9c5703..6585ca39f 100644 --- a/Makefile +++ b/Makefile @@ -397,7 +397,7 @@ manual: $(TARGETS) $(EXTRA_TARGETS) clean: rm -rf share - cd manual && bash clean.sh + if test -d manual; then cd manual && sh clean.sh; fi rm -f $(OBJS) $(GENFILES) $(TARGETS) $(EXTRA_TARGETS) $(EXTRA_OBJS) rm -f kernel/version_*.o kernel/version_*.cc abc/abc-[0-9a-f]* rm -f libs/*/*.d frontends/*/*.d passes/*/*.d backends/*/*.d kernel/*.d techlibs/*/*.d From 698357dd9a17365566f4db2662e9ce9fea7594c4 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 12 Aug 2015 17:13:54 +0200 Subject: [PATCH 6/6] Added "write_smt2 -regs" --- backends/smt2/smt2.cc | 43 ++++++++++++++++++++++++++++++++++++------- 1 file changed, 36 insertions(+), 7 deletions(-) diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index d828d6588..9b1972b14 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -32,7 +32,7 @@ struct Smt2Worker CellTypes ct; SigMap sigmap; RTLIL::Module *module; - bool bvmode, memmode, verbose; + bool bvmode, memmode, regsmode, verbose; int idcounter; std::vector decls, trans; @@ -44,8 +44,8 @@ struct Smt2Worker std::map memarrays; std::map bvsizes; - Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool verbose) : - ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), verbose(verbose), idcounter(0) + Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool regsmode, bool verbose) : + ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), regsmode(regsmode), verbose(verbose), idcounter(0) { decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module))); @@ -470,9 +470,30 @@ struct Smt2Worker { if (verbose) log("=> export logic driving outputs\n"); - for (auto wire : module->wires()) - if (wire->port_id || wire->get_bool_attribute("\\keep")) { + pool reg_bits; + if (regsmode) { + for (auto cell : module->cells()) + if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) { + // not using sigmap -- we want the net directly at the dff output + for (auto bit : cell->getPort("\\Q")) + reg_bits.insert(bit); + } + } + + for (auto wire : module->wires()) { + bool is_register = false; + if (regsmode) + for (auto bit : SigSpec(wire)) + if (reg_bits.count(bit)) + is_register = true; + if (wire->port_id || is_register || wire->get_bool_attribute("\\keep")) { RTLIL::SigSpec sig = sigmap(wire); + if (wire->port_input) + decls.push_back(stringf("; yosys-smt2-input %s %d\n", log_id(wire), wire->width)); + if (wire->port_output) + decls.push_back(stringf("; yosys-smt2-output %s %d\n", log_id(wire), wire->width)); + if (is_register) + decls.push_back(stringf("; yosys-smt2-register %s %d\n", log_id(wire), wire->width)); if (bvmode && GetSize(sig) > 1) { decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", log_id(module), log_id(wire), log_id(module), GetSize(sig), get_bv(sig).c_str())); @@ -486,6 +507,7 @@ struct Smt2Worker log_id(module), log_id(wire), log_id(module), get_bool(sig[i]).c_str())); } } + } if (verbose) log("=> export logic associated with the initial state\n"); @@ -666,6 +688,9 @@ struct Smt2Backend : public Backend { log(" will be generated for accessing the arrays that are used to represent\n"); log(" memories.\n"); log("\n"); + log(" -regs\n"); + log(" also create '_n' functions for all registers.\n"); + log("\n"); log(" -tpl \n"); log(" use the given template file. the line containing only the token '%%%%'\n"); log(" is replaced with the regular output of this command.\n"); @@ -722,7 +747,7 @@ struct Smt2Backend : public Backend { virtual void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) { std::ifstream template_f; - bool bvmode = false, memmode = false, verbose = false; + bool bvmode = false, memmode = false, regsmode = false, verbose = false; log_header("Executing SMT2 backend.\n"); @@ -744,6 +769,10 @@ struct Smt2Backend : public Backend { memmode = true; continue; } + if (args[argidx] == "-regs") { + regsmode = true; + continue; + } if (args[argidx] == "-verbose") { verbose = true; continue; @@ -773,7 +802,7 @@ struct Smt2Backend : public Backend { log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); - Smt2Worker worker(module, bvmode, memmode, verbose); + Smt2Worker worker(module, bvmode, memmode, regsmode, verbose); worker.run(); worker.write(*f); }