diff --git a/CHANGELOG b/CHANGELOG index 638ce558bfb..6dcd05de665 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -39,7 +39,7 @@ Yosys 0.9 .. Yosys 0.9-dev - Improvements in pmgen: slices, choices, define, generate - 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 "_TECHMAP_WIREINIT_*_" parameter and "_TECHMAP_REMOVEINIT_*_" wire for "techmap" pass - Added "-match-init" option to "dff2dffs" pass - Added "techmap_autopurge" support to techmap - Added "add -mod " @@ -62,11 +62,14 @@ Yosys 0.9 .. Yosys 0.9-dev - Improved support of $readmem[hb] Memory Content File inclusion - Added "opt_lut_ins" pass - Added "logger" pass - - Removed "dffsr2dff" (use opt_rmdff instead) - Added "design -delete" - Added "select -unset" - Use YosysHQ/abc instead of upstream berkeley-abc/abc - Added $divfloor and $modfloor cells + - Added $adffe, $dffsre, $sdff, $sdffe, $sdffce, $adlatch cells + - Added "dfflegalize" pass + - Added "_TECHMAP_CELLNAME_" parameter for "techmap" pass + - Merged "dffsr2dff", "opt_rmdff", "dff2dffe", "dff2dffs", "peepopt.dffmux" passes into a new "opt_dff" pass Yosys 0.8 .. Yosys 0.9 ---------------------- diff --git a/CODEOWNERS b/CODEOWNERS index a73779920c1..350a62120b5 100644 --- a/CODEOWNERS +++ b/CODEOWNERS @@ -33,5 +33,6 @@ misc/*.py @btut backends/firrtl @ucbjrl @azidar passes/sat/qbfsat.cc @boqwxp +passes/sat/qbfsat.h @boqwxp passes/cmds/exec.cc @boqwxp passes/cmds/printattrs.cc @boqwxp diff --git a/Makefile b/Makefile index 3d3e60359b1..97a6370d9ec 100644 --- a/Makefile +++ b/Makefile @@ -30,6 +30,7 @@ ENABLE_GCOV := 0 ENABLE_GPROF := 0 ENABLE_DEBUG := 0 ENABLE_NDEBUG := 0 +ENABLE_CCACHE := 0 LINK_CURSES := 0 LINK_TERMCAP := 0 LINK_ABC := 0 @@ -81,7 +82,7 @@ all: top-all YOSYS_SRC := $(dir $(firstword $(MAKEFILE_LIST))) VPATH := $(YOSYS_SRC) -CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -D_YOSYS_ -fPIC -I$(PREFIX)/include +CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -MP -D_YOSYS_ -fPIC -I$(PREFIX)/include LDLIBS := $(LDLIBS) -lstdc++ -lm PLUGIN_LDFLAGS := @@ -122,7 +123,7 @@ LDFLAGS += -rdynamic LDLIBS += -lrt endif -YOSYS_VER := 0.9+2406 +YOSYS_VER := 0.9+3683 GIT_REV := $(shell cd $(YOSYS_SRC) && git rev-parse --short HEAD 2> /dev/null || echo UNKNOWN) OBJS = kernel/version_$(GIT_REV).o @@ -170,8 +171,7 @@ else PYTHON_CONFIG := $(PYTHON_EXECUTABLE)-config endif -PYTHON_PREFIX := $(shell $(PYTHON_CONFIG) --prefix) -PYTHON_DESTDIR := $(PYTHON_PREFIX)/lib/python$(PYTHON_VERSION)/site-packages +PYTHON_DESTDIR := $(shell $(PYTHON_EXECUTABLE) -c "import site; print(site.getsitepackages()[-1]);") # Reload Makefile.conf to override python specific variables if defined ifneq ($(wildcard Makefile.conf),) @@ -246,7 +246,7 @@ CXXFLAGS := -std=c++11 $(filter-out -fPIC -ggdb,$(CXXFLAGS)) ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DABC_MEMALIGN=8" EMCCFLAGS := -Os -Wno-warn-absolute-paths EMCCFLAGS += --memory-init-file 0 --embed-file share -s NO_EXIT_RUNTIME=1 -EMCCFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg']" +EMCCFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg','_memset']" EMCCFLAGS += -s TOTAL_MEMORY=134217728 EMCCFLAGS += -s EXTRA_EXPORTED_RUNTIME_METHODS='["ccall", "cwrap"]' # https://github.com/kripken/emscripten/blob/master/src/settings.js @@ -528,6 +528,10 @@ ifeq ($(ENABLE_COVER),1) CXXFLAGS += -DYOSYS_ENABLE_COVER endif +ifeq ($(ENABLE_CCACHE),1) +CXX := ccache $(CXX) +endif + define add_share_file EXTRA_TARGETS += $(subst //,/,$(1)/$(notdir $(2))) $(subst //,/,$(1)/$(notdir $(2))): $(2) @@ -580,13 +584,16 @@ $(eval $(call add_include_file,kernel/modtools.h)) $(eval $(call add_include_file,kernel/macc.h)) $(eval $(call add_include_file,kernel/utils.h)) $(eval $(call add_include_file,kernel/satgen.h)) +$(eval $(call add_include_file,kernel/ff.h)) +$(eval $(call add_include_file,kernel/ffinit.h)) +$(eval $(call add_include_file,kernel/mem.h)) $(eval $(call add_include_file,libs/ezsat/ezsat.h)) $(eval $(call add_include_file,libs/ezsat/ezminisat.h)) $(eval $(call add_include_file,libs/sha1/sha1.h)) $(eval $(call add_include_file,libs/json11/json11.hpp)) $(eval $(call add_include_file,passes/fsm/fsmdata.h)) $(eval $(call add_include_file,frontends/ast/ast.h)) -$(eval $(call add_include_file,backends/ilang/ilang_backend.h)) +$(eval $(call add_include_file,backends/rtlil/rtlil_backend.h)) $(eval $(call add_include_file,backends/cxxrtl/cxxrtl.h)) $(eval $(call add_include_file,backends/cxxrtl/cxxrtl_vcd.h)) $(eval $(call add_include_file,backends/cxxrtl/cxxrtl_capi.cc)) @@ -595,7 +602,7 @@ $(eval $(call add_include_file,backends/cxxrtl/cxxrtl_vcd_capi.cc)) $(eval $(call add_include_file,backends/cxxrtl/cxxrtl_vcd_capi.h)) OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/yosys.o -OBJS += kernel/cellaigs.o kernel/celledges.o +OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/mem.o kernel/log.o: CXXFLAGS += -DYOSYS_SRC='"$(YOSYS_SRC)"' kernel/yosys.o: CXXFLAGS += -DYOSYS_DATDIR='"$(DATDIR)"' -DYOSYS_PROGRAM_PREFIX='"$(PROGRAM_PREFIX)"' @@ -627,7 +634,7 @@ include $(YOSYS_SRC)/techlibs/*/Makefile.inc else include $(YOSYS_SRC)/frontends/verilog/Makefile.inc -include $(YOSYS_SRC)/frontends/ilang/Makefile.inc +include $(YOSYS_SRC)/frontends/rtlil/Makefile.inc include $(YOSYS_SRC)/frontends/ast/Makefile.inc include $(YOSYS_SRC)/frontends/blif/Makefile.inc @@ -644,7 +651,7 @@ include $(YOSYS_SRC)/passes/opt/Makefile.inc include $(YOSYS_SRC)/passes/techmap/Makefile.inc include $(YOSYS_SRC)/backends/verilog/Makefile.inc -include $(YOSYS_SRC)/backends/ilang/Makefile.inc +include $(YOSYS_SRC)/backends/rtlil/Makefile.inc include $(YOSYS_SRC)/techlibs/common/Makefile.inc @@ -654,6 +661,10 @@ ifeq ($(LINK_ABC),1) OBJS += $(PROGRAM_PREFIX)yosys-libabc.a endif +# prevent the CXXFLAGS set by this Makefile from reaching abc/Makefile, +# especially the -MD flag which will break the build when CXX is clang +unexport CXXFLAGS + top-all: $(TARGETS) $(EXTRA_TARGETS) @echo "" @echo " Build successful." @@ -679,7 +690,7 @@ endif %.pyh: %.h $(Q) mkdir -p $(dir $@) - $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(LD) -x c++ -o $@ -E -P - + $(P) cat $< | grep -E -v "#[ ]*(include|error)" | $(LD) $(CXXFLAGS) -x c++ -o $@ -E -P - ifeq ($(ENABLE_PYOSYS),1) $(PY_WRAPPER_FILE).cc: misc/$(PY_GEN_SCRIPT).py $(PY_WRAP_INCLUDES) @@ -783,6 +794,7 @@ test: $(TARGETS) $(EXTRA_TARGETS) +cd tests/arch/anlogic && bash run-test.sh $(SEEDOPT) +cd tests/arch/gowin && bash run-test.sh $(SEEDOPT) +cd tests/arch/intel_alm && bash run-test.sh $(SEEDOPT) + +cd tests/arch/nexus && bash run-test.sh $(SEEDOPT) +cd tests/rpc && bash run-test.sh +cd tests/memfile && bash run-test.sh +cd tests/verilog && bash run-test.sh @@ -839,9 +851,9 @@ ifeq ($(ENABLE_LIBYOSYS),1) $(INSTALL_SUDO) cp libyosys.so $(DESTDIR)$(LIBDIR)/ $(INSTALL_SUDO) $(STRIP) -S $(DESTDIR)$(LIBDIR)/libyosys.so ifeq ($(ENABLE_PYOSYS),1) - $(INSTALL_SUDO) mkdir -p $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys - $(INSTALL_SUDO) cp libyosys.so $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so - $(INSTALL_SUDO) cp misc/__init__.py $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/ + $(INSTALL_SUDO) mkdir -p $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys + $(INSTALL_SUDO) cp libyosys.so $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so + $(INSTALL_SUDO) cp misc/__init__.py $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/ endif endif @@ -851,9 +863,9 @@ uninstall: ifeq ($(ENABLE_LIBYOSYS),1) $(INSTALL_SUDO) rm -vf $(DESTDIR)$(LIBDIR)/libyosys.so ifeq ($(ENABLE_PYOSYS),1) - $(INSTALL_SUDO) rm -vf $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so - $(INSTALL_SUDO) rm -vf $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/__init__.py - $(INSTALL_SUDO) rmdir $(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys + $(INSTALL_SUDO) rm -vf $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/libyosys.so + $(INSTALL_SUDO) rm -vf $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys/__init__.py + $(INSTALL_SUDO) rmdir $(DESTDIR)$(PYTHON_DESTDIR)/$(subst -,_,$(PROGRAM_PREFIX))pyosys endif endif diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 81a3f483bba..476b30488d2 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -111,7 +111,7 @@ struct AigerWriter // promote public wires for (auto wire : module->wires()) - if (wire->name[0] == '\\') + if (wire->name.isPublic()) sigmap.add(wire); // promote input wires diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index ef0103c179b..27499b64a7a 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -146,7 +146,7 @@ struct XAigerWriter // promote public wires for (auto wire : module->wires()) - if (wire->name[0] == '\\') + if (wire->name.isPublic()) sigmap.add(wire); // promote input wires diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc index 780a163202d..08881904256 100644 --- a/backends/blif/blif.cc +++ b/backends/blif/blif.cc @@ -86,20 +86,18 @@ struct BlifDumper } } - vector cstr_buf; pool cstr_bits_seen; - const char *cstr(RTLIL::IdString id) + const std::string str(RTLIL::IdString id) { std::string str = RTLIL::unescape_id(id); for (size_t i = 0; i < str.size(); i++) if (str[i] == '#' || str[i] == '=' || str[i] == '<' || str[i] == '>') str[i] = '?'; - cstr_buf.push_back(str); - return cstr_buf.back().c_str(); + return str; } - const char *cstr(RTLIL::SigBit sig) + const std::string str(RTLIL::SigBit sig) { cstr_bits_seen.insert(sig); @@ -117,11 +115,10 @@ struct BlifDumper if (sig.wire->width != 1) str += stringf("[%d]", sig.wire->upto ? sig.wire->start_offset+sig.wire->width-sig.offset-1 : sig.wire->start_offset+sig.offset); - cstr_buf.push_back(str); - return cstr_buf.back().c_str(); + return str; } - const char *cstr_init(RTLIL::SigBit sig) + const std::string str_init(RTLIL::SigBit sig) { sigmap.apply(sig); @@ -130,8 +127,7 @@ struct BlifDumper string str = stringf(" %d", init_bits.at(sig)); - cstr_buf.push_back(str); - return cstr_buf.back().c_str(); + return str; } const char *subckt_or_gate(std::string cell_type) @@ -168,7 +164,7 @@ struct BlifDumper void dump() { f << stringf("\n"); - f << stringf(".model %s\n", cstr(module->name)); + f << stringf(".model %s\n", str(module->name).c_str()); std::map inputs, outputs; @@ -183,7 +179,7 @@ struct BlifDumper for (auto &it : inputs) { RTLIL::Wire *wire = it.second; for (int i = 0; i < wire->width; i++) - f << stringf(" %s", cstr(RTLIL::SigSpec(wire, i))); + f << stringf(" %s", str(RTLIL::SigSpec(wire, i)).c_str()); } f << stringf("\n"); @@ -191,7 +187,7 @@ struct BlifDumper for (auto &it : outputs) { RTLIL::Wire *wire = it.second; for (int i = 0; i < wire->width; i++) - f << stringf(" %s", cstr(RTLIL::SigSpec(wire, i))); + f << stringf(" %s", str(RTLIL::SigSpec(wire, i)).c_str()); } f << stringf("\n"); @@ -233,131 +229,131 @@ struct BlifDumper if (config->unbuf_types.count(cell->type)) { auto portnames = config->unbuf_types.at(cell->type); f << stringf(".names %s %s\n1 1\n", - cstr(cell->getPort(portnames.first)), cstr(cell->getPort(portnames.second))); + str(cell->getPort(portnames.first)).c_str(), str(cell->getPort(portnames.second)).c_str()); continue; } if (!config->icells_mode && cell->type == ID($_NOT_)) { f << stringf(".names %s %s\n0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_AND_)) { f << stringf(".names %s %s %s\n11 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_OR_)) { f << stringf(".names %s %s %s\n1- 1\n-1 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_XOR_)) { f << stringf(".names %s %s %s\n10 1\n01 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_NAND_)) { f << stringf(".names %s %s %s\n0- 1\n-0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_NOR_)) { f << stringf(".names %s %s %s\n00 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_XNOR_)) { f << stringf(".names %s %s %s\n11 1\n00 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_ANDNOT_)) { f << stringf(".names %s %s %s\n10 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_ORNOT_)) { f << stringf(".names %s %s %s\n1- 1\n-0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_AOI3_)) { f << stringf(".names %s %s %s %s\n-00 1\n0-0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::C)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_OAI3_)) { f << stringf(".names %s %s %s %s\n00- 1\n--0 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), str(cell->getPort(ID::C)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_AOI4_)) { f << stringf(".names %s %s %s %s %s\n-0-0 1\n-00- 1\n0--0 1\n0-0- 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), - cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), + str(cell->getPort(ID::C)).c_str(), str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_OAI4_)) { f << stringf(".names %s %s %s %s %s\n00-- 1\n--00 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), - cstr(cell->getPort(ID::C)), cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), + str(cell->getPort(ID::C)).c_str(), str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_MUX_)) { f << stringf(".names %s %s %s %s\n1-0 1\n-11 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), - cstr(cell->getPort(ID::S)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), + str(cell->getPort(ID::S)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_NMUX_)) { f << stringf(".names %s %s %s %s\n0-0 1\n-01 1\n", - cstr(cell->getPort(ID::A)), cstr(cell->getPort(ID::B)), - cstr(cell->getPort(ID::S)), cstr(cell->getPort(ID::Y))); + str(cell->getPort(ID::A)).c_str(), str(cell->getPort(ID::B)).c_str(), + str(cell->getPort(ID::S)).c_str(), str(cell->getPort(ID::Y)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_FF_)) { - f << stringf(".latch %s %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_DFF_N_)) { - f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr(cell->getPort(ID::C)), cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s fe %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str(cell->getPort(ID::C)).c_str(), str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_DFF_P_)) { - f << stringf(".latch %s %s re %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr(cell->getPort(ID::C)), cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s re %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str(cell->getPort(ID::C)).c_str(), str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_DLATCH_N_)) { - f << stringf(".latch %s %s al %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr(cell->getPort(ID::E)), cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s al %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str(cell->getPort(ID::E)).c_str(), str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } if (!config->icells_mode && cell->type == ID($_DLATCH_P_)) { - f << stringf(".latch %s %s ah %s%s\n", cstr(cell->getPort(ID::D)), cstr(cell->getPort(ID::Q)), - cstr(cell->getPort(ID::E)), cstr_init(cell->getPort(ID::Q))); + f << stringf(".latch %s %s ah %s%s\n", str(cell->getPort(ID::D)).c_str(), str(cell->getPort(ID::Q)).c_str(), + str(cell->getPort(ID::E)).c_str(), str_init(cell->getPort(ID::Q)).c_str()); goto internal_cell; } @@ -367,10 +363,10 @@ struct BlifDumper auto width = cell->parameters.at(ID::WIDTH).as_int(); log_assert(inputs.size() == width); for (int i = width-1; i >= 0; i--) - f << stringf(" %s", cstr(inputs.extract(i, 1))); + f << stringf(" %s", str(inputs.extract(i, 1)).c_str()); auto &output = cell->getPort(ID::Y); log_assert(output.size() == 1); - f << stringf(" %s", cstr(output)); + f << stringf(" %s", str(output).c_str()); f << stringf("\n"); RTLIL::SigSpec mask = cell->parameters.at(ID::LUT); for (int i = 0; i < (1 << width); i++) @@ -393,10 +389,10 @@ struct BlifDumper table.push_back(State::S0); log_assert(inputs.size() == width); for (int i = 0; i < width; i++) - f << stringf(" %s", cstr(inputs.extract(i, 1))); + f << stringf(" %s", str(inputs.extract(i, 1)).c_str()); auto &output = cell->getPort(ID::Y); log_assert(output.size() == 1); - f << stringf(" %s", cstr(output)); + f << stringf(" %s", str(output).c_str()); f << stringf("\n"); for (int i = 0; i < depth; i++) { for (int j = 0; j < width; j++) { @@ -411,11 +407,11 @@ struct BlifDumper goto internal_cell; } - f << stringf(".%s %s", subckt_or_gate(cell->type.str()), cstr(cell->type)); + f << stringf(".%s %s", subckt_or_gate(cell->type.str()), str(cell->type).c_str()); for (auto &conn : cell->connections()) { if (conn.second.size() == 1) { - f << stringf(" %s=%s", cstr(conn.first), cstr(conn.second[0])); + f << stringf(" %s=%s", str(conn.first).c_str(), str(conn.second[0]).c_str()); continue; } @@ -424,20 +420,20 @@ struct BlifDumper if (w == nullptr) { for (int i = 0; i < GetSize(conn.second); i++) - f << stringf(" %s[%d]=%s", cstr(conn.first), i, cstr(conn.second[i])); + f << stringf(" %s[%d]=%s", str(conn.first).c_str(), i, str(conn.second[i]).c_str()); } else { for (int i = 0; i < std::min(GetSize(conn.second), GetSize(w)); i++) { SigBit sig(w, i); - f << stringf(" %s[%d]=%s", cstr(conn.first), sig.wire->upto ? + f << stringf(" %s[%d]=%s", str(conn.first).c_str(), sig.wire->upto ? sig.wire->start_offset+sig.wire->width-sig.offset-1 : - sig.wire->start_offset+sig.offset, cstr(conn.second[i])); + sig.wire->start_offset+sig.offset, str(conn.second[i]).c_str()); } } } f << stringf("\n"); if (config->cname_mode) - f << stringf(".cname %s\n", cstr(cell->name)); + f << stringf(".cname %s\n", str(cell->name).c_str()); if (config->attr_mode) dump_params(".attr", cell->attributes); if (config->param_mode) @@ -446,7 +442,7 @@ struct BlifDumper if (0) { internal_cell: if (config->iname_mode) - f << stringf(".cname %s\n", cstr(cell->name)); + f << stringf(".cname %s\n", str(cell->name).c_str()); if (config->iattr_mode) dump_params(".attr", cell->attributes); } @@ -462,12 +458,12 @@ struct BlifDumper continue; if (config->conn_mode) - f << stringf(".conn %s %s\n", cstr(rhs_bit), cstr(lhs_bit)); + f << stringf(".conn %s %s\n", str(rhs_bit).c_str(), str(lhs_bit).c_str()); else if (!config->buf_type.empty()) f << stringf(".%s %s %s=%s %s=%s\n", subckt_or_gate(config->buf_type), config->buf_type.c_str(), - config->buf_in.c_str(), cstr(rhs_bit), config->buf_out.c_str(), cstr(lhs_bit)); + config->buf_in.c_str(), str(rhs_bit).c_str(), config->buf_out.c_str(), str(lhs_bit).c_str()); else - f << stringf(".names %s %s\n1 1\n", cstr(rhs_bit), cstr(lhs_bit)); + f << stringf(".names %s %s\n1 1\n", str(rhs_bit).c_str(), str(lhs_bit).c_str()); } f << stringf(".end\n"); diff --git a/backends/btor/.gitignore b/backends/btor/.gitignore new file mode 100644 index 00000000000..d23d492d733 --- /dev/null +++ b/backends/btor/.gitignore @@ -0,0 +1 @@ +/test_cells.tmp/ diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index e5da6c1e7e1..639c6f12950 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -27,6 +27,7 @@ #include "kernel/sigtools.h" #include "kernel/celltypes.h" #include "kernel/log.h" +#include "kernel/mem.h" #include USING_YOSYS_NAMESPACE @@ -68,12 +69,15 @@ struct BtorWorker // ff inputs that need to be evaluated (, ) vector> ff_todo; + vector> mem_todo; pool cell_recursion_guard; vector bad_properties; dict initbits; pool statewires; pool srcsymbols; + vector memories; + dict mem_cells; string indent, info_filename; vector info_lines; @@ -205,9 +209,8 @@ struct BtorWorker if (cell->type.in(ID($xnor), ID($_XNOR_))) btor_op = "xnor"; log_assert(!btor_op.empty()); - int width = GetSize(cell->getPort(ID::Y)); - width = std::max(width, GetSize(cell->getPort(ID::A))); - width = std::max(width, GetSize(cell->getPort(ID::B))); + int width_ay = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y))); + int width = std::max(width_ay, GetSize(cell->getPort(ID::B))); bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false; bool b_signed = cell->hasParam(ID::B_SIGNED) ? cell->getParam(ID::B_SIGNED).as_bool() : false; @@ -224,11 +227,23 @@ struct BtorWorker int sid = get_bv_sid(width); int nid; + int nid_a; + if (cell->type.in(ID($shl), ID($shr), ID($shift), ID($shiftx)) && a_signed && width_ay < width) { + // sign-extend A up to the width of Y + int nid_a_padded = get_sig_nid(cell->getPort(ID::A), width_ay, a_signed); + + // zero-extend the rest + int zeroes = get_sig_nid(Const(0, width-width_ay)); + nid_a = next_nid++; + btorf("%d concat %d %d %d\n", nid_a, sid, zeroes, nid_a_padded); + } else { + nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); + } + + int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); + if (btor_op == "shift") { - int nid_a = get_sig_nid(cell->getPort(ID::A), width, false); - int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); - int nid_r = next_nid++; btorf("%d srl %d %d %d\n", nid_r, sid, nid_a, nid_b); @@ -248,9 +263,6 @@ struct BtorWorker } else { - int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed); - int nid_b = get_sig_nid(cell->getPort(ID::B), width, b_signed); - nid = next_nid++; btorf("%d %s %d %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, nid_b, getinfo(cell).c_str()); } @@ -696,49 +708,45 @@ struct BtorWorker goto okay; } - if (cell->type == ID($mem)) + if (cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) { - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int nwords = cell->getParam(ID::SIZE).as_int(); - int rdports = cell->getParam(ID::RD_PORTS).as_int(); - int wrports = cell->getParam(ID::WR_PORTS).as_int(); + Mem *mem = mem_cells[cell]; - Const wr_clk_en = cell->getParam(ID::WR_CLK_ENABLE); - Const rd_clk_en = cell->getParam(ID::RD_CLK_ENABLE); + int abits = ceil_log2(mem->size); - bool asyncwr = wr_clk_en.is_fully_zero(); + bool asyncwr = false; + bool syncwr = false; - if (!asyncwr && !wr_clk_en.is_fully_ones()) - log_error("Memory %s.%s has mixed async/sync write ports.\n", - log_id(module), log_id(cell)); - - if (!rd_clk_en.is_fully_zero()) - log_error("Memory %s.%s has sync read ports.\n", - log_id(module), log_id(cell)); + for (auto &port : mem->wr_ports) { + if (port.clk_enable) + syncwr = true; + else + asyncwr = true; + } - SigSpec sig_rd_addr = sigmap(cell->getPort(ID::RD_ADDR)); - SigSpec sig_rd_data = sigmap(cell->getPort(ID::RD_DATA)); + if (asyncwr && syncwr) + log_error("Memory %s.%s has mixed async/sync write ports.\n", + log_id(module), log_id(mem->memid)); - SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR)); - SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA)); - SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN)); + for (auto &port : mem->rd_ports) + if (port.clk_enable) + log_error("Memory %s.%s has sync read ports.\n", + log_id(module), log_id(mem->memid)); - int data_sid = get_bv_sid(width); + int data_sid = get_bv_sid(mem->width); int bool_sid = get_bv_sid(1); - int sid = get_mem_sid(abits, width); + int sid = get_mem_sid(abits, mem->width); - Const initdata = cell->getParam(ID::INIT); - initdata.exts(nwords*width); int nid_init_val = -1; - if (!initdata.is_fully_undef()) + if (!mem->inits.empty()) { + Const initdata = mem->get_init_data(); bool constword = true; - Const firstword = initdata.extract(0, width); + Const firstword = initdata.extract(0, mem->width); - for (int i = 1; i < nwords; i++) { - Const thisword = initdata.extract(i*width, width); + for (int i = 1; i < mem->size; i++) { + Const thisword = initdata.extract(i*mem->width, mem->width); if (thisword != firstword) { constword = false; break; @@ -756,8 +764,8 @@ struct BtorWorker nid_init_val = next_nid++; btorf("%d state %d\n", nid_init_val, sid); - for (int i = 0; i < nwords; i++) { - Const thisword = initdata.extract(i*width, width); + for (int i = 0; i < mem->size; i++) { + Const thisword = initdata.extract(i*mem->width, mem->width); if (thisword.is_fully_undef()) continue; Const thisaddr(i, abits); @@ -776,10 +784,10 @@ struct BtorWorker int nid = next_nid++; int nid_head = nid; - if (cell->name[0] == '$') + if (mem->memid[0] == '$') btorf("%d state %d\n", nid, sid); else - btorf("%d state %d %s\n", nid, sid, log_id(cell)); + btorf("%d state %d %s\n", nid, sid, log_id(mem->memid)); if (nid_init_val >= 0) { @@ -789,15 +797,14 @@ struct BtorWorker if (asyncwr) { - for (int port = 0; port < wrports; port++) + for (auto &port : mem->wr_ports) { - SigSpec wa = sig_wr_addr.extract(port*abits, abits); - SigSpec wd = sig_wr_data.extract(port*width, width); - SigSpec we = sig_wr_en.extract(port*width, width); + SigSpec wa = port.addr; + wa.extend_u0(abits); int wa_nid = get_sig_nid(wa); - int wd_nid = get_sig_nid(wd); - int we_nid = get_sig_nid(we); + int wd_nid = get_sig_nid(port.data); + int we_nid = get_sig_nid(port.en); int nid2 = next_nid++; btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); @@ -827,22 +834,22 @@ struct BtorWorker } } - for (int port = 0; port < rdports; port++) + for (auto &port : mem->rd_ports) { - SigSpec ra = sig_rd_addr.extract(port*abits, abits); - SigSpec rd = sig_rd_data.extract(port*width, width); + SigSpec ra = port.addr; + ra.extend_u0(abits); int ra_nid = get_sig_nid(ra); int rd_nid = next_nid++; btorf("%d read %d %d %d\n", rd_nid, data_sid, nid_head, ra_nid); - add_nid_sig(rd_nid, rd); + add_nid_sig(rd_nid, port.data); } if (!asyncwr) { - ff_todo.push_back(make_pair(nid, cell)); + mem_todo.push_back(make_pair(nid, mem)); } else { @@ -1057,6 +1064,15 @@ struct BtorWorker if (!info_filename.empty()) infof("name %s\n", log_id(module)); + memories = Mem::get_all_memories(module); + + dict mem_dict; + for (auto &mem : memories) + mem_dict[mem.memid] = &mem; + for (auto cell : module->cells()) + if (cell->type.in(ID($mem), ID($memwr), ID($memrd), ID($meminit))) + mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()]; + btorf_push("inputs"); for (auto wire : module->wires()) @@ -1193,7 +1209,7 @@ struct BtorWorker continue; } - while (!ff_todo.empty()) + while (!ff_todo.empty() || !mem_todo.empty()) { vector> todo; todo.swap(ff_todo); @@ -1205,70 +1221,71 @@ struct BtorWorker btorf_push(stringf("next %s", log_id(cell))); - if (cell->type == ID($mem)) - { - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int wrports = cell->getParam(ID::WR_PORTS).as_int(); + SigSpec sig = sigmap(cell->getPort(ID::D)); + int nid_q = get_sig_nid(sig); + int sid = get_bv_sid(GetSize(sig)); + btorf("%d next %d %d %d%s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str()); - SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR)); - SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA)); - SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN)); + btorf_pop(stringf("next %s", log_id(cell))); + } - int data_sid = get_bv_sid(width); - int bool_sid = get_bv_sid(1); - int sid = get_mem_sid(abits, width); - int nid_head = nid; + vector> mtodo; + mtodo.swap(mem_todo); - for (int port = 0; port < wrports; port++) - { - SigSpec wa = sig_wr_addr.extract(port*abits, abits); - SigSpec wd = sig_wr_data.extract(port*width, width); - SigSpec we = sig_wr_en.extract(port*width, width); + for (auto &it : mtodo) + { + int nid = it.first; + Mem *mem = it.second; + + btorf_push(stringf("next %s", log_id(mem->memid))); + + int abits = ceil_log2(mem->size); - int wa_nid = get_sig_nid(wa); - int wd_nid = get_sig_nid(wd); - int we_nid = get_sig_nid(we); + int data_sid = get_bv_sid(mem->width); + int bool_sid = get_bv_sid(1); + int sid = get_mem_sid(abits, mem->width); + int nid_head = nid; - int nid2 = next_nid++; - btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); + for (auto &port : mem->wr_ports) + { + SigSpec wa = port.addr; + wa.extend_u0(abits); - int nid3 = next_nid++; - btorf("%d not %d %d\n", nid3, data_sid, we_nid); + int wa_nid = get_sig_nid(wa); + int wd_nid = get_sig_nid(port.data); + int we_nid = get_sig_nid(port.en); - int nid4 = next_nid++; - btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); + int nid2 = next_nid++; + btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid); + + int nid3 = next_nid++; + btorf("%d not %d %d\n", nid3, data_sid, we_nid); - int nid5 = next_nid++; - btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid); + int nid4 = next_nid++; + btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3); - int nid6 = next_nid++; - btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); + int nid5 = next_nid++; + btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid); - int nid7 = next_nid++; - btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); + int nid6 = next_nid++; + btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4); - int nid8 = next_nid++; - btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); + int nid7 = next_nid++; + btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6); - int nid9 = next_nid++; - btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); + int nid8 = next_nid++; + btorf("%d redor %d %d\n", nid8, bool_sid, we_nid); - nid_head = nid9; - } + int nid9 = next_nid++; + btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head); - int nid2 = next_nid++; - btorf("%d next %d %d %d%s\n", nid2, sid, nid, nid_head, getinfo(cell).c_str()); - } - else - { - SigSpec sig = sigmap(cell->getPort(ID::D)); - int nid_q = get_sig_nid(sig); - int sid = get_bv_sid(GetSize(sig)); - btorf("%d next %d %d %d%s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str()); + nid_head = nid9; } - btorf_pop(stringf("next %s", log_id(cell))); + int nid2 = next_nid++; + btorf("%d next %d %d %d%s\n", nid2, sid, nid, nid_head, (mem->cell ? getinfo(mem->cell) : getinfo(mem->mem)).c_str()); + + btorf_pop(stringf("next %s", log_id(mem->memid))); } } diff --git a/backends/btor/test_cells.sh b/backends/btor/test_cells.sh old mode 100644 new mode 100755 index 3f077201a0e..0a011932d22 --- a/backends/btor/test_cells.sh +++ b/backends/btor/test_cells.sh @@ -6,7 +6,7 @@ rm -rf test_cells.tmp mkdir -p test_cells.tmp cd test_cells.tmp -../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor' +../../../yosys -p 'test_cell -n 5 -w test all /$alu /$fa /$lcu /$lut /$sop /$macc /$mul /$div /$mod /$divfloor /$modfloor /$shiftx' for fn in test_*.il; do ../../../yosys -p " @@ -19,7 +19,7 @@ for fn in test_*.il; do hierarchy -top main write_btor ${fn%.il}.btor " - boolectormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out + btormc -kmax 1 --trace-gen --stop-first -v ${fn%.il}.btor > ${fn%.il}.out if grep " SATISFIABLE" ${fn%.il}.out; then echo "Check failed for ${fn%.il}." exit 1 diff --git a/backends/cxxrtl/cxxrtl.h b/backends/cxxrtl/cxxrtl.h index f0d7b9fc7a0..41089a153d5 100644 --- a/backends/cxxrtl/cxxrtl.h +++ b/backends/cxxrtl/cxxrtl.h @@ -452,10 +452,11 @@ struct value : public expr_base> { bool carry = CarryIn; for (size_t n = 0; n < result.chunks; n++) { result.data[n] = data[n] + (Invert ? ~other.data[n] : other.data[n]) + carry; + if (result.chunks - 1 == n) + result.data[result.chunks - 1] &= result.msb_mask; carry = (result.data[n] < data[n]) || (result.data[n] == data[n] && carry); } - result.data[result.chunks - 1] &= result.msb_mask; return {result, carry}; } @@ -823,6 +824,7 @@ struct debug_alias {}; // To avoid violating strict aliasing rules, this structure has to be a subclass of the one used // in the C API, or it would not be possible to cast between the pointers to these. struct debug_item : ::cxxrtl_object { + // Object types. enum : uint32_t { VALUE = CXXRTL_VALUE, WIRE = CXXRTL_WIRE, @@ -830,13 +832,24 @@ struct debug_item : ::cxxrtl_object { ALIAS = CXXRTL_ALIAS, }; + // Object flags. + enum : uint32_t { + INPUT = CXXRTL_INPUT, + OUTPUT = CXXRTL_OUTPUT, + INOUT = CXXRTL_INOUT, + DRIVEN_SYNC = CXXRTL_DRIVEN_SYNC, + DRIVEN_COMB = CXXRTL_DRIVEN_COMB, + UNDRIVEN = CXXRTL_UNDRIVEN, + }; + debug_item(const ::cxxrtl_object &object) : cxxrtl_object(object) {} template - debug_item(value &item, size_t lsb_offset = 0) { + debug_item(value &item, size_t lsb_offset = 0, uint32_t flags_ = 0) { static_assert(sizeof(item) == value::chunks * sizeof(chunk_t), "value is not compatible with C layout"); type = VALUE; + flags = flags_; width = Bits; lsb_at = lsb_offset; depth = 1; @@ -850,6 +863,7 @@ struct debug_item : ::cxxrtl_object { static_assert(sizeof(item) == value::chunks * sizeof(chunk_t), "value is not compatible with C layout"); type = VALUE; + flags = DRIVEN_COMB; width = Bits; lsb_at = lsb_offset; depth = 1; @@ -859,11 +873,12 @@ struct debug_item : ::cxxrtl_object { } template - debug_item(wire &item, size_t lsb_offset = 0) { + debug_item(wire &item, size_t lsb_offset = 0, uint32_t flags_ = 0) { static_assert(sizeof(item.curr) == value::chunks * sizeof(chunk_t) && sizeof(item.next) == value::chunks * sizeof(chunk_t), "wire is not compatible with C layout"); type = WIRE; + flags = flags_; width = Bits; lsb_at = lsb_offset; depth = 1; @@ -877,6 +892,7 @@ struct debug_item : ::cxxrtl_object { static_assert(sizeof(item.data[0]) == value::chunks * sizeof(chunk_t), "memory is not compatible with C layout"); type = MEMORY; + flags = 0; width = Width; lsb_at = 0; depth = item.data.size(); @@ -890,6 +906,7 @@ struct debug_item : ::cxxrtl_object { static_assert(sizeof(item) == value::chunks * sizeof(chunk_t), "value is not compatible with C layout"); type = ALIAS; + flags = DRIVEN_COMB; width = Bits; lsb_at = lsb_offset; depth = 1; @@ -904,6 +921,7 @@ struct debug_item : ::cxxrtl_object { sizeof(item.next) == value::chunks * sizeof(chunk_t), "wire is not compatible with C layout"); type = ALIAS; + flags = DRIVEN_COMB; width = Bits; lsb_at = lsb_offset; depth = 1; diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index 5e5ba5ac0f0..a48ea5b23a8 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/backends/cxxrtl/cxxrtl_backend.cc @@ -22,6 +22,7 @@ #include "kernel/sigtools.h" #include "kernel/utils.h" #include "kernel/celltypes.h" +#include "kernel/mem.h" #include "kernel/log.h" USING_YOSYS_NAMESPACE @@ -200,16 +201,12 @@ bool is_elidable_cell(RTLIL::IdString type) ID($mux), ID($concat), ID($slice), ID($pmux)); } -bool is_sync_ff_cell(RTLIL::IdString type) -{ - return type.in( - ID($dff), ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)); -} - bool is_ff_cell(RTLIL::IdString type) { - return is_sync_ff_cell(type) || type.in( - ID($adff), ID($adffe), ID($dffsr), ID($dffsre), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr)); + return type.in( + ID($dff), ID($dffe), ID($sdff), ID($sdffe), ID($sdffce), + ID($adff), ID($adffe), ID($dffsr), ID($dffsre), + ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr)); } bool is_internal_cell(RTLIL::IdString type) @@ -277,6 +274,7 @@ struct FlowGraph { std::vector nodes; dict> wire_comb_defs, wire_sync_defs, wire_uses; dict wire_def_elidable, wire_use_elidable; + dict bit_has_state; ~FlowGraph() { @@ -284,17 +282,24 @@ struct FlowGraph { delete node; } - void add_defs(Node *node, const RTLIL::SigSpec &sig, bool fully_sync, bool elidable) + void add_defs(Node *node, const RTLIL::SigSpec &sig, bool is_ff, bool elidable) { for (auto chunk : sig.chunks()) if (chunk.wire) { - if (fully_sync) + if (is_ff) { + // A sync def means that a wire holds design state because it is driven directly by + // a flip-flop output. Such a wire can never be unbuffered. wire_sync_defs[chunk.wire].insert(node); - else + } else { + // A comb def means that a wire doesn't hold design state. It might still be connected, + // indirectly, to a flip-flop output. wire_comb_defs[chunk.wire].insert(node); + } } + for (auto bit : sig.bits()) + bit_has_state[bit] |= is_ff; // Only comb defs of an entire wire in the right order can be elided. - if (!fully_sync && sig.is_wire()) + if (!is_ff && sig.is_wire()) wire_def_elidable[sig.as_wire()] = elidable; } @@ -322,7 +327,7 @@ struct FlowGraph { // Connections void add_connect_defs_uses(Node *node, const RTLIL::SigSig &conn) { - add_defs(node, conn.first, /*fully_sync=*/false, /*elidable=*/true); + add_defs(node, conn.first, /*is_ff=*/false, /*elidable=*/true); add_uses(node, conn.second); } @@ -369,7 +374,7 @@ struct FlowGraph { if (cell->output(conn.first)) if (is_cxxrtl_sync_port(cell, conn.first)) { // See note regarding elidability below. - add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/false); + add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/false); } } @@ -378,18 +383,18 @@ struct FlowGraph { for (auto conn : cell->connections()) { if (cell->output(conn.first)) { if (is_elidable_cell(cell->type)) - add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/true); - else if (is_sync_ff_cell(cell->type) || (cell->type == ID($memrd) && cell->getParam(ID::CLK_ENABLE).as_bool())) - add_defs(node, conn.second, /*fully_sync=*/true, /*elidable=*/false); + add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/true); + else if (is_ff_cell(cell->type) || (cell->type == ID($memrd) && cell->getParam(ID::CLK_ENABLE).as_bool())) + add_defs(node, conn.second, /*is_ff=*/true, /*elidable=*/false); else if (is_internal_cell(cell->type)) - add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/false); + add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/false); else if (!is_cxxrtl_sync_port(cell, conn.first)) { // Although at first it looks like outputs of user-defined cells may always be elided, the reality is // more complex. Fully sync outputs produce no defs and so don't participate in elision. Fully comb // outputs are assigned in a different way depending on whether the cell's eval() immediately converged. // Unknown/mixed outputs could be elided, but should be rare in practical designs and don't justify // the infrastructure required to elide outputs of cells with many of them. - add_defs(node, conn.second, /*fully_sync=*/false, /*elidable=*/false); + add_defs(node, conn.second, /*is_ff=*/false, /*elidable=*/false); } } if (cell->input(conn.first)) @@ -427,7 +432,7 @@ struct FlowGraph { void add_case_defs_uses(Node *node, const RTLIL::CaseRule *case_) { for (auto &action : case_->actions) { - add_defs(node, action.first, /*is_sync=*/false, /*elidable=*/false); + add_defs(node, action.first, /*is_ff=*/false, /*elidable=*/false); add_uses(node, action.second); } for (auto sub_switch : case_->switches) { @@ -446,9 +451,9 @@ struct FlowGraph { for (auto sync : process->syncs) for (auto action : sync->actions) { if (sync->type == RTLIL::STp || sync->type == RTLIL::STn || sync->type == RTLIL::STe) - add_defs(node, action.first, /*is_sync=*/true, /*elidable=*/false); + add_defs(node, action.first, /*is_ff=*/true, /*elidable=*/false); else - add_defs(node, action.first, /*is_sync=*/false, /*elidable=*/false); + add_defs(node, action.first, /*is_ff=*/false, /*elidable=*/false); add_uses(node, action.second); } } @@ -522,6 +527,7 @@ struct CxxrtlWorker { std::ostream *impl_f = nullptr; std::ostream *intf_f = nullptr; + bool run_hierarchy = false; bool run_flatten = false; bool run_proc = false; @@ -549,6 +555,7 @@ struct CxxrtlWorker { pool localized_wires; dict debug_alias_wires; dict debug_const_wires; + dict bit_has_state; dict> blackbox_specializations; dict eval_converges; @@ -1142,7 +1149,7 @@ struct CxxrtlWorker { } // The generated code has two bounds checks; one in an assertion, and another that guards the read. // This is done so that the code does not invoke undefined behavior under any conditions, but nevertheless - // loudly crashes if an illegal condition is encountered. The assert may be turned off with -NDEBUG not + // loudly crashes if an illegal condition is encountered. The assert may be turned off with -DNDEBUG not // just for release builds, but also to make sure the simulator (which is presumably embedded in some // larger program) will never crash the code that calls into it. // @@ -1635,6 +1642,10 @@ struct CxxrtlWorker { size_t count_alias_wires = 0; size_t count_member_wires = 0; size_t count_skipped_wires = 0; + size_t count_driven_sync = 0; + size_t count_driven_comb = 0; + size_t count_undriven = 0; + size_t count_mixed_driver = 0; inc_indent(); f << indent << "assert(path.empty() || path[path.size() - 1] == ' ');\n"; for (auto wire : module->wires()) { @@ -1660,9 +1671,55 @@ struct CxxrtlWorker { count_alias_wires++; } else if (!localized_wires.count(wire)) { // Member wire + std::vector flags; + + if (wire->port_input && wire->port_output) + flags.push_back("INOUT"); + else if (wire->port_input) + flags.push_back("INPUT"); + else if (wire->port_output) + flags.push_back("OUTPUT"); + + bool has_driven_sync = false; + bool has_driven_comb = false; + bool has_undriven = false; + SigSpec sig(wire); + for (auto bit : sig.bits()) + if (!bit_has_state.count(bit)) + has_undriven = true; + else if (bit_has_state[bit]) + has_driven_sync = true; + else + has_driven_comb = true; + if (has_driven_sync) + flags.push_back("DRIVEN_SYNC"); + if (has_driven_sync && !has_driven_comb && !has_undriven) + count_driven_sync++; + if (has_driven_comb) + flags.push_back("DRIVEN_COMB"); + if (!has_driven_sync && has_driven_comb && !has_undriven) + count_driven_comb++; + if (has_undriven) + flags.push_back("UNDRIVEN"); + if (!has_driven_sync && !has_driven_comb && has_undriven) + count_undriven++; + if (has_driven_sync + has_driven_comb + has_undriven > 1) + count_mixed_driver++; + f << indent << "items.add(path + " << escape_cxx_string(get_hdl_name(wire)); f << ", debug_item(" << mangle(wire) << ", "; - f << wire->start_offset << "));\n"; + f << wire->start_offset; + bool first = true; + for (auto flag : flags) { + if (first) { + first = false; + f << ", "; + } else { + f << "|"; + } + f << "debug_item::" << flag; + } + f << "));\n"; count_member_wires++; } else { count_skipped_wires++; @@ -1690,7 +1747,11 @@ struct CxxrtlWorker { log_debug(" Public wires: %zu, of which:\n", count_public_wires); log_debug(" Const wires: %zu\n", count_const_wires); log_debug(" Alias wires: %zu\n", count_alias_wires); - log_debug(" Member wires: %zu\n", count_member_wires); + log_debug(" Member wires: %zu, of which:\n", count_member_wires); + log_debug(" Driven sync: %zu\n", count_driven_sync); + log_debug(" Driven comb: %zu\n", count_driven_comb); + log_debug(" Undriven: %zu\n", count_undriven); + log_debug(" Mixed driver: %zu\n", count_mixed_driver); log_debug(" Other wires: %zu (no debug information)\n", count_skipped_wires); } @@ -1935,6 +1996,7 @@ struct CxxrtlWorker { f << "} // namespace " << design_ns << "\n"; f << "\n"; if (top_module != nullptr && debug_info) { + f << "extern \"C\"\n"; f << "cxxrtl_toplevel " << design_ns << "_create() {\n"; inc_indent(); std::string top_type = design_ns + "::" + mangle(top_module); @@ -2122,6 +2184,8 @@ struct CxxrtlWorker { if (wire->name.begins_with("$") && !elide_internal) continue; if (wire->name.begins_with("\\") && !elide_public) continue; if (edge_wires[wire]) continue; + if (flow.wire_comb_defs[wire].size() > 1) + log_cmd_error("Wire %s.%s has multiple drivers.\n", log_id(module), log_id(wire)); log_assert(flow.wire_comb_defs[wire].size() == 1); elided_wires[wire] = **flow.wire_comb_defs[wire].begin(); } @@ -2208,6 +2272,9 @@ struct CxxrtlWorker { eval_converges[module] = feedback_wires.empty() && buffered_comb_wires.empty(); + for (auto item : flow.bit_has_state) + bit_has_state.insert(item); + if (debug_info) { // Find wires that alias other wires or are tied to a constant; debug information can be enriched with these // at essentially zero additional cost. @@ -2263,9 +2330,9 @@ struct CxxrtlWorker { } } - void check_design(RTLIL::Design *design, bool &has_sync_init, bool &has_packed_mem) + void check_design(RTLIL::Design *design, bool &has_top, bool &has_sync_init, bool &has_packed_mem) { - has_sync_init = has_packed_mem = false; + has_sync_init = has_packed_mem = has_top = false; for (auto module : design->modules()) { if (module->get_blackbox_attribute() && !module->has_attribute(ID(cxxrtl_blackbox))) @@ -2277,13 +2344,17 @@ struct CxxrtlWorker { if (!design->selected_module(module)) continue; + if (module->get_bool_attribute(ID::top)) + has_top = true; + for (auto proc : module->processes) for (auto sync : proc.second->syncs) if (sync->type == RTLIL::STi) has_sync_init = true; - for (auto cell : module->cells()) - if (cell->type == ID($mem)) + // The Mem constructor also checks for well-formedness of $meminit cells, if any. + for (auto &mem : Mem::get_all_memories(module)) + if (mem.packed) has_packed_mem = true; } } @@ -2291,9 +2362,13 @@ struct CxxrtlWorker { void prepare_design(RTLIL::Design *design) { bool did_anything = false; - bool has_sync_init, has_packed_mem; + bool has_top, has_sync_init, has_packed_mem; log_push(); - check_design(design, has_sync_init, has_packed_mem); + check_design(design, has_top, has_sync_init, has_packed_mem); + if (run_hierarchy && !has_top) { + Pass::call(design, "hierarchy -auto-top"); + did_anything = true; + } if (run_flatten) { Pass::call(design, "flatten"); did_anything = true; @@ -2314,9 +2389,9 @@ struct CxxrtlWorker { did_anything = true; } // Recheck the design if it was modified. - if (has_sync_init || has_packed_mem) - check_design(design, has_sync_init, has_packed_mem); - log_assert(!(has_sync_init || has_packed_mem)); + if (did_anything) + check_design(design, has_top, has_sync_init, has_packed_mem); + log_assert(has_top && !has_sync_init && !has_packed_mem); log_pop(); if (did_anything) log_spacer(); @@ -2498,6 +2573,11 @@ struct CxxrtlBackend : public Backend { log(" place the generated code into namespace . if not specified,\n"); log(" \"cxxrtl_design\" is used.\n"); log("\n"); + log(" -nohierarchy\n"); + log(" use design hierarchy as-is. in most designs, a top module should be\n"); + log(" present as it is exposed through the C API and has unbuffered outputs\n"); + log(" for improved performance; it will be determined automatically if absent.\n"); + log("\n"); log(" -noflatten\n"); log(" don't flatten the design. fully flattened designs can evaluate within\n"); log(" one delta cycle if they have no combinatorial feedback.\n"); @@ -2554,6 +2634,7 @@ struct CxxrtlBackend : public Backend { void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override { + bool nohierarchy = false; bool noflatten = false; bool noproc = false; int opt_level = DEFAULT_OPT_LEVEL; @@ -2565,6 +2646,10 @@ struct CxxrtlBackend : public Backend { size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-nohierarchy") { + nohierarchy = true; + continue; + } if (args[argidx] == "-noflatten") { noflatten = true; continue; @@ -2610,6 +2695,7 @@ struct CxxrtlBackend : public Backend { } extra_args(f, filename, args, argidx); + worker.run_hierarchy = !nohierarchy; worker.run_flatten = !noflatten; worker.run_proc = !noproc; switch (opt_level) { diff --git a/backends/cxxrtl/cxxrtl_capi.cc b/backends/cxxrtl/cxxrtl_capi.cc index e0566e152ae..b77e4c49141 100644 --- a/backends/cxxrtl/cxxrtl_capi.cc +++ b/backends/cxxrtl/cxxrtl_capi.cc @@ -43,6 +43,14 @@ void cxxrtl_destroy(cxxrtl_handle handle) { delete handle; } +int cxxrtl_eval(cxxrtl_handle handle) { + return handle->module->eval(); +} + +int cxxrtl_commit(cxxrtl_handle handle) { + return handle->module->commit(); +} + size_t cxxrtl_step(cxxrtl_handle handle) { return handle->module->step(); } diff --git a/backends/cxxrtl/cxxrtl_capi.h b/backends/cxxrtl/cxxrtl_capi.h index 599284898c0..385d6dcf386 100644 --- a/backends/cxxrtl/cxxrtl_capi.h +++ b/backends/cxxrtl/cxxrtl_capi.h @@ -55,12 +55,28 @@ cxxrtl_handle cxxrtl_create(cxxrtl_toplevel design); // Release all resources used by a design and its handle. void cxxrtl_destroy(cxxrtl_handle handle); +// Evaluate the design, propagating changes on inputs to the `next` value of internal state and +// output wires. +// +// Returns 1 if the design is known to immediately converge, 0 otherwise. +int cxxrtl_eval(cxxrtl_handle handle); + +// Commit the design, replacing the `curr` value of internal state and output wires with the `next` +// value. +// +// Return 1 if any of the `curr` values were updated, 0 otherwise. +int cxxrtl_commit(cxxrtl_handle handle); + // Simulate the design to a fixed point. // // Returns the number of delta cycles. size_t cxxrtl_step(cxxrtl_handle handle); // Type of a simulated object. +// +// The type of a simulated object indicates the way it is stored and the operations that are legal +// to perform on it (i.e. won't crash the simulation). It says very little about object semantics, +// which is specified through flags. enum cxxrtl_type { // Values correspond to singly buffered netlist nodes, i.e. nodes driven exclusively by // combinatorial cells, or toplevel input nodes. @@ -74,7 +90,8 @@ enum cxxrtl_type { CXXRTL_VALUE = 0, // Wires correspond to doubly buffered netlist nodes, i.e. nodes driven, at least in part, by - // storage cells, or by combinatorial cells that are a part of a feedback path. + // storage cells, or by combinatorial cells that are a part of a feedback path. They are also + // present in non-optimized builds. // // Wires can be inspected via the `curr` pointer and modified via the `next` pointer (which are // distinct for wires). Note that changes to the bits driven by combinatorial cells will be @@ -91,7 +108,7 @@ enum cxxrtl_type { CXXRTL_MEMORY = 2, // Aliases correspond to netlist nodes driven by another node such that their value is always - // exactly equal, or driven by a constant value. + // exactly equal. // // Aliases can be inspected via the `curr` pointer. They cannot be modified, and the `next` // pointer is always NULL. @@ -100,6 +117,66 @@ enum cxxrtl_type { // More object types may be added in the future, but the existing ones will never change. }; +// Flags of a simulated object. +// +// The flags of a simulated object indicate its role in the netlist: +// * The flags `CXXRTL_INPUT` and `CXXRTL_OUTPUT` designate module ports. +// * The flags `CXXRTL_DRIVEN_SYNC`, `CXXRTL_DRIVEN_COMB`, and `CXXRTL_UNDRIVEN` specify +// the semantics of node state. An object with several of these flags set has different bits +// follow different semantics. +enum cxxrtl_flag { + // Node is a module input port. + // + // This flag can be set on objects of type `CXXRTL_VALUE` and `CXXRTL_WIRE`. It may be combined + // with `CXXRTL_OUTPUT`, as well as other flags. + CXXRTL_INPUT = 1 << 0, + + // Node is a module output port. + // + // This flag can be set on objects of type `CXXRTL_WIRE`. It may be combined with `CXXRTL_INPUT`, + // as well as other flags. + CXXRTL_OUTPUT = 1 << 1, + + // Node is a module inout port. + // + // This flag can be set on objects of type `CXXRTL_WIRE`. It may be combined with other flags. + CXXRTL_INOUT = (CXXRTL_INPUT|CXXRTL_OUTPUT), + + // Node has bits that are driven by a storage cell. + // + // This flag can be set on objects of type `CXXRTL_WIRE`. It may be combined with + // `CXXRTL_DRIVEN_COMB` and `CXXRTL_UNDRIVEN`, as well as other flags. + // + // This flag is set on wires that have bits connected directly to the output of a flip-flop or + // a latch, and hold its state. Many `CXXRTL_WIRE` objects may not have the `CXXRTL_DRIVEN_SYNC` + // flag set; for example, output ports and feedback wires generally won't. Writing to the `next` + // pointer of these wires updates stored state, and for designs without combinatorial loops, + // capturing the value from every of these wires through the `curr` pointer creates a complete + // snapshot of the design state. + CXXRTL_DRIVEN_SYNC = 1 << 2, + + // Node has bits that are driven by a combinatorial cell or another node. + // + // This flag can be set on objects of type `CXXRTL_VALUE` and `CXXRTL_WIRE`. It may be combined + // with `CXXRTL_DRIVEN_SYNC` and `CXXRTL_UNDRIVEN`, as well as other flags. + // + // This flag is set on objects that have bits connected to the output of a combinatorial cell, + // or directly to another node. For designs without combinatorial loops, writing to such bits + // through the `next` pointer (if it is not NULL) has no effect. + CXXRTL_DRIVEN_COMB = 1 << 3, + + // Node has bits that are not driven. + // + // This flag can be set on objects of type `CXXRTL_VALUE` and `CXXRTL_WIRE`. It may be combined + // with `CXXRTL_DRIVEN_SYNC` and `CXXRTL_DRIVEN_COMB`, as well as other flags. + // + // This flag is set on objects that have bits not driven by an output of any cell or by another + // node, such as inputs and dangling wires. + CXXRTL_UNDRIVEN = 1 << 4, + + // More object flags may be added in the future, but the existing ones will never change. +}; + // Description of a simulated object. // // The `data` array can be accessed directly to inspect and, if applicable, modify the bits @@ -111,6 +188,9 @@ struct cxxrtl_object { // determines all other properties of the object. uint32_t type; // actually `enum cxxrtl_type` + // Flags of the object. + uint32_t flags; // actually bit mask of `enum cxxrtl_flags` + // Width of the object in bits. size_t width; diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc index 5e6becfd03d..e0013238c83 100644 --- a/backends/edif/edif.cc +++ b/backends/edif/edif.cc @@ -330,7 +330,7 @@ struct EdifBackend : public Backend { } *f << stringf("\n (property %s (string \"%d'h%s\"))", EDIF_DEF(name), GetSize(val.bits), hex_string.c_str()); } - }; + }; for (auto module : sorted_modules) { if (module->get_blackbox_attribute()) @@ -373,8 +373,8 @@ struct EdifBackend : public Backend { } { - int c1 = w1->name[0] == '\\'; - int c2 = w2->name[0] == '\\'; + int c1 = w1->name.isPublic(); + int c2 = w2->name.isPublic(); if (c1 > c2) goto promote; if (c1 < c2) goto nopromote; @@ -524,7 +524,7 @@ struct EdifBackend : public Backend { *f << stringf(" (portRef %c (instanceRef GND))\n", gndvccy ? 'Y' : 'G'); if (sig == RTLIL::State::S1) *f << stringf(" (portRef %c (instanceRef VCC))\n", gndvccy ? 'Y' : 'P'); - } + } *f << stringf(" )"); if (attr_properties && sig.wire != NULL) for (auto &p : sig.wire->attributes) diff --git a/backends/ilang/Makefile.inc b/backends/ilang/Makefile.inc deleted file mode 100644 index 52fc2b891e7..00000000000 --- a/backends/ilang/Makefile.inc +++ /dev/null @@ -1,3 +0,0 @@ - -OBJS += backends/ilang/ilang_backend.o - diff --git a/backends/intersynth/intersynth.cc b/backends/intersynth/intersynth.cc index 98a14173b10..a6b36de6cba 100644 --- a/backends/intersynth/intersynth.cc +++ b/backends/intersynth/intersynth.cc @@ -59,7 +59,7 @@ struct IntersynthBackend : public Backend { log(" do not generate celltypes and conntypes commands. i.e. just output\n"); log(" the netlists. this is used for postsilicon synthesis.\n"); log("\n"); - log(" -lib \n"); + log(" -lib \n"); log(" Use the specified library file for determining whether cell ports are\n"); log(" inputs or outputs. This option can be used multiple times to specify\n"); log(" more than one library.\n"); @@ -108,7 +108,7 @@ struct IntersynthBackend : public Backend { if (f.fail()) log_error("Can't open lib file `%s'.\n", filename.c_str()); RTLIL::Design *lib = new RTLIL::Design; - Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0 ? "ilang" : "verilog")); + Frontend::frontend_call(lib, &f, filename, (filename.size() > 3 && filename.compare(filename.size()-3, std::string::npos, ".il") == 0 ? "rtlil" : "verilog")); libs.push_back(lib); } diff --git a/backends/rtlil/Makefile.inc b/backends/rtlil/Makefile.inc new file mode 100644 index 00000000000..f691282ca16 --- /dev/null +++ b/backends/rtlil/Makefile.inc @@ -0,0 +1,3 @@ + +OBJS += backends/rtlil/rtlil_backend.o + diff --git a/backends/ilang/ilang_backend.cc b/backends/rtlil/rtlil_backend.cc similarity index 88% rename from backends/ilang/ilang_backend.cc rename to backends/rtlil/rtlil_backend.cc index aa5a175ca29..01b4bde5330 100644 --- a/backends/ilang/ilang_backend.cc +++ b/backends/rtlil/rtlil_backend.cc @@ -18,19 +18,19 @@ * --- * * A very simple and straightforward backend for the RTLIL text - * representation (as understood by the 'ilang' frontend). + * representation. * */ -#include "ilang_backend.h" +#include "rtlil_backend.h" #include "kernel/yosys.h" #include USING_YOSYS_NAMESPACE -using namespace ILANG_BACKEND; +using namespace RTLIL_BACKEND; YOSYS_NAMESPACE_BEGIN -void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int width, int offset, bool autoint) +void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int width, int offset, bool autoint) { if (width < 0) width = data.bits.size() - offset; @@ -83,7 +83,7 @@ void ILANG_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi } } -void ILANG_BACKEND::dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool autoint) +void RTLIL_BACKEND::dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool autoint) { if (chunk.wire == NULL) { dump_const(f, chunk.data, chunk.width, chunk.offset, autoint); @@ -97,7 +97,7 @@ void ILANG_BACKEND::dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, } } -void ILANG_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, bool autoint) +void RTLIL_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, bool autoint) { if (sig.is_chunk()) { dump_sigchunk(f, sig.as_chunk(), autoint); @@ -111,7 +111,7 @@ void ILANG_BACKEND::dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, boo } } -void ILANG_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL::Wire *wire) +void RTLIL_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL::Wire *wire) { for (auto &it : wire->attributes) { f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str()); @@ -136,7 +136,7 @@ void ILANG_BACKEND::dump_wire(std::ostream &f, std::string indent, const RTLIL:: f << stringf("%s\n", wire->name.c_str()); } -void ILANG_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL::Memory *memory) +void RTLIL_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL::Memory *memory) { for (auto &it : memory->attributes) { f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str()); @@ -153,7 +153,7 @@ void ILANG_BACKEND::dump_memory(std::ostream &f, std::string indent, const RTLIL f << stringf("%s\n", memory->name.c_str()); } -void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::Cell *cell) +void RTLIL_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL::Cell *cell) { for (auto &it : cell->attributes) { f << stringf("%s" "attribute %s ", indent.c_str(), it.first.c_str()); @@ -177,7 +177,7 @@ void ILANG_BACKEND::dump_cell(std::ostream &f, std::string indent, const RTLIL:: f << stringf("%s" "end\n", indent.c_str()); } -void ILANG_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, const RTLIL::CaseRule *cs) +void RTLIL_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, const RTLIL::CaseRule *cs) { for (auto it = cs->actions.begin(); it != cs->actions.end(); ++it) { @@ -192,7 +192,7 @@ void ILANG_BACKEND::dump_proc_case_body(std::ostream &f, std::string indent, con dump_proc_switch(f, indent, *it); } -void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const RTLIL::SwitchRule *sw) +void RTLIL_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const RTLIL::SwitchRule *sw) { for (auto it = sw->attributes.begin(); it != sw->attributes.end(); ++it) { f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str()); @@ -225,7 +225,7 @@ void ILANG_BACKEND::dump_proc_switch(std::ostream &f, std::string indent, const f << stringf("%s" "end\n", indent.c_str()); } -void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RTLIL::SyncRule *sy) +void RTLIL_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RTLIL::SyncRule *sy) { f << stringf("%s" "sync ", indent.c_str()); switch (sy->type) { @@ -251,7 +251,7 @@ void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RT } } -void ILANG_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL::Process *proc) +void RTLIL_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL::Process *proc) { for (auto it = proc->attributes.begin(); it != proc->attributes.end(); ++it) { f << stringf("%s" "attribute %s ", indent.c_str(), it->first.c_str()); @@ -265,7 +265,7 @@ void ILANG_BACKEND::dump_proc(std::ostream &f, std::string indent, const RTLIL:: f << stringf("%s" "end\n", indent.c_str()); } -void ILANG_BACKEND::dump_conn(std::ostream &f, std::string indent, const RTLIL::SigSpec &left, const RTLIL::SigSpec &right) +void RTLIL_BACKEND::dump_conn(std::ostream &f, std::string indent, const RTLIL::SigSpec &left, const RTLIL::SigSpec &right) { f << stringf("%s" "connect ", indent.c_str()); dump_sigspec(f, left); @@ -274,7 +274,7 @@ void ILANG_BACKEND::dump_conn(std::ostream &f, std::string indent, const RTLIL:: f << stringf("\n"); } -void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Module *module, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n) +void RTLIL_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Module *module, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n) { bool print_header = flag_m || design->selected_whole_module(module->name); bool print_body = !flag_n || !design->selected_whole_module(module->name); @@ -360,7 +360,7 @@ void ILANG_BACKEND::dump_module(std::ostream &f, std::string indent, RTLIL::Modu f << stringf("%s" "end\n", indent.c_str()); } -void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n) +void RTLIL_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool only_selected, bool flag_m, bool flag_n) { int init_autoidx = autoidx; @@ -396,15 +396,15 @@ void ILANG_BACKEND::dump_design(std::ostream &f, RTLIL::Design *design, bool onl YOSYS_NAMESPACE_END PRIVATE_NAMESPACE_BEGIN -struct IlangBackend : public Backend { - IlangBackend() : Backend("ilang", "write design to ilang file") { } +struct RTLILBackend : public Backend { + RTLILBackend() : Backend("rtlil", "write design to RTLIL file") { } void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" write_ilang [filename]\n"); + log(" write_rtlil [filename]\n"); log("\n"); - log("Write the current design to an 'ilang' file. (ilang is a text representation\n"); + log("Write the current design to an RTLIL file. (RTLIL is a text representation\n"); log("of a design in yosys's internal format.)\n"); log("\n"); log(" -selected\n"); @@ -415,7 +415,7 @@ struct IlangBackend : public Backend { { bool selected = false; - log_header(design, "Executing ILANG backend.\n"); + log_header(design, "Executing RTLIL backend.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { @@ -432,12 +432,27 @@ struct IlangBackend : public Backend { log("Output filename: %s\n", filename.c_str()); *f << stringf("# Generated by %s\n", yosys_version_str); - ILANG_BACKEND::dump_design(*f, design, selected, true, false); + RTLIL_BACKEND::dump_design(*f, design, selected, true, false); + } +} RTLILBackend; + +struct IlangBackend : public Backend { + IlangBackend() : Backend("ilang", "(deprecated) alias of write_rtlil") { } + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log("See `help write_rtlil`.\n"); + log("\n"); + } + void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) override + { + RTLILBackend.execute(f, filename, args, design); } } IlangBackend; struct DumpPass : public Pass { - DumpPass() : Pass("dump", "print parts of the design in ilang format") { } + DumpPass() : Pass("dump", "print parts of the design in RTLIL format") { } void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| @@ -445,7 +460,7 @@ struct DumpPass : public Pass { log(" dump [options] [selection]\n"); log("\n"); log("Write the selected parts of the design to the console or specified file in\n"); - log("ilang format.\n"); + log("RTLIL format.\n"); log("\n"); log(" -m\n"); log(" also dump the module headers, even if only parts of a single\n"); @@ -508,7 +523,7 @@ struct DumpPass : public Pass { f = &buf; } - ILANG_BACKEND::dump_design(*f, design, true, flag_m, flag_n); + RTLIL_BACKEND::dump_design(*f, design, true, flag_m, flag_n); if (!filename.empty()) { delete f; diff --git a/backends/ilang/ilang_backend.h b/backends/rtlil/rtlil_backend.h similarity index 94% rename from backends/ilang/ilang_backend.h rename to backends/rtlil/rtlil_backend.h index 97dcbb6280d..77eea353ca9 100644 --- a/backends/ilang/ilang_backend.h +++ b/backends/rtlil/rtlil_backend.h @@ -18,19 +18,19 @@ * --- * * A very simple and straightforward backend for the RTLIL text - * representation (as understood by the 'ilang' frontend). + * representation. * */ -#ifndef ILANG_BACKEND_H -#define ILANG_BACKEND_H +#ifndef RTLIL_BACKEND_H +#define RTLIL_BACKEND_H #include "kernel/yosys.h" #include YOSYS_NAMESPACE_BEGIN -namespace ILANG_BACKEND { +namespace RTLIL_BACKEND { void dump_const(std::ostream &f, const RTLIL::Const &data, int width = -1, int offset = 0, bool autoint = true); void dump_sigchunk(std::ostream &f, const RTLIL::SigChunk &chunk, bool autoint = true); void dump_sigspec(std::ostream &f, const RTLIL::SigSpec &sig, bool autoint = true); diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 526b36352cb..a185fdd747d 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -22,6 +22,7 @@ #include "kernel/sigtools.h" #include "kernel/celltypes.h" #include "kernel/log.h" +#include "kernel/mem.h" #include USING_YOSYS_NAMESPACE @@ -40,12 +41,15 @@ struct Smt2Worker std::map bit_driver; std::set exported_cells, hiercells, hiercells_queue; pool recursive_cells, registers; + std::vector memories; + dict mem_cells; + std::set memory_queue; pool clock_posedge, clock_negedge; vector ex_state_eq, ex_input_eq; std::map> fcache; - std::map memarrays; + std::map memarrays; std::map bvsizes; dict ids; @@ -116,12 +120,73 @@ struct Smt2Worker makebits(stringf("%s_is", get_id(module))); + dict mem_dict; + memories = Mem::get_all_memories(module); + for (auto &mem : memories) + { + mem_dict[mem.memid] = &mem; + for (auto &port : mem.wr_ports) + { + if (port.clk_enable) { + SigSpec clk = sigmap(port.clk); + for (int i = 0; i < GetSize(clk); i++) + { + if (clk[i].wire == nullptr) + continue; + if (port.clk_polarity) + clock_posedge.insert(clk[i]); + else + clock_negedge.insert(clk[i]); + } + } + for (auto bit : sigmap(port.en)) + noclock.insert(bit); + for (auto bit : sigmap(port.addr)) + noclock.insert(bit); + for (auto bit : sigmap(port.data)) + noclock.insert(bit); + } + for (auto &port : mem.rd_ports) + { + if (port.clk_enable) { + SigSpec clk = sigmap(port.clk); + for (int i = 0; i < GetSize(clk); i++) + { + if (clk[i].wire == nullptr) + continue; + if (port.clk_polarity) + clock_posedge.insert(clk[i]); + else + clock_negedge.insert(clk[i]); + } + } + for (auto bit : sigmap(port.en)) + noclock.insert(bit); + for (auto bit : sigmap(port.addr)) + noclock.insert(bit); + for (auto bit : sigmap(port.data)) + noclock.insert(bit); + Cell *driver = port.cell ? port.cell : mem.cell; + for (auto bit : sigmap(port.data)) { + if (bit_driver.count(bit)) + log_error("Found multiple drivers for %s.\n", log_signal(bit)); + bit_driver[bit] = driver; + } + } + } + for (auto cell : module->cells()) for (auto &conn : cell->connections()) { if (GetSize(conn.second) == 0) continue; + // Handled above. + if (cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) { + mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()]; + continue; + } + bool is_input = ct.cell_input(cell->type, conn.first); bool is_output = ct.cell_output(cell->type, conn.first); @@ -135,24 +200,6 @@ struct Smt2Worker log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n", log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type)); - if (cell->type.in(ID($mem)) && conn.first.in(ID::RD_CLK, ID::WR_CLK)) - { - SigSpec clk = sigmap(conn.second); - for (int i = 0; i < GetSize(clk); i++) - { - if (clk[i].wire == nullptr) - continue; - - if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_ENABLE : ID::WR_CLK_ENABLE)[i] != State::S1) - continue; - - if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_POLARITY : ID::WR_CLK_POLARITY)[i] == State::S1) - clock_posedge.insert(clk[i]); - else - clock_negedge.insert(clk[i]); - } - } - else if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C)) { bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool()); @@ -647,27 +694,35 @@ struct Smt2Worker // FIXME: $slice $concat } - if (memmode && cell->type == ID($mem)) + if (memmode && cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) { + Mem *mem = mem_cells[cell]; + + if (memarrays.count(mem)) { + recursive_cells.erase(cell); + return; + } + int arrayid = idcounter++; - memarrays[cell] = arrayid; - - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int rd_ports = cell->getParam(ID::RD_PORTS).as_int(); - int wr_ports = cell->getParam(ID::WR_PORTS).as_int(); - - bool async_read = false; - if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) { - if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero()) - log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module)); - async_read = true; + memarrays[mem] = arrayid; + + int abits = ceil_log2(mem->size); + + bool has_sync_wr = false; + bool has_async_wr = false; + for (auto &port : mem->wr_ports) { + if (port.clk_enable) + has_sync_wr = true; + else + has_async_wr = true; } + if (has_async_wr && has_sync_wr) + log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module)); - decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(cell), abits, width, rd_ports, wr_ports, async_read ? "async" : "sync")); + decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync")); string memstate; - if (async_read) { + if (has_async_wr) { memstate = stringf("%s#%d#final", get_id(module), arrayid); } else { memstate = stringf("%s#%d#0", get_id(module), arrayid); @@ -675,80 +730,79 @@ struct Smt2Worker if (statebv) { - int mem_size = cell->getParam(ID::SIZE).as_int(); - int mem_offset = cell->getParam(ID::OFFSET).as_int(); - - makebits(memstate, width*mem_size, get_id(cell)); + makebits(memstate, mem->width*mem->size, get_id(mem->memid)); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n", - get_id(module), get_id(cell), get_id(module), width*mem_size, memstate.c_str())); + get_id(module), get_id(mem->memid), get_id(module), mem->width*mem->size, memstate.c_str())); - for (int i = 0; i < rd_ports; i++) + for (int i = 0; i < GetSize(mem->rd_ports); i++) { - SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); + auto &port = mem->rd_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); std::string addr = get_bv(addr_sig); - if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool()) + if (port.clk_enable) log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! " - "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module)); + "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module)); decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); + get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); std::string read_expr = "#b"; - for (int k = 0; k < width; k++) + for (int k = 0; k < mem->width; k++) read_expr += "0"; - for (int k = 0; k < mem_size; k++) + for (int k = 0; k < mem->size; k++) read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n %s)", - get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(), - width*(k+1)-1, width*k, memstate.c_str(), read_expr.c_str()); + get_id(module), i, get_id(mem->memid), Const(k+mem->start_offset, abits).as_string().c_str(), + mem->width*(k+1)-1, mem->width*k, memstate.c_str(), read_expr.c_str()); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n %s) ; %s\n", - get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig))); + get_id(module), idcounter, get_id(module), mem->width, read_expr.c_str(), log_signal(port.data))); decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n", - get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter)); + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter)); - register_bv(data_sig, idcounter++); + register_bv(port.data, idcounter++); } } else { if (statedt) dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - memstate.c_str(), abits, width, get_id(cell))); + memstate.c_str(), abits, mem->width, get_id(mem->memid))); else decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - memstate.c_str(), get_id(module), abits, width, get_id(cell))); + memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid))); decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n", - get_id(module), get_id(cell), get_id(module), abits, width, memstate.c_str())); + get_id(module), get_id(mem->memid), get_id(module), abits, mem->width, memstate.c_str())); - for (int i = 0; i < rd_ports; i++) + for (int i = 0; i < GetSize(mem->rd_ports); i++) { - SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); + auto &port = mem->rd_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); std::string addr = get_bv(addr_sig); - if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool()) + if (port.clk_enable) log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! " - "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module)); + "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module)); decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); + get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s| state) (|%s_m:R%dA %s| state))) ; %s\n", - get_id(module), idcounter, get_id(module), width, memstate.c_str(), get_id(module), i, get_id(cell), log_signal(data_sig))); + get_id(module), idcounter, get_id(module), mem->width, memstate.c_str(), get_id(module), i, get_id(mem->memid), log_signal(port.data))); decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n", - get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter)); + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter)); - register_bv(data_sig, idcounter++); + register_bv(port.data, idcounter++); } } - registers.insert(cell); + memory_queue.insert(mem); recursive_cells.erase(cell); return; } @@ -822,40 +876,51 @@ struct Smt2Worker for (auto bit : SigSpec(wire)) if (reg_bits.count(bit)) is_register = true; - if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) { + if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) { RTLIL::SigSpec sig = sigmap(wire); + std::vector comments; if (wire->port_input) - decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width)); + comments.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width)); if (wire->port_output) - decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width)); + comments.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width)); if (is_register) - decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); - if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) - decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); + comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); + if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) + comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) - decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), + comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : "")); if (bvmode && GetSize(sig) > 1) { + std::string sig_bv = get_bv(sig); + if (!comments.empty()) + decls.insert(decls.end(), comments.begin(), comments.end()); decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", - get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str())); + get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", get_id(module), get_id(wire), get_id(module), get_id(wire))); } else { - for (int i = 0; i < GetSize(sig); i++) + std::vector sig_bool; + for (int i = 0; i < GetSize(sig); i++) { + sig_bool.push_back(get_bool(sig[i])); + } + if (!comments.empty()) + decls.insert(decls.end(), comments.begin(), comments.end()); + for (int i = 0; i < GetSize(sig); i++) { if (GetSize(sig) > 1) { decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n", - get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str())); + get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))", get_id(module), get_id(wire), i, get_id(module), get_id(wire), i)); } else { decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", - get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str())); + get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", get_id(module), get_id(wire), get_id(module), get_id(wire))); } + } } } } @@ -966,7 +1031,7 @@ struct Smt2Worker } } - for (int iter = 1; !registers.empty(); iter++) + for (int iter = 1; !registers.empty() || !memory_queue.empty(); iter++) { pool this_regs; this_regs.swap(registers); @@ -999,152 +1064,156 @@ struct Smt2Worker if (cell->type == ID($anyconst)) ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str())); } + } - if (cell->type == ID($mem)) - { - int arrayid = memarrays.at(cell); + std::set this_mems; + this_mems.swap(memory_queue); + + for (auto mem : this_mems) + { + int arrayid = memarrays.at(mem); + + int abits = ceil_log2(mem->size);; + + bool has_sync_wr = false; + bool has_async_wr = false; + for (auto &port : mem->wr_ports) { + if (port.clk_enable) + has_sync_wr = true; + else + has_async_wr = true; + } - int abits = cell->getParam(ID::ABITS).as_int(); - int width = cell->getParam(ID::WIDTH).as_int(); - int wr_ports = cell->getParam(ID::WR_PORTS).as_int(); + string initial_memstate, final_memstate; - bool async_read = false; - string initial_memstate, final_memstate; + if (has_async_wr) { + log_assert(!has_sync_wr); + initial_memstate = stringf("%s#%d#0", get_id(module), arrayid); + final_memstate = stringf("%s#%d#final", get_id(module), arrayid); + } - if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) { - log_assert(cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero()); - async_read = true; - initial_memstate = stringf("%s#%d#0", get_id(module), arrayid); - final_memstate = stringf("%s#%d#final", get_id(module), arrayid); + if (statebv) + { + if (has_async_wr) { + makebits(final_memstate, mem->width*mem->size, get_id(mem->memid)); } - if (statebv) + for (int i = 0; i < GetSize(mem->wr_ports); i++) { - int mem_size = cell->getParam(ID::SIZE).as_int(); - int mem_offset = cell->getParam(ID::OFFSET).as_int(); - - if (async_read) { - makebits(final_memstate, width*mem_size, get_id(cell)); + auto &port = mem->wr_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); + + std::string addr = get_bv(addr_sig); + std::string data = get_bv(port.data); + std::string mask = get_bv(port.en); + + decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); + addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid)); + + decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data))); + data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid)); + + decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en))); + mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid)); + + std::string data_expr; + + for (int k = mem->size-1; k >= 0; k--) { + std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))", + data.c_str(), mask.c_str(), mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i, mask.c_str()); + data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))", + addr.c_str(), Const(k+mem->start_offset, abits).as_string().c_str(), new_data.c_str(), + mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i); } - for (int i = 0; i < wr_ports; i++) - { - SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); - SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); + decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n", + get_id(module), arrayid, i+1, get_id(module), mem->width*mem->size, data_expr.c_str(), get_id(mem->memid))); + } + } + else + { + if (has_async_wr) { + if (statedt) + dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", + initial_memstate.c_str(), abits, mem->width, get_id(mem->memid))); + else + decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", + initial_memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid))); + } - std::string addr = get_bv(addr_sig); - std::string data = get_bv(data_sig); - std::string mask = get_bv(mask_sig); + for (int i = 0; i < GetSize(mem->wr_ports); i++) + { + auto &port = mem->wr_ports[i]; + SigSpec addr_sig = port.addr; + addr_sig.extend_u0(abits); - decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); - addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell)); + std::string addr = get_bv(addr_sig); + std::string data = get_bv(port.data); + std::string mask = get_bv(port.en); - decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig))); - data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell)); + decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); + addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid)); - decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig))); - mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell)); + decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data))); + data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid)); - std::string data_expr; + decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", + get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en))); + mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid)); - for (int k = mem_size-1; k >= 0; k--) { - std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))", - data.c_str(), mask.c_str(), width*(k+1)-1, width*k, get_id(module), arrayid, i, mask.c_str()); - data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))", - addr.c_str(), Const(k+mem_offset, abits).as_string().c_str(), new_data.c_str(), - width*(k+1)-1, width*k, get_id(module), arrayid, i); - } + data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))", + data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str()); - decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n", - get_id(module), arrayid, i+1, get_id(module), width*mem_size, data_expr.c_str(), get_id(cell))); - } + decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) " + "(store (|%s#%d#%d| state) %s %s)) ; %s\n", + get_id(module), arrayid, i+1, get_id(module), abits, mem->width, + get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid))); } - else - { - if (async_read) { - if (statedt) - dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - initial_memstate.c_str(), abits, width, get_id(cell))); - else - decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", - initial_memstate.c_str(), get_id(module), abits, width, get_id(cell))); - } - - for (int i = 0; i < wr_ports; i++) - { - SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); - SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); - SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); + } - std::string addr = get_bv(addr_sig); - std::string data = get_bv(data_sig); - std::string mask = get_bv(mask_sig); + std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, GetSize(mem->wr_ports)); + std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid); + trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(mem->memid))); + ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid)); - decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig))); - addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell)); + if (has_async_wr) + hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(mem->memid))); - decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig))); - data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell)); + Const init_data = mem->get_init_data(); - decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n", - get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig))); - mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell)); + for (int i = 0; i < mem->size; i++) + { + if (i*mem->width >= GetSize(init_data)) + break; - data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))", - data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str()); + Const initword = init_data.extract(i*mem->width, mem->width, State::Sx); + Const initmask = initword; + bool gen_init_constr = false; - decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) " - "(store (|%s#%d#%d| state) %s %s)) ; %s\n", - get_id(module), arrayid, i+1, get_id(module), abits, width, - get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell))); + 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; } } - std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports); - std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid); - trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell))); - ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid)); - - if (async_read) - hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell))); - - Const init_data = cell->getParam(ID::INIT); - int memsize = cell->getParam(ID::SIZE).as_int(); - - for (int i = 0; i < memsize; i++) + if (gen_init_constr) { - if (i*width >= GetSize(init_data)) - break; - - Const initword = init_data.extract(i*width, width, State::Sx); - Const initmask = initword; - bool gen_init_constr = false; - - 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("(= (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(), - initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i)); - } + if (statebv) + /* FIXME */; + else + 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(), + initmask.as_string().c_str(), initword.as_string().c_str(), get_id(mem->memid), i)); } } } @@ -1387,8 +1456,12 @@ struct Smt2Backend : public Backend { log(" use the given template file. the line containing only the token '%%%%'\n"); log(" is replaced with the regular output of this command.\n"); log("\n"); + log(" -solver-option