From b00abe4a26ca24d22c822e5400e2f3aede93df48 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Wed, 10 Apr 2024 11:45:12 +0200 Subject: [PATCH 001/499] Extend `log` command with `-push`, `-pop`, `-header` options --- passes/cmds/logcmd.cc | 38 +++++++++++++++++++++++++++++++++----- 1 file changed, 33 insertions(+), 5 deletions(-) diff --git a/passes/cmds/logcmd.cc b/passes/cmds/logcmd.cc index 20cbd894345..8e51af4b3b7 100644 --- a/passes/cmds/logcmd.cc +++ b/passes/cmds/logcmd.cc @@ -31,7 +31,8 @@ struct LogPass : public Pass { { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| log("\n"); - log(" log string\n"); + log(" log [options] string\n"); + log(" log [ -push | -pop ]\n"); log("\n"); log("Print the given string to the screen and/or the log file. This is useful for TCL\n"); log("scripts, because the TCL command \"puts\" only goes to stdout but not to\n"); @@ -52,14 +53,26 @@ struct LogPass : public Pass { log(" -n\n"); log(" do not append a newline\n"); log("\n"); + log(" -header\n"); + log(" log a pass header\n"); + log("\n"); + log(" -push\n"); + log(" push a new level on the pass counter\n"); + log("\n"); + log(" -push\n"); + log(" pop from the pass counter\n"); + log("\n"); } - void execute(std::vector args, RTLIL::Design*) override + void execute(std::vector args, RTLIL::Design* design) override { size_t argidx; bool to_stdout = false; bool to_stderr = false; bool to_log = true; bool newline = true; + bool header = false; + bool push = false; + bool pop = false; std::string text; for (argidx = 1; argidx < args.size(); argidx++) @@ -68,15 +81,30 @@ struct LogPass : public Pass { else if (args[argidx] == "-stderr") to_stderr = true; else if (args[argidx] == "-nolog") to_log = false; else if (args[argidx] == "-n") newline = false; + else if (args[argidx] == "-header") header = true; + else if (args[argidx] == "-push") push = true; + else if (args[argidx] == "-pop") pop = true; else break; } + + if ((push || pop) && args.size() != 2) + log_cmd_error("Bad usage: 'log -push' or 'log -pop' must be used without other arguments.\n"); + + if (push) { log_push(); return; } + if (pop) { log_pop(); return; } + for (; argidx < args.size(); argidx++) text += args[argidx] + ' '; if (!text.empty()) text.resize(text.size()-1); - if (to_stdout) fprintf(stdout, (newline ? "%s\n" : "%s"), text.c_str()); - if (to_stderr) fprintf(stderr, (newline ? "%s\n" : "%s"), text.c_str()); - if (to_log) log ( (newline ? "%s\n" : "%s"), text.c_str()); + const char *fmtline = newline ? "%s\n" : "%s"; + + if (to_stdout) fprintf(stdout, fmtline, text.c_str()); + if (to_stderr) fprintf(stderr, fmtline, text.c_str()); + if (to_log) { + if (!header) log(fmtline, text.c_str()); + else log_header(design, fmtline, text.c_str()); + } } } LogPass; From f2ebc3f7b14e1847798fecdf1c12cd3311cb214e Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Thu, 25 Apr 2024 09:39:23 +1200 Subject: [PATCH 002/499] github: Add template for documentation issues --- .github/ISSUE_TEMPLATE/docs_report.yml | 55 ++++++++++++++++++++++++++ 1 file changed, 55 insertions(+) create mode 100644 .github/ISSUE_TEMPLATE/docs_report.yml diff --git a/.github/ISSUE_TEMPLATE/docs_report.yml b/.github/ISSUE_TEMPLATE/docs_report.yml new file mode 100644 index 00000000000..aa65c63b9c9 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/docs_report.yml @@ -0,0 +1,55 @@ +name: Documentation Report +description: Report a problem with the Yosys documentation +labels: ["pending-verification"] +body: + - type: markdown + attributes: + value: > + + If you have a general question, please ask it in the [Discussions](https://github.com/YosysHQ/yosys/discussions) area + or join our [IRC Channel](https://web.libera.chat/#yosys) or [Community Slack](https://join.slack.com/t/yosyshq/shared_invite/zt-1aopkns2q-EiQ97BeQDt_pwvE41sGSuA). + + + If you have found a bug in Yosys, or in building the documentation, + please fill out the Bug Report issue form, this form is for problems + with the live documentation on [Read the + Docs](https://yosyshq.readthedocs.io/projects/yosys/). Please only + report problems that appear on the latest version of the documentation. + + + Please contact [YosysHQ GmbH](https://www.yosyshq.com/) if you need + commercial support for Yosys. + + - type: input + id: docs_url + attributes: + label: Link to page + description: "Please provide a link to the page where the problem was found." + placeholder: "e.g. https://yosyshq.readthedocs.io/projects/yosys/" + validations: + required: true + + - type: input + id: build_number + attributes: + label: Build number + description: "If possible, please provide the latest build number from https://readthedocs.org/projects/yosys/builds/." + placeholder: "e.g. Build #24078236" + validations: + required: false + + - type: textarea + id: problem + attributes: + label: Issue + description: "Please describe what is incorrect, invalid, or missing." + validations: + required: true + + - type: textarea + id: expected + attributes: + label: Expected + description: "If applicable, please describe what should appear instead." + validations: + required: false From 374cd3966d65cf8dda4cdfd2563462211ab3216f Mon Sep 17 00:00:00 2001 From: Jason Wu Date: Mon, 29 Apr 2024 10:04:34 +0800 Subject: [PATCH 003/499] export define marco to qtcreator.config --- Makefile | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 22fe373a68a..d77cacd54c6 100644 --- a/Makefile +++ b/Makefile @@ -92,7 +92,7 @@ YOSYS_SRC := $(dir $(firstword $(MAKEFILE_LIST))) VPATH := $(YOSYS_SRC) CXXSTD ?= c++11 -CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -MP -D_YOSYS_ -fPIC -I$(PREFIX)/include +CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -MP -D_YOSYS_ -fPIC -I$(PREFIX)/include LIBS := $(LIBS) -lstdc++ -lm PLUGIN_LINKFLAGS := PLUGIN_LIBS := @@ -1045,11 +1045,12 @@ coverage: genhtml coverage.info --output-directory coverage_html qtcreator: + echo "$(CXXFLAGS)" | grep -o '\-D[^ ]*' | tr ' ' '\n' | sed 's/-D/#define /' | sed 's/=/ /'> qtcreator.config { for file in $(basename $(OBJS)); do \ for prefix in cc y l; do if [ -f $${file}.$${prefix} ]; then echo $$file.$${prefix}; fi; done \ done; find backends frontends kernel libs passes -type f \( -name '*.h' -o -name '*.hh' \); } > qtcreator.files { echo .; find backends frontends kernel libs passes -type f \( -name '*.h' -o -name '*.hh' \) -printf '%h\n' | sort -u; } > qtcreator.includes - touch qtcreator.config qtcreator.creator + touch qtcreator.creator vcxsrc: $(GENFILES) $(EXTRA_TARGETS) rm -rf yosys-win32-vcxsrc-$(YOSYS_VER){,.zip} From f1672b2f14cbf4aac89bd2e922bbd6919f808c6d Mon Sep 17 00:00:00 2001 From: Jason Wu <41063703+offline3@users.noreply.github.com> Date: Mon, 29 Apr 2024 10:16:22 +0800 Subject: [PATCH 004/499] Update Makefile --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index d77cacd54c6..296d66d0dad 100644 --- a/Makefile +++ b/Makefile @@ -92,7 +92,7 @@ YOSYS_SRC := $(dir $(firstword $(MAKEFILE_LIST))) VPATH := $(YOSYS_SRC) CXXSTD ?= c++11 -CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -MP -D_YOSYS_ -fPIC -I$(PREFIX)/include +CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -MP -D_YOSYS_ -fPIC -I$(PREFIX)/include LIBS := $(LIBS) -lstdc++ -lm PLUGIN_LINKFLAGS := PLUGIN_LIBS := From 8cc9aa7fc6a4d9008e68a4e146358a191cb854c4 Mon Sep 17 00:00:00 2001 From: Lofty Date: Fri, 3 May 2024 11:16:34 +0100 Subject: [PATCH 005/499] intel_alm: drop quartus support --- techlibs/intel_alm/Makefile.inc | 3 - techlibs/intel_alm/common/alm_sim.v | 414 +-------------------- techlibs/intel_alm/common/bram_m20k.txt | 33 -- techlibs/intel_alm/common/bram_m20k_map.v | 31 -- techlibs/intel_alm/common/dff_sim.v | 32 -- techlibs/intel_alm/common/mem_sim.v | 56 +-- techlibs/intel_alm/common/quartus_rename.v | 311 ---------------- techlibs/intel_alm/synth_intel_alm.cc | 81 +--- tests/arch/intel_alm/add_sub.ys | 9 - tests/arch/intel_alm/adffs.ys | 46 --- tests/arch/intel_alm/blockram.ys | 1 + tests/arch/intel_alm/counter.ys | 14 - tests/arch/intel_alm/dffs.ys | 22 -- tests/arch/intel_alm/fsm.ys | 22 -- tests/arch/intel_alm/logic.ys | 13 - tests/arch/intel_alm/lutram.ys | 1 + tests/arch/intel_alm/mul.ys | 25 -- tests/arch/intel_alm/mux.ys | 43 --- tests/arch/intel_alm/quartus_ice.ys | 26 -- tests/arch/intel_alm/shifter.ys | 11 - tests/arch/intel_alm/tribuf.ys | 14 - 21 files changed, 18 insertions(+), 1190 deletions(-) delete mode 100644 techlibs/intel_alm/common/bram_m20k.txt delete mode 100644 techlibs/intel_alm/common/bram_m20k_map.v delete mode 100644 techlibs/intel_alm/common/quartus_rename.v delete mode 100644 tests/arch/intel_alm/quartus_ice.ys diff --git a/techlibs/intel_alm/Makefile.inc b/techlibs/intel_alm/Makefile.inc index b5f279a921c..9e24d695e85 100644 --- a/techlibs/intel_alm/Makefile.inc +++ b/techlibs/intel_alm/Makefile.inc @@ -20,10 +20,7 @@ $(eval $(call add_share_file,share/intel_alm/cyclonev,techlibs/intel_alm/cyclone # RAM $(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/bram_m10k.txt)) $(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/bram_m10k_map.v)) -$(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/bram_m20k.txt)) -$(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/bram_m20k_map.v)) $(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/lutram_mlab.txt)) # Miscellaneous $(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/megafunction_bb.v)) -$(eval $(call add_share_file,share/intel_alm/common,techlibs/intel_alm/common/quartus_rename.v)) diff --git a/techlibs/intel_alm/common/alm_sim.v b/techlibs/intel_alm/common/alm_sim.v index d3bd673903f..858e43c76cc 100644 --- a/techlibs/intel_alm/common/alm_sim.v +++ b/techlibs/intel_alm/common/alm_sim.v @@ -1,4 +1,4 @@ -// The core logic primitive of the Cyclone V/10GX is the Adaptive Logic Module +// The core logic primitive of the Cyclone V is the Adaptive Logic Module // (ALM). Each ALM is made up of an 8-input, 2-output look-up table, covered // in this file, connected to combinational outputs, a carry chain, and four // D flip-flops (which are covered as MISTRAL_FF in dff_sim.v). @@ -77,14 +77,6 @@ // SUMOUT 368 1342 1323 887 927 - 785 - // CARRYOUT 71 1082 1062 866 813 - 1198 - -// Arria V LUT output timings (picoseconds): -// -// CARRY A B C D E F G -// COMBOUT - 387 375 316 317 - 76 319 (LUT6) -// COMBOUT - 387 375 316 317 218 76 319 (LUT7) -// SUMOUT 249 744 732 562 576 - 511 - -// CARRYOUT 19 629 623 530 514 - 696 - - (* abc9_lut=2, lib_whitebox *) module MISTRAL_ALUT6(input A, B, C, D, E, F, output Q); @@ -100,26 +92,6 @@ specify (F => Q) = 97; endspecify `endif -`ifdef arriav -specify - (A => Q) = 387; - (B => Q) = 375; - (C => Q) = 316; - (D => Q) = 317; - (E => Q) = 319; - (F => Q) = 76; -endspecify -`endif -`ifdef cyclone10gx -specify - (A => Q) = 275; - (B => Q) = 272; - (C => Q) = 175; - (D => Q) = 165; - (E => Q) = 162; - (F => Q) = 53; -endspecify -`endif assign Q = LUT >> {F, E, D, C, B, A}; @@ -140,24 +112,6 @@ specify (E => Q) = 97; endspecify `endif -`ifdef arriav -specify - (A => Q) = 375; - (B => Q) = 316; - (C => Q) = 317; - (D => Q) = 319; - (E => Q) = 76; -endspecify -`endif -`ifdef cyclone10gx -specify - (A => Q) = 272; - (B => Q) = 175; - (C => Q) = 165; - (D => Q) = 162; - (E => Q) = 53; -endspecify -`endif assign Q = LUT >> {E, D, C, B, A}; @@ -177,22 +131,6 @@ specify (D => Q) = 97; endspecify `endif -`ifdef arriav -specify - (A => Q) = 316; - (B => Q) = 317; - (C => Q) = 319; - (D => Q) = 76; -endspecify -`endif -`ifdef cyclone10gx -specify - (A => Q) = 175; - (B => Q) = 165; - (C => Q) = 162; - (D => Q) = 53; -endspecify -`endif assign Q = LUT >> {D, C, B, A}; @@ -211,20 +149,6 @@ specify (C => Q) = 97; endspecify `endif -`ifdef arriav -specify - (A => Q) = 316; - (B => Q) = 317; - (C => Q) = 76; -endspecify -`endif -`ifdef cyclone10gx -specify - (A => Q) = 165; - (B => Q) = 162; - (C => Q) = 53; -endspecify -`endif assign Q = LUT >> {C, B, A}; @@ -242,18 +166,6 @@ specify (B => Q) = 97; endspecify `endif -`ifdef arriav -specify - (A => Q) = 316; - (B => Q) = 76; -endspecify -`endif -`ifdef cyclone10gx -specify - (A => Q) = 162; - (B => Q) = 53; -endspecify -`endif assign Q = LUT >> {B, A}; @@ -268,16 +180,6 @@ specify (A => Q) = 97; endspecify `endif -`ifdef arriav -specify - (A => Q) = 76; -endspecify -`endif -`ifdef cyclone10gx -specify - (A => Q) = 53; -endspecify -`endif assign Q = ~A; @@ -306,40 +208,6 @@ specify (CI => CO) = 36; // Divided by 2 to account for there being two ALUT_ARITHs in an ALM) endspecify `endif -`ifdef arriav -specify - (A => SO) = 744; - (B => SO) = 732; - (C => SO) = 562; - (D0 => SO) = 576; - (D1 => SO) = 511; - (CI => SO) = 249; - - (A => CO) = 629; - (B => CO) = 623; - (C => CO) = 530; - (D0 => CO) = 514; - (D1 => CO) = 696; - (CI => CO) = 10; // Divided by 2 to account for there being two ALUT_ARITHs in an ALM) -endspecify -`endif -`ifdef cyclone10gx -specify - (A => SO) = 644; - (B => SO) = 477; - (C => SO) = 416; - (D0 => SO) = 380; - (D1 => SO) = 431; - (CI => SO) = 276; - - (A => CO) = 525; - (B => CO) = 433; - (C => CO) = 712; - (D0 => CO) = 653; - (D1 => CO) = 593; - (CI => CO) = 16; -endspecify -`endif wire q0, q1; @@ -349,283 +217,3 @@ assign q1 = LUT1 >> {D1, C, B, A}; assign {CO, SO} = q0 + !q1 + CI; endmodule - - -/* -// A, B, C0, C1, E0, E1, F0, F1: data inputs -// CARRYIN: carry input -// SHAREIN: shared-arithmetic input -// CLK0, CLK1, CLK2: clock inputs -// -// COMB0, COMB1: combinational outputs -// FF0, FF1, FF2, FF3: DFF outputs -// SUM0, SUM1: adder outputs -// CARRYOUT: carry output -// SHAREOUT: shared-arithmetic output -module MISTRAL_ALM( - input A, B, C0, C1, E0, E1, F0, F1, CARRYIN, SHAREIN, // LUT path - input CLK0, CLK1, CLK2, AC0, AC1, // FF path - output COMB0, COMB1, SUM0, SUM1, CARRYOUT, SHAREOUT, - output FF0, FF1, FF2, FF3 -); - -parameter LUT0 = 16'b0000; -parameter LUT1 = 16'b0000; -parameter LUT2 = 16'b0000; -parameter LUT3 = 16'b0000; - -parameter INIT0 = 1'b0; -parameter INIT1 = 1'b0; -parameter INIT2 = 1'b0; -parameter INIT3 = 1'b0; - -parameter C0_MUX = "C0"; -parameter C1_MUX = "C1"; - -parameter F0_MUX = "VCC"; -parameter F1_MUX = "GND"; - -parameter FEEDBACK0 = "FF0"; -parameter FEEDBACK1 = "FF2"; - -parameter ADD_MUX = "LUT"; - -parameter DFF01_DATA_MUX = "COMB"; -parameter DFF23_DATA_MUX = "COMB"; - -parameter DFF0_CLK = "CLK0"; -parameter DFF1_CLK = "CLK0"; -parameter DFF2_CLK = "CLK0"; -parameter DFF3_CLK = "CLK0"; - -parameter DFF0_AC = "AC0"; -parameter DFF1_AC = "AC0"; -parameter DFF2_AC = "AC0"; -parameter DFF3_AC = "AC0"; - -// Feedback muxes from the flip-flop outputs. -wire ff_feedback_mux0, ff_feedback_mux1; - -// C-input muxes which can be set to also use the F-input. -wire c0_input_mux, c1_input_mux; - -// F-input muxes which can be set to a constant to allow LUT5 use. -wire f0_input_mux, f1_input_mux; - -// Adder input muxes to select between shared-arithmetic mode and arithmetic mode. -wire add0_input_mux, add1_input_mux; - -// Combinational-output muxes for LUT #1 and LUT #3 -wire lut1_comb_mux, lut3_comb_mux; - -// Sum-output muxes for LUT #1 and LUT #3 -wire lut1_sum_mux, lut3_sum_mux; - -// DFF data-input muxes -wire dff01_data_mux, dff23_data_mux; - -// DFF clock selectors -wire dff0_clk, dff1_clk, dff2_clk, dff3_clk; - -// DFF asynchronous-clear selectors -wire dff0_ac, dff1_ac, dff2_ac, dff3_ac; - -// LUT, DFF and adder output wires for routing. -wire lut0_out, lut1a_out, lut1b_out, lut2_out, lut3a_out, lut3b_out; -wire dff0_out, dff1_out, dff2_out, dff3_out; -wire add0_sum, add1_sum, add0_carry, add1_carry; - -generate - if (FEEDBACK0 === "FF0") - assign ff_feedback_mux0 = dff0_out; - else if (FEEDBACK0 === "FF1") - assign ff_feedback_mux0 = dff1_out; - else - $error("Invalid FEEDBACK0 setting!"); - - if (FEEDBACK1 == "FF2") - assign ff_feedback_mux1 = dff2_out; - else if (FEEDBACK1 == "FF3") - assign ff_feedback_mux1 = dff3_out; - else - $error("Invalid FEEDBACK1 setting!"); - - if (C0_MUX === "C0") - assign c0_input_mux = C0; - else if (C0_MUX === "F1") - assign c0_input_mux = F1; - else if (C0_MUX === "FEEDBACK1") - assign c0_input_mux = ff_feedback_mux1; - else - $error("Invalid C0_MUX setting!"); - - if (C1_MUX === "C1") - assign c1_input_mux = C1; - else if (C1_MUX === "F0") - assign c1_input_mux = F0; - else if (C1_MUX === "FEEDBACK0") - assign c1_input_mux = ff_feedback_mux0; - else - $error("Invalid C1_MUX setting!"); - - // F0 == VCC is LUT5 - // F0 == F0 is LUT6 - // F0 == FEEDBACK is unknown - if (F0_MUX === "VCC") - assign f0_input_mux = 1'b1; - else if (F0_MUX === "F0") - assign f0_input_mux = F0; - else if (F0_MUX === "FEEDBACK0") - assign f0_input_mux = ff_feedback_mux0; - else - $error("Invalid F0_MUX setting!"); - - // F1 == GND is LUT5 - // F1 == F1 is LUT6 - // F1 == FEEDBACK is unknown - if (F1_MUX === "GND") - assign f1_input_mux = 1'b0; - else if (F1_MUX === "F1") - assign f1_input_mux = F1; - else if (F1_MUX === "FEEDBACK1") - assign f1_input_mux = ff_feedback_mux1; - else - $error("Invalid F1_MUX setting!"); - - if (ADD_MUX === "LUT") begin - assign add0_input_mux = ~lut1_sum_mux; - assign add1_input_mux = ~lut3_sum_mux; - end else if (ADD_MUX === "SHARE") begin - assign add0_input_mux = SHAREIN; - assign add1_input_mux = lut1_comb_mux; - end else - $error("Invalid ADD_MUX setting!"); - - if (DFF01_DATA_MUX === "COMB") - assign dff01_data_mux = COMB0; - else if (DFF01_DATA_MUX === "SUM") - assign dff01_data_mux = SUM0; - else - $error("Invalid DFF01_DATA_MUX setting!"); - - if (DFF23_DATA_MUX === "COMB") - assign dff23_data_mux = COMB0; - else if (DFF23_DATA_MUX === "SUM") - assign dff23_data_mux = SUM0; - else - $error("Invalid DFF23_DATA_MUX setting!"); - - if (DFF0_CLK === "CLK0") - assign dff0_clk = CLK0; - else if (DFF0_CLK === "CLK1") - assign dff0_clk = CLK1; - else if (DFF0_CLK === "CLK2") - assign dff0_clk = CLK2; - else - $error("Invalid DFF0_CLK setting!"); - - if (DFF1_CLK === "CLK0") - assign dff1_clk = CLK0; - else if (DFF1_CLK === "CLK1") - assign dff1_clk = CLK1; - else if (DFF1_CLK === "CLK2") - assign dff1_clk = CLK2; - else - $error("Invalid DFF1_CLK setting!"); - - if (DFF2_CLK === "CLK0") - assign dff2_clk = CLK0; - else if (DFF2_CLK === "CLK1") - assign dff2_clk = CLK1; - else if (DFF2_CLK === "CLK2") - assign dff2_clk = CLK2; - else - $error("Invalid DFF2_CLK setting!"); - - if (DFF3_CLK === "CLK0") - assign dff3_clk = CLK0; - else if (DFF3_CLK === "CLK1") - assign dff3_clk = CLK1; - else if (DFF3_CLK === "CLK2") - assign dff3_clk = CLK2; - else - $error("Invalid DFF3_CLK setting!"); - - if (DFF0_AC === "AC0") - assign dff0_ac = AC0; - else if (DFF0_AC === "AC1") - assign dff0_ac = AC1; - else - $error("Invalid DFF0_AC setting!"); - - if (DFF1_AC === "AC0") - assign dff1_ac = AC0; - else if (DFF1_AC === "AC1") - assign dff1_ac = AC1; - else - $error("Invalid DFF1_AC setting!"); - - if (DFF2_AC === "AC0") - assign dff2_ac = AC0; - else if (DFF2_AC === "AC1") - assign dff2_ac = AC1; - else - $error("Invalid DFF2_AC setting!"); - - if (DFF3_AC === "AC0") - assign dff3_ac = AC0; - else if (DFF3_AC === "AC1") - assign dff3_ac = AC1; - else - $error("Invalid DFF3_AC setting!"); - -endgenerate - -// F0 on the Quartus diagram -MISTRAL_ALUT4 #(.LUT(LUT0)) lut0 (.A(A), .B(B), .C(C0), .D(c1_input_mux), .Q(lut0_out)); - -// F2 on the Quartus diagram -MISTRAL_ALUT4 #(.LUT(LUT1)) lut1_comb (.A(A), .B(B), .C(C0), .D(c1_input_mux), .Q(lut1_comb_mux)); -MISTRAL_ALUT4 #(.LUT(LUT1)) lut1_sum (.A(A), .B(B), .C(C0), .D(E0), .Q(lut1_sum_mux)); - -// F1 on the Quartus diagram -MISTRAL_ALUT4 #(.LUT(LUT2)) lut2 (.A(A), .B(B), .C(C1), .D(c0_input_mux), .Q(lut2_out)); - -// F3 on the Quartus diagram -MISTRAL_ALUT4 #(.LUT(LUT3)) lut3_comb (.A(A), .B(B), .C(C1), .D(c0_input_mux), .Q(lut3_comb_mux)); -MISTRAL_ALUT4 #(.LUT(LUT3)) lut3_sum (.A(A), .B(B), .C(C1), .D(E1), .Q(lut3_sum_mux)); - -MISTRAL_FF #(.INIT(INIT0)) dff0 (.D(dff01_data_mux), .CLK(dff0_clk), .ACn(dff0_ac), .Q(dff0_out)); -MISTRAL_FF #(.INIT(INIT1)) dff1 (.D(dff01_data_mux), .CLK(dff1_clk), .ACn(dff1_ac), .Q(dff1_out)); -MISTRAL_FF #(.INIT(INIT2)) dff2 (.D(dff23_data_mux), .CLK(dff2_clk), .ACn(dff2_ac), .Q(dff2_out)); -MISTRAL_FF #(.INIT(INIT3)) dff3 (.D(dff23_data_mux), .CLK(dff3_clk), .ACn(dff3_ac), .Q(dff3_out)); - -// Adders -assign {add0_carry, add0_sum} = CARRYIN + lut0_out + lut1_sum_mux; -assign {add1_carry, add1_sum} = add0_carry + lut2_out + lut3_sum_mux; - -// COMBOUT outputs on the Quartus diagram -assign COMB0 = E0 ? (f0_input_mux ? lut3_comb_mux : lut1_comb_mux) - : (f0_input_mux ? lut2_out : lut0_out); - -assign COMB1 = E1 ? (f1_input_mux ? lut3_comb_mux : lut1_comb_mux) - : (f1_input_mux ? lut2_out : lut0_out); - -// SUMOUT output on the Quartus diagram -assign SUM0 = add0_sum; -assign SUM1 = add1_sum; - -// COUT output on the Quartus diagram -assign CARRYOUT = add1_carry; - -// SHAREOUT output on the Quartus diagram -assign SHAREOUT = lut3_comb_mux; - -// REGOUT outputs on the Quartus diagram -assign FF0 = dff0_out; -assign FF1 = dff1_out; -assign FF2 = dff2_out; -assign FF3 = dff3_out; - -endmodule -*/ diff --git a/techlibs/intel_alm/common/bram_m20k.txt b/techlibs/intel_alm/common/bram_m20k.txt deleted file mode 100644 index b4c5a537287..00000000000 --- a/techlibs/intel_alm/common/bram_m20k.txt +++ /dev/null @@ -1,33 +0,0 @@ -bram __MISTRAL_M20K_SDP - init 1 # TODO: Re-enable when I figure out how BRAM init works - abits 14 @D16384x1 - dbits 1 @D16384x1 - abits 13 @D8192x2 - dbits 2 @D8192x2 - abits 12 @D4096x4 @D4096x5 - dbits 4 @D4096x4 - dbits 5 @D4096x5 - abits 11 @D2048x8 @D2048x10 - dbits 8 @D2048x8 - dbits 10 @D2048x10 - abits 10 @D1024x16 @D1024x20 - dbits 16 @D1024x16 - dbits 20 @D1024x20 - abits 9 @D512x32 @D512x40 - dbits 32 @D512x32 - dbits 40 @D512x40 - groups 2 - ports 1 1 - wrmode 1 0 - # read enable; write enable + byte enables (only for multiples of 8) - enable 1 1 - transp 0 0 - clocks 1 1 - clkpol 1 1 -endbram - - -match __MISTRAL_M20K_SDP - min efficiency 5 - make_transp -endmatch diff --git a/techlibs/intel_alm/common/bram_m20k_map.v b/techlibs/intel_alm/common/bram_m20k_map.v deleted file mode 100644 index 15739d66a2e..00000000000 --- a/techlibs/intel_alm/common/bram_m20k_map.v +++ /dev/null @@ -1,31 +0,0 @@ -module __MISTRAL_M20K_SDP(CLK1, A1ADDR, A1DATA, A1EN, B1ADDR, B1DATA, B1EN); - -parameter CFG_ABITS = 10; -parameter CFG_DBITS = 20; -parameter CFG_ENABLE_A = 1; -parameter CFG_ENABLE_B = 1; - -input CLK1; -input [CFG_ABITS-1:0] A1ADDR, B1ADDR; -input [CFG_DBITS-1:0] A1DATA; -output [CFG_DBITS-1:0] B1DATA; -input [CFG_ENABLE_A-1:0] A1EN, B1EN; - -altsyncram #( - .operation_mode("dual_port"), - .ram_block_type("m20k"), - .widthad_a(CFG_ABITS), - .width_a(CFG_DBITS), - .widthad_b(CFG_ABITS), - .width_b(CFG_DBITS), -) _TECHMAP_REPLACE_ ( - .address_a(A1ADDR), - .data_a(A1DATA), - .wren_a(A1EN), - .address_b(B1ADDR), - .q_b(B1DATA), - .clock0(CLK1), - .clock1(CLK1) -); - -endmodule diff --git a/techlibs/intel_alm/common/dff_sim.v b/techlibs/intel_alm/common/dff_sim.v index 8d58bf61485..a558973f9fd 100644 --- a/techlibs/intel_alm/common/dff_sim.v +++ b/techlibs/intel_alm/common/dff_sim.v @@ -77,38 +77,6 @@ specify if (ACLR === 1'b0) (ACLR => Q) = 282; endspecify `endif -`ifdef arriav -specify - if (ENA && ACLR !== 1'b0 && !SCLR && !SLOAD) (posedge CLK => (Q : DATAIN)) = 470; - if (ENA && SCLR) (posedge CLK => (Q : 1'b0)) = 633; - if (ENA && !SCLR && SLOAD) (posedge CLK => (Q : SDATA)) = 439; - - $setup(DATAIN, posedge CLK, /* -170 */ 0); - $setup(ENA, posedge CLK, /* -170 */ 0); - $setup(SCLR, posedge CLK, /* -170 */ 0); - $setup(SLOAD, posedge CLK, /* -170 */ 0); - $setup(SDATA, posedge CLK, /* -170 */ 0); - - if (ACLR === 1'b0) (ACLR => Q) = 215; -endspecify -`endif -`ifdef cyclone10gx -specify - // TODO (long-term): investigate these numbers. - // It seems relying on the Quartus Timing Analyzer was not the best idea; it's too fiddly. - if (ENA && ACLR !== 1'b0 && !SCLR && !SLOAD) (posedge CLK => (Q : DATAIN)) = 219; - if (ENA && SCLR) (posedge CLK => (Q : 1'b0)) = 219; - if (ENA && !SCLR && SLOAD) (posedge CLK => (Q : SDATA)) = 219; - - $setup(DATAIN, posedge CLK, 268); - $setup(ENA, posedge CLK, 268); - $setup(SCLR, posedge CLK, 268); - $setup(SLOAD, posedge CLK, 268); - $setup(SDATA, posedge CLK, 268); - - if (ACLR === 1'b0) (ACLR => Q) = 0; -endspecify -`endif initial begin // Altera flops initialise to zero. diff --git a/techlibs/intel_alm/common/mem_sim.v b/techlibs/intel_alm/common/mem_sim.v index 563f1d2413e..5ab1b73261f 100644 --- a/techlibs/intel_alm/common/mem_sim.v +++ b/techlibs/intel_alm/common/mem_sim.v @@ -1,7 +1,7 @@ // The MLAB // -------- // In addition to Logic Array Blocks (LABs) that contain ten Adaptive Logic -// Modules (ALMs, see alm_sim.v), the Cyclone V/10GX also contain +// Modules (ALMs, see alm_sim.v), the Cyclone V also contains // Memory/Logic Array Blocks (MLABs) that can act as either ten ALMs, or utilise // the memory the ALM uses to store the look-up table data for general usage, // producing a 32 address by 20-bit block of memory. MLABs are spread out @@ -14,11 +14,8 @@ // or shift registers (by using the output of the Nth bit as input for the N+1th // bit). // -// Oddly, instead of providing a block 32 address by 20-bit cell, Quartus asks -// synthesis tools to build MLABs out of 32 address by 1-bit cells, and tries -// to put these cells in the same MLAB during cell placement. Because of this -// a MISTRAL_MLAB cell represents one of these 32 address by 1-bit cells, and -// 20 of them represent a physical MLAB. +// For historical reasons a MISTRAL_MLAB cell represents a 32 address by 1-bit cell, +// and 20 of them represent a physical MLAB. // // How the MLAB works // ------------------ @@ -28,10 +25,7 @@ // by the Yosys `memory_bram` pass, and it doesn't make sense to me to use // `techmap` just for the sake of renaming the cell ports. // -// The MLAB can be initialised to any value, but unfortunately Quartus only -// allows memory initialisation from a file. Since Yosys doesn't preserve input -// file information, or write the contents of an `initial` block to a file, -// Yosys can't currently initialise the MLAB in a way Quartus will accept. +// The MLAB can be initialised to any value. // // The MLAB takes in data from A1DATA at the rising edge of CLK1, and if A1EN // is high, writes it to the address in A1ADDR. A1EN can therefore be used to @@ -39,9 +33,7 @@ // // Simultaneously, the MLAB reads data from B1ADDR, and outputs it to B1DATA, // asynchronous to CLK1 and ignoring A1EN. If a synchronous read is needed -// then the output can be fed to embedded flops. Presently, Yosys assumes -// Quartus will pack external flops into the MLAB, but this is an assumption -// that needs testing. +// then the output can be fed to embedded flops. // The vendor sim model outputs 'x for a very short period (a few // combinational delta cycles) after each write. This has been omitted from @@ -69,33 +61,6 @@ specify (B1ADDR[4] => B1DATA) = 96; endspecify `endif -`ifdef arriav -specify - $setup(A1ADDR, posedge CLK1, 62); - $setup(A1DATA, posedge CLK1, 62); - $setup(A1EN, posedge CLK1, 62); - - (B1ADDR[0] => B1DATA) = 370; - (B1ADDR[1] => B1DATA) = 292; - (B1ADDR[2] => B1DATA) = 218; - (B1ADDR[3] => B1DATA) = 74; - (B1ADDR[4] => B1DATA) = 177; -endspecify -`endif -`ifdef cyclone10gx -// TODO: Cyclone 10 GX timings; the below timings are for Cyclone V -specify - $setup(A1ADDR, posedge CLK1, 86); - $setup(A1DATA, posedge CLK1, 86); - $setup(A1EN, posedge CLK1, 86); - - (B1ADDR[0] => B1DATA) = 487; - (B1ADDR[1] => B1DATA) = 475; - (B1ADDR[2] => B1DATA) = 382; - (B1ADDR[3] => B1DATA) = 284; - (B1ADDR[4] => B1DATA) = 96; -endspecify -`endif always @(posedge CLK1) if (A1EN) mem[A1ADDR] <= A1DATA; @@ -134,17 +99,6 @@ specify if (B1EN) (posedge CLK1 => (B1DATA : A1DATA)) = 1004; endspecify `endif -`ifdef arriav -specify - $setup(A1ADDR, posedge CLK1, 97); - $setup(A1DATA, posedge CLK1, 74); - $setup(A1EN, posedge CLK1, 109); - $setup(B1ADDR, posedge CLK1, 97); - $setup(B1EN, posedge CLK1, 126); - - if (B1EN) (posedge CLK1 => (B1DATA : A1DATA)) = 787; -endspecify -`endif always @(posedge CLK1) begin if (!A1EN) diff --git a/techlibs/intel_alm/common/quartus_rename.v b/techlibs/intel_alm/common/quartus_rename.v deleted file mode 100644 index 217dc5de98b..00000000000 --- a/techlibs/intel_alm/common/quartus_rename.v +++ /dev/null @@ -1,311 +0,0 @@ -`ifdef cyclonev -`define LCELL cyclonev_lcell_comb -`define MAC cyclonev_mac -`define MLAB cyclonev_mlab_cell -`define RAM_BLOCK cyclonev_ram_block -`define IBUF cyclonev_io_ibuf -`define OBUF cyclonev_io_obuf -`define CLKENA cyclonev_clkena -`endif -`ifdef arriav -`define LCELL arriav_lcell_comb -`define MAC arriav_mac -`define MLAB arriav_mlab_cell -`define RAM_BLOCK arriav_ram_block -`define IBUF arriav_io_ibuf -`define OBUF arriav_io_obuf -`define CLKENA arriav_clkena -`endif -`ifdef cyclone10gx -`define LCELL cyclone10gx_lcell_comb -`define MAC cyclone10gx_mac -`define MLAB cyclone10gx_mlab_cell -`define RAM_BLOCK cyclone10gx_ram_block -`define IBUF cyclone10gx_io_ibuf -`define OBUF cyclone10gx_io_obuf -`define CLKENA cyclone10gx_clkena -`endif - -module __MISTRAL_VCC(output Q); - -MISTRAL_ALUT2 #(.LUT(4'b1111)) _TECHMAP_REPLACE_ (.A(1'b1), .B(1'b1), .Q(Q)); - -endmodule - - -module __MISTRAL_GND(output Q); - -MISTRAL_ALUT2 #(.LUT(4'b0000)) _TECHMAP_REPLACE_ (.A(1'b1), .B(1'b1), .Q(Q)); - -endmodule - - -module MISTRAL_FF(input DATAIN, CLK, ACLR, ENA, SCLR, SLOAD, SDATA, output reg Q); - -dffeas #(.power_up("low"), .is_wysiwyg("true")) _TECHMAP_REPLACE_ (.d(DATAIN), .clk(CLK), .clrn(ACLR), .ena(ENA), .sclr(SCLR), .sload(SLOAD), .asdata(SDATA), .q(Q)); - -endmodule - - -module MISTRAL_ALUT6(input A, B, C, D, E, F, output Q); -parameter [63:0] LUT = 64'h0000_0000_0000_0000; - -`LCELL #(.lut_mask(LUT)) _TECHMAP_REPLACE_ (.dataa(A), .datab(B), .datac(C), .datad(D), .datae(E), .dataf(F), .combout(Q)); - -endmodule - - -module MISTRAL_ALUT5(input A, B, C, D, E, output Q); -parameter [31:0] LUT = 32'h0000_0000; - -`LCELL #(.lut_mask({2{LUT}})) _TECHMAP_REPLACE_ (.dataa(A), .datab(B), .datac(C), .datad(D), .datae(E), .combout(Q)); - -endmodule - - -module MISTRAL_ALUT4(input A, B, C, D, output Q); -parameter [15:0] LUT = 16'h0000; - -`LCELL #(.lut_mask({4{LUT}})) _TECHMAP_REPLACE_ (.dataa(A), .datab(B), .datac(C), .datad(D), .combout(Q)); - -endmodule - - -module MISTRAL_ALUT3(input A, B, C, output Q); -parameter [7:0] LUT = 8'h00; - -`LCELL #(.lut_mask({8{LUT}})) _TECHMAP_REPLACE_ (.dataa(A), .datab(B), .datac(C), .combout(Q)); - -endmodule - - -module MISTRAL_ALUT2(input A, B, output Q); -parameter [3:0] LUT = 4'h0; - -`LCELL #(.lut_mask({16{LUT}})) _TECHMAP_REPLACE_ (.dataa(A), .datab(B), .combout(Q)); - -endmodule - - -module MISTRAL_NOT(input A, output Q); - -NOT _TECHMAP_REPLACE_ (.IN(A), .OUT(Q)); - -endmodule - - -module MISTRAL_ALUT_ARITH(input A, B, C, D0, D1, CI, output SO, CO); -parameter LUT0 = 16'h0000; -parameter LUT1 = 16'h0000; - -`LCELL #(.lut_mask({16'h0, LUT1, 16'h0, LUT0})) _TECHMAP_REPLACE_ (.dataa(A), .datab(B), .datac(C), .datad(D0), .dataf(D1), .cin(CI), .sumout(SO), .cout(CO)); - -endmodule - - -module MISTRAL_MLAB(input [4:0] A1ADDR, input A1DATA, A1EN, CLK1, input [4:0] B1ADDR, output B1DATA); - -parameter _TECHMAP_CELLNAME_ = ""; - -// Here we get to an unfortunate situation. The cell has a mem_init0 parameter, -// which takes in a hexadecimal string that could be used to initialise RAM. -// In the vendor simulation models, this appears to work fine, but Quartus, -// either intentionally or not, forgets about this parameter and initialises the -// RAM to zero. -// -// Because of this, RAM initialisation is presently disabled, but the source -// used to generate mem_init0 is kept (commented out) in case this gets fixed -// or an undocumented way to get Quartus to initialise from mem_init0 is found. - -`MLAB #( - .logical_ram_name(_TECHMAP_CELLNAME_), - .logical_ram_depth(32), - .logical_ram_width(1), - .mixed_port_feed_through_mode("Dont Care"), - .first_bit_number(0), - .first_address(0), - .last_address(31), - .address_width(5), - .data_width(1), - .byte_enable_mask_width(1), - .port_b_data_out_clock("NONE"), - // .mem_init0($sformatf("%08x", INIT)) -) _TECHMAP_REPLACE_ ( - .portaaddr(A1ADDR), - .portadatain(A1DATA), - .portbaddr(B1ADDR), - .portbdataout(B1DATA), - .ena0(A1EN), - .clk0(CLK1) -); - -endmodule - - -module MISTRAL_M10K(A1ADDR, A1DATA, A1EN, CLK1, B1ADDR, B1DATA, B1EN); - -parameter CFG_ABITS = 10; -parameter CFG_DBITS = 10; - -parameter _TECHMAP_CELLNAME_ = ""; - -input [CFG_ABITS-1:0] A1ADDR, B1ADDR; -input [CFG_DBITS-1:0] A1DATA; -input CLK1, A1EN, B1EN; -output [CFG_DBITS-1:0] B1DATA; - -// Much like the MLAB, the M10K has mem_init[01234] parameters which would let -// you initialise the RAM cell via hex literals. If they were implemented. - -// Since the MISTRAL_M10K block has an inverted write-enable (like the real hardware) -// but the Quartus primitive expects a normal write-enable, we add an inverter. -wire A1EN_N; -NOT wren_inv (.IN(A1EN), .OUT(A1EN_N)); - -`RAM_BLOCK #( - .operation_mode("dual_port"), - .logical_ram_name(_TECHMAP_CELLNAME_), - .port_a_address_width(CFG_ABITS), - .port_a_data_width(CFG_DBITS), - .port_a_logical_ram_depth(2**CFG_ABITS), - .port_a_logical_ram_width(CFG_DBITS), - .port_a_first_address(0), - .port_a_last_address(2**CFG_ABITS - 1), - .port_a_first_bit_number(0), - .port_b_address_width(CFG_ABITS), - .port_b_data_width(CFG_DBITS), - .port_b_logical_ram_depth(2**CFG_ABITS), - .port_b_logical_ram_width(CFG_DBITS), - .port_b_first_address(0), - .port_b_last_address(2**CFG_ABITS - 1), - .port_b_first_bit_number(0), - .port_b_address_clock("clock0"), - .port_b_read_enable_clock("clock0") -) ram_block ( - .portaaddr(A1ADDR), - .portadatain(A1DATA), - .portawe(A1EN_N), - .portbaddr(B1ADDR), - .portbdataout(B1DATA), - .portbre(B1EN), - .clk0(CLK1) -); - -endmodule - - -module MISTRAL_MUL27X27(input [26:0] A, B, output [53:0] Y); - -parameter A_SIGNED = 1; -parameter B_SIGNED = 1; - -`MAC #( - .ax_width(27), - .signed_max(A_SIGNED ? "true" : "false"), - .ay_scan_in_width(27), - .signed_may(B_SIGNED ? "true" : "false"), - .result_a_width(54), - .operation_mode("M27x27") -) _TECHMAP_REPLACE_ ( - .ax(A), - .ay(B), - .resulta(Y) -); - -endmodule - - -module MISTRAL_MUL18X18(input [17:0] A, B, output [35:0] Y); - -parameter A_SIGNED = 1; -parameter B_SIGNED = 1; - -`MAC #( - .ax_width(18), - .signed_max(A_SIGNED ? "true" : "false"), - .ay_scan_in_width(18), - .signed_may(B_SIGNED ? "true" : "false"), - .result_a_width(36), - .operation_mode("M18x18_FULL") -) _TECHMAP_REPLACE_ ( - .ax(A), - .ay(B), - .resulta(Y) -); - -endmodule - - -module MISTRAL_MUL9X9(input [8:0] A, B, output [17:0] Y); - -parameter A_SIGNED = 1; -parameter B_SIGNED = 1; - -`MAC #( - .ax_width(9), - .signed_max(A_SIGNED ? "true" : "false"), - .ay_scan_in_width(9), - .signed_may(B_SIGNED ? "true" : "false"), - .result_a_width(18), - .operation_mode("M9x9") -) _TECHMAP_REPLACE_ ( - .ax(A), - .ay(B), - .resulta(Y) -); - -endmodule - -module MISTRAL_IB(input PAD, output O); -`IBUF #( - .bus_hold("false"), - .differential_mode("false") -) _TECHMAP_REPLACE_ ( - .i(PAD), - .o(O) -); -endmodule - -module MISTRAL_OB(output PAD, input I, OE); -`OBUF #( - .bus_hold("false"), - .differential_mode("false") -) _TECHMAP_REPLACE_ ( - .i(I), - .o(PAD), - .oe(OE) -); -endmodule - -module MISTRAL_IO(output PAD, input I, OE, output O); -`IBUF #( - .bus_hold("false"), - .differential_mode("false") -) ibuf ( - .i(PAD), - .o(O) -); - -`OBUF #( - .bus_hold("false"), - .differential_mode("false") -) obuf ( - .i(I), - .o(PAD), - .oe(OE) -); -endmodule - -module MISTRAL_CLKBUF (input A, output Q); -`CLKENA #( - .clock_type("auto"), - .ena_register_mode("always enabled"), - .ena_register_power_up("high"), - .disable_mode("low"), - .test_syn("high") -) _TECHMAP_REPLACE_ ( - .inclk(A), - .ena(1'b1), - .outclk(Q) -); -endmodule diff --git a/techlibs/intel_alm/synth_intel_alm.cc b/techlibs/intel_alm/synth_intel_alm.cc index c33eb43bf35..cdae9586eb0 100644 --- a/techlibs/intel_alm/synth_intel_alm.cc +++ b/techlibs/intel_alm/synth_intel_alm.cc @@ -2,7 +2,7 @@ * yosys -- Yosys Open SYnthesis Suite * * Copyright (C) 2012 Claire Xenia Wolf - * Copyright (C) 2019 Dan Ravensloft + * Copyright (C) 2019 Hannah Ravensloft * * Permission to use, copy, modify, and/or distribute this software for any * purpose with or without fee is hereby granted, provided that the above @@ -43,21 +43,11 @@ struct SynthIntelALMPass : public ScriptPass { log(" -family \n"); log(" target one of:\n"); log(" \"cyclonev\" - Cyclone V (default)\n"); - log(" \"arriav\" - Arria V (non-GZ)\n"); - log(" \"cyclone10gx\" - Cyclone 10GX\n"); - log("\n"); - log(" -vqm \n"); - log(" write the design to the specified Verilog Quartus Mapping File. Writing\n"); - log(" of an output file is omitted if this parameter is not specified. Implies\n"); - log(" -quartus.\n"); log("\n"); log(" -noflatten\n"); log(" do not flatten design before synthesis; useful for per-module area\n"); log(" statistics\n"); log("\n"); - log(" -quartus\n"); - log(" output a netlist using Quartus cells instead of MISTRAL_* cells\n"); - log("\n"); log(" -dff\n"); log(" pass DFFs to ABC to perform sequential logic optimisations\n"); log(" (EXPERIMENTAL)\n"); @@ -87,17 +77,15 @@ struct SynthIntelALMPass : public ScriptPass { log("\n"); } - string top_opt, family_opt, bram_type, vout_file; - bool flatten, quartus, nolutram, nobram, dff, nodsp, noiopad, noclkbuf; + string top_opt, family_opt, bram_type; + bool flatten, nolutram, nobram, dff, nodsp, noiopad, noclkbuf; void clear_flags() override { top_opt = "-auto-top"; family_opt = "cyclonev"; bram_type = "m10k"; - vout_file = ""; flatten = true; - quartus = false; nolutram = false; nobram = false; dff = false; @@ -121,11 +109,6 @@ struct SynthIntelALMPass : public ScriptPass { top_opt = "-top " + args[++argidx]; continue; } - if (args[argidx] == "-vqm" && argidx + 1 < args.size()) { - quartus = true; - vout_file = args[++argidx]; - continue; - } if (args[argidx] == "-run" && argidx + 1 < args.size()) { size_t pos = args[argidx + 1].find(':'); if (pos == std::string::npos) @@ -134,10 +117,6 @@ struct SynthIntelALMPass : public ScriptPass { run_to = args[argidx].substr(pos + 1); continue; } - if (args[argidx] == "-quartus") { - quartus = true; - continue; - } if (args[argidx] == "-nolutram") { nolutram = true; continue; @@ -173,18 +152,6 @@ struct SynthIntelALMPass : public ScriptPass { if (!design->full_selection()) log_cmd_error("This command only operates on fully selected designs!\n"); - if (family_opt == "cyclonev" || family_opt == "arriav") { - bram_type = "m10k"; - } else if (family_opt == "cyclone10gx") { - bram_type = "m20k"; - } else if (family_opt == "arriva") { - // I have typoed "arriav" as "arriva" (a local bus company) - // so many times I thought it would be funny to have an easter egg. - log_cmd_error("synth_intel_alm cannot synthesize for bus companies. (did you mean '-family arriav'?)\n"); - } else { - log_cmd_error("Invalid family specified: '%s'\n", family_opt.c_str()); - } - log_header(design, "Executing SYNTH_INTEL_ALM pass.\n"); log_push(); @@ -237,22 +204,16 @@ struct SynthIntelALMPass : public ScriptPass { if (help_mode) { run("techmap -map +/mul2dsp.v [...]", "(unless -nodsp)"); } else if (!nodsp) { - // Cyclone V/Arria V supports 9x9 multiplication, Cyclone 10 GX does not. run("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=27 -D DSP_B_MAXWIDTH=27 -D DSP_A_MINWIDTH=19 -D DSP_B_MINWIDTH=4 -D DSP_NAME=__MUL27X27"); run("chtype -set $mul t:$__soft_mul"); run("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=27 -D DSP_B_MAXWIDTH=27 -D DSP_A_MINWIDTH=4 -D DSP_B_MINWIDTH=19 -D DSP_NAME=__MUL27X27"); run("chtype -set $mul t:$__soft_mul"); - if (family_opt == "cyclonev" || family_opt == "arriav") { - run("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=18 -D DSP_B_MAXWIDTH=18 -D DSP_A_MINWIDTH=10 -D DSP_B_MINWIDTH=4 -D DSP_NAME=__MUL18X18"); - run("chtype -set $mul t:$__soft_mul"); - run("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=18 -D DSP_B_MAXWIDTH=18 -D DSP_A_MINWIDTH=4 -D DSP_B_MINWIDTH=10 -D DSP_NAME=__MUL18X18"); - run("chtype -set $mul t:$__soft_mul"); - run("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=9 -D DSP_B_MAXWIDTH=9 -D DSP_A_MINWIDTH=4 -D DSP_B_MINWIDTH=4 -D DSP_NAME=__MUL9X9"); - run("chtype -set $mul t:$__soft_mul"); - } else if (family_opt == "cyclone10gx") { - run("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=18 -D DSP_B_MAXWIDTH=18 -D DSP_A_MINWIDTH=4 -D DSP_B_MINWIDTH=4 -D DSP_NAME=__MUL18X18"); - run("chtype -set $mul t:$__soft_mul"); - } + run("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=18 -D DSP_B_MAXWIDTH=18 -D DSP_A_MINWIDTH=10 -D DSP_B_MINWIDTH=4 -D DSP_NAME=__MUL18X18"); + run("chtype -set $mul t:$__soft_mul"); + run("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=18 -D DSP_B_MAXWIDTH=18 -D DSP_A_MINWIDTH=4 -D DSP_B_MINWIDTH=10 -D DSP_NAME=__MUL18X18"); + run("chtype -set $mul t:$__soft_mul"); + run("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=9 -D DSP_B_MAXWIDTH=9 -D DSP_A_MINWIDTH=4 -D DSP_B_MINWIDTH=4 -D DSP_NAME=__MUL9X9"); + run("chtype -set $mul t:$__soft_mul"); } run("alumacc"); if (!noiopad) @@ -269,7 +230,7 @@ struct SynthIntelALMPass : public ScriptPass { } if (!nolutram && check_label("map_lutram", "(skip if -nolutram)")) { - run("memory_bram -rules +/intel_alm/common/lutram_mlab.txt", "(for Cyclone V / Cyclone 10GX)"); + run("memory_bram -rules +/intel_alm/common/lutram_mlab.txt", "(for Cyclone V)"); } if (check_label("map_ffram")) { @@ -303,28 +264,6 @@ struct SynthIntelALMPass : public ScriptPass { run("check"); run("blackbox =A:whitebox"); } - - if (check_label("quartus")) { - if (quartus || help_mode) { - // Quartus ICEs if you have a wire which has `[]` in its name, - // which Yosys produces when building memories out of flops. - run("rename -hide w:*[* w:*]*"); - // VQM mode does not support 'x, so replace those with zero. - run("setundef -zero"); - // VQM mode does not support multi-bit constant assignments - // (e.g. 2'b00 is an error), so as a workaround use references - // to constant driver cells, which Quartus accepts. - run("hilomap -singleton -hicell __MISTRAL_VCC Q -locell __MISTRAL_GND Q"); - // Rename from Yosys-internal MISTRAL_* cells to Quartus cells. - run(stringf("techmap -D %s -map +/intel_alm/common/quartus_rename.v", family_opt.c_str())); - } - } - - if (check_label("vqm")) { - if (!vout_file.empty() || help_mode) { - run(stringf("write_verilog -attr2comment -defparam -nohex -decimal %s", help_mode ? "" : vout_file.c_str())); - } - } } } SynthIntelALMPass; diff --git a/tests/arch/intel_alm/add_sub.ys b/tests/arch/intel_alm/add_sub.ys index 8f87adf2713..6453da116a1 100644 --- a/tests/arch/intel_alm/add_sub.ys +++ b/tests/arch/intel_alm/add_sub.ys @@ -7,12 +7,3 @@ stat select -assert-count 9 t:MISTRAL_ALUT_ARITH select -assert-none t:MISTRAL_ALUT_ARITH %% t:* %D -design -reset -read_verilog ../common/add_sub.v -hierarchy -top top -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd top # Constrain all select calls below inside the top module -stat -select -assert-count 9 t:MISTRAL_ALUT_ARITH -select -assert-none t:MISTRAL_ALUT_ARITH %% t:* %D diff --git a/tests/arch/intel_alm/adffs.ys b/tests/arch/intel_alm/adffs.ys index d7487c40bec..1f81902ec5a 100644 --- a/tests/arch/intel_alm/adffs.ys +++ b/tests/arch/intel_alm/adffs.ys @@ -12,18 +12,6 @@ select -assert-count 1 t:MISTRAL_NOT select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D -design -load read -hierarchy -top adff -proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd adff # Constrain all select calls below inside the top module -select -assert-count 1 t:MISTRAL_FF -select -assert-count 1 t:MISTRAL_NOT - -select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D - - design -load read hierarchy -top adffn proc @@ -35,17 +23,6 @@ select -assert-count 1 t:MISTRAL_FF select -assert-none t:MISTRAL_FF %% t:* %D -design -load read -hierarchy -top adffn -proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd adffn # Constrain all select calls below inside the top module -select -assert-count 1 t:MISTRAL_FF - -select -assert-none t:MISTRAL_FF %% t:* %D - - design -load read hierarchy -top dffs proc @@ -58,18 +35,6 @@ select -assert-count 1 t:MISTRAL_ALUT2 select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 %% t:* %D -design -load read -hierarchy -top dffs -proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd dffs # Constrain all select calls below inside the top module -select -assert-count 1 t:MISTRAL_FF -select -assert-count 1 t:MISTRAL_ALUT2 - -select -assert-none t:MISTRAL_FF t:MISTRAL_ALUT2 %% t:* %D - - design -load read hierarchy -top ndffnr proc @@ -81,14 +46,3 @@ select -assert-count 2 t:MISTRAL_NOT select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D - -design -load read -hierarchy -top ndffnr -proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd ndffnr # Constrain all select calls below inside the top module -select -assert-count 1 t:MISTRAL_FF -select -assert-count 2 t:MISTRAL_NOT - -select -assert-none t:MISTRAL_FF t:MISTRAL_NOT %% t:* %D diff --git a/tests/arch/intel_alm/blockram.ys b/tests/arch/intel_alm/blockram.ys index 21b5ecbfb60..4af59e7d434 100644 --- a/tests/arch/intel_alm/blockram.ys +++ b/tests/arch/intel_alm/blockram.ys @@ -5,3 +5,4 @@ cd sync_ram_sdp select -assert-count 1 t:MISTRAL_NOT select -assert-count 1 t:MISTRAL_M10K select -assert-none t:MISTRAL_NOT t:MISTRAL_M10K %% t:* %D + diff --git a/tests/arch/intel_alm/counter.ys b/tests/arch/intel_alm/counter.ys index 2b428fb3e51..44e00081445 100644 --- a/tests/arch/intel_alm/counter.ys +++ b/tests/arch/intel_alm/counter.ys @@ -11,17 +11,3 @@ select -assert-count 8 t:MISTRAL_ALUT_ARITH select -assert-count 8 t:MISTRAL_FF select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D - -design -reset -read_verilog ../common/counter.v -hierarchy -top top -proc -flatten -equiv_opt -assert -async2sync -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd top # Constrain all select calls below inside the top module - -select -assert-count 2 t:MISTRAL_NOT -select -assert-count 8 t:MISTRAL_ALUT_ARITH -select -assert-count 8 t:MISTRAL_FF -select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT_ARITH t:MISTRAL_FF %% t:* %D diff --git a/tests/arch/intel_alm/dffs.ys b/tests/arch/intel_alm/dffs.ys index 34b99f04cbf..aeaae4aa3ce 100644 --- a/tests/arch/intel_alm/dffs.ys +++ b/tests/arch/intel_alm/dffs.ys @@ -7,17 +7,6 @@ equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd dff # Constrain all select calls below inside the top module select -assert-count 1 t:MISTRAL_FF - -select -assert-none t:MISTRAL_FF %% t:* %D - -design -load read -hierarchy -top dff -proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd dff # Constrain all select calls below inside the top module -select -assert-count 1 t:MISTRAL_FF - select -assert-none t:MISTRAL_FF %% t:* %D @@ -28,16 +17,5 @@ equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) cd dffe # Constrain all select calls below inside the top module select -assert-count 1 t:MISTRAL_FF - select -assert-none t:MISTRAL_FF %% t:* %D - -design -load read -hierarchy -top dffe -proc -equiv_opt -async2sync -assert -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd dffe # Constrain all select calls below inside the top module -select -assert-count 1 t:MISTRAL_FF - -select -assert-none t:MISTRAL_FF %% t:* %D diff --git a/tests/arch/intel_alm/fsm.ys b/tests/arch/intel_alm/fsm.ys index 0aeea450ac5..f3060684a9f 100644 --- a/tests/arch/intel_alm/fsm.ys +++ b/tests/arch/intel_alm/fsm.ys @@ -20,25 +20,3 @@ select -assert-max 6 t:MISTRAL_ALUT5 # Clang returns 5, GCC returns 4 select -assert-max 2 t:MISTRAL_ALUT6 # Clang returns 1, GCC returns 2 select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D -design -reset -read_verilog ../common/fsm.v -hierarchy -top fsm -proc -flatten - -equiv_opt -run :prove -map +/intel_alm/common/alm_sim.v -map +/intel_alm/common/dff_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf -async2sync -miter -equiv -make_assert -flatten gold gate miter -sat -verify -prove-asserts -show-public -set-at 1 in_reset 1 -seq 20 -prove-skip 1 miter - -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd fsm # Constrain all select calls below inside the top module - -select -assert-count 6 t:MISTRAL_FF -select -assert-max 1 t:MISTRAL_NOT -select -assert-max 2 t:MISTRAL_ALUT2 # Clang returns 2, GCC returns 1 -select -assert-max 2 t:MISTRAL_ALUT3 # Clang returns 2, GCC returns 1 -select -assert-max 2 t:MISTRAL_ALUT4 # Clang returns 0, GCC returns 1 -select -assert-max 6 t:MISTRAL_ALUT5 # Clang returns 5, GCC returns 4 -select -assert-max 2 t:MISTRAL_ALUT6 # Clang returns 1, GCC returns 2 -select -assert-none t:MISTRAL_FF t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_ALUT4 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D diff --git a/tests/arch/intel_alm/logic.ys b/tests/arch/intel_alm/logic.ys index d34d1bc65de..831f9f1741e 100644 --- a/tests/arch/intel_alm/logic.ys +++ b/tests/arch/intel_alm/logic.ys @@ -10,16 +10,3 @@ select -assert-count 6 t:MISTRAL_ALUT2 select -assert-count 2 t:MISTRAL_ALUT4 select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT4 %% t:* %D - -design -reset -read_verilog ../common/logic.v -hierarchy -top top -proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd top # Constrain all select calls below inside the top module - -select -assert-count 1 t:MISTRAL_NOT -select -assert-count 6 t:MISTRAL_ALUT2 -select -assert-count 2 t:MISTRAL_ALUT4 -select -assert-none t:MISTRAL_NOT t:MISTRAL_ALUT2 t:MISTRAL_ALUT4 %% t:* %D \ No newline at end of file diff --git a/tests/arch/intel_alm/lutram.ys b/tests/arch/intel_alm/lutram.ys index 9ddb1ec874e..4e77afded78 100644 --- a/tests/arch/intel_alm/lutram.ys +++ b/tests/arch/intel_alm/lutram.ys @@ -37,3 +37,4 @@ select -assert-count 2 t:MISTRAL_ALUT2 select -assert-count 8 t:MISTRAL_ALUT3 select -assert-count 8 t:MISTRAL_FF select -assert-none t:MISTRAL_ALUT2 t:MISTRAL_ALUT3 t:MISTRAL_FF t:MISTRAL_MLAB %% t:* %D + diff --git a/tests/arch/intel_alm/mul.ys b/tests/arch/intel_alm/mul.ys index e147d93ac1e..75b32846304 100644 --- a/tests/arch/intel_alm/mul.ys +++ b/tests/arch/intel_alm/mul.ys @@ -9,8 +9,6 @@ cd top # Constrain all select calls below inside the top module select -assert-count 1 t:MISTRAL_MUL9X9 select -assert-none t:MISTRAL_MUL9X9 %% t:* %D -# Cyclone 10 GX does not have 9x9 multipliers. - design -reset read_verilog ../common/mul.v chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 @@ -23,18 +21,6 @@ cd top # Constrain all select calls below inside the top module select -assert-count 1 t:MISTRAL_MUL18X18 select -assert-none t:MISTRAL_MUL18X18 %% t:* %D -design -reset -read_verilog ../common/mul.v -chparam -set X_WIDTH 17 -set Y_WIDTH 17 -set A_WIDTH 34 -hierarchy -top top -proc -equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd top # Constrain all select calls below inside the top module - -select -assert-count 1 t:MISTRAL_MUL18X18 -select -assert-none t:MISTRAL_MUL18X18 %% t:* %D - design -reset read_verilog ../common/mul.v chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 @@ -47,14 +33,3 @@ cd top # Constrain all select calls below inside the top module select -assert-count 1 t:MISTRAL_MUL27X27 select -assert-none t:MISTRAL_MUL27X27 %% t:* %D -design -reset -read_verilog ../common/mul.v -chparam -set X_WIDTH 26 -set Y_WIDTH 26 -set A_WIDTH 52 -hierarchy -top top -proc -equiv_opt -assert -map +/intel_alm/common/dsp_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd top # Constrain all select calls below inside the top module - -select -assert-count 1 t:MISTRAL_MUL27X27 -select -assert-none t:MISTRAL_MUL27X27 %% t:* %D diff --git a/tests/arch/intel_alm/mux.ys b/tests/arch/intel_alm/mux.ys index 20969ead35f..951b0eff6b4 100644 --- a/tests/arch/intel_alm/mux.ys +++ b/tests/arch/intel_alm/mux.ys @@ -11,16 +11,6 @@ select -assert-count 1 t:MISTRAL_ALUT3 select -assert-none t:MISTRAL_ALUT3 %% t:* %D -design -load read -hierarchy -top mux2 -proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd mux2 # Constrain all select calls below inside the top module -select -assert-count 1 t:MISTRAL_ALUT3 -select -assert-none t:MISTRAL_ALUT3 %% t:* %D - - design -load read hierarchy -top mux4 proc @@ -31,16 +21,6 @@ select -assert-count 1 t:MISTRAL_ALUT6 select -assert-none t:MISTRAL_ALUT6 %% t:* %D -design -load read -hierarchy -top mux4 -proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd mux4 # Constrain all select calls below inside the top module -select -assert-count 1 t:MISTRAL_ALUT6 -select -assert-none t:MISTRAL_ALUT6 %% t:* %D - - design -load read hierarchy -top mux8 proc @@ -52,17 +32,6 @@ select -assert-count 2 t:MISTRAL_ALUT6 select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D -design -load read -hierarchy -top mux8 -proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd mux8 # Constrain all select calls below inside the top module -select -assert-count 1 t:MISTRAL_ALUT3 -select -assert-count 2 t:MISTRAL_ALUT6 -select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT6 %% t:* %D - - design -load read hierarchy -top mux16 proc @@ -74,15 +43,3 @@ select -assert-max 2 t:MISTRAL_ALUT5 select -assert-max 5 t:MISTRAL_ALUT6 select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D - -design -load read -hierarchy -top mux16 -proc -equiv_opt -assert -map +/intel_alm/common/alm_sim.v synth_intel_alm -family cyclone10gx -noiopad -noclkbuf # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) -cd mux16 # Constrain all select calls below inside the top module -select -assert-max 1 t:MISTRAL_ALUT3 -select -assert-max 2 t:MISTRAL_ALUT5 -select -assert-max 5 t:MISTRAL_ALUT6 - -select -assert-none t:MISTRAL_ALUT3 t:MISTRAL_ALUT5 t:MISTRAL_ALUT6 %% t:* %D diff --git a/tests/arch/intel_alm/quartus_ice.ys b/tests/arch/intel_alm/quartus_ice.ys deleted file mode 100644 index 4e1896b82a8..00000000000 --- a/tests/arch/intel_alm/quartus_ice.ys +++ /dev/null @@ -1,26 +0,0 @@ -read_verilog < Date: Wed, 10 Apr 2024 14:17:57 +0200 Subject: [PATCH 006/499] techmap: Support dynamic cell types --- kernel/constids.inc | 2 ++ passes/techmap/techmap.cc | 7 +++++++ 2 files changed, 9 insertions(+) diff --git a/kernel/constids.inc b/kernel/constids.inc index 7db21debb0e..00db94af441 100644 --- a/kernel/constids.inc +++ b/kernel/constids.inc @@ -222,6 +222,8 @@ X(_TECHMAP_REPLACE_) X(techmap_simplemap) X(_techmap_special_) X(techmap_wrap) +X(_TECHMAP_PLACEHOLDER_) +X(techmap_chtype) X(T_FALL_MAX) X(T_FALL_MIN) X(T_FALL_TYP) diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index db395315ce6..eda7c2f6c3b 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -336,6 +336,9 @@ struct TechmapWorker if (c->type.begins_with("\\$")) c->type = c->type.substr(1); + + if (c->type == ID::_TECHMAP_PLACEHOLDER_ && tpl_cell->has_attribute(ID::techmap_chtype)) + c->type = RTLIL::escape_id(tpl_cell->get_string_attribute(ID::techmap_chtype)); vector autopurge_ports; @@ -1135,6 +1138,10 @@ struct TechmapPass : public Pass { log("new wire alias to be created and named as above but with the `_TECHMAP_REPLACE_'\n"); log("prefix also substituted.\n"); log("\n"); + log("A cell with the type _TECHMAP_PLACEHOLDER_ in the map file will have its type\n"); + log("changed to the content of the techmap_chtype attribute. This allows for choosing\n"); + log("the cell type dynamically.\n"); + log("\n"); log("See 'help extract' for a pass that does the opposite thing.\n"); log("\n"); log("See 'help flatten' for a pass that does flatten the design (which is\n"); From 6ff4ecb2b42b8df40c2c44051159d53bf9eea65b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Wed, 10 Apr 2024 18:32:27 +0200 Subject: [PATCH 007/499] techmap: Remove `techmap_chtype` from the result --- passes/techmap/techmap.cc | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index eda7c2f6c3b..64de3a1cac0 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -337,8 +337,10 @@ struct TechmapWorker if (c->type.begins_with("\\$")) c->type = c->type.substr(1); - if (c->type == ID::_TECHMAP_PLACEHOLDER_ && tpl_cell->has_attribute(ID::techmap_chtype)) + if (c->type == ID::_TECHMAP_PLACEHOLDER_ && tpl_cell->has_attribute(ID::techmap_chtype)) { c->type = RTLIL::escape_id(tpl_cell->get_string_attribute(ID::techmap_chtype)); + c->attributes.erase(ID::techmap_chtype); + } vector autopurge_ports; From a833f050364c959c2eebc039c019a3df8d420825 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Thu, 2 May 2024 23:49:50 +0200 Subject: [PATCH 008/499] techmap: add dynamic cell type test --- tests/techmap/techmap_chtype.ys | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) create mode 100644 tests/techmap/techmap_chtype.ys diff --git a/tests/techmap/techmap_chtype.ys b/tests/techmap/techmap_chtype.ys new file mode 100644 index 00000000000..7c339842013 --- /dev/null +++ b/tests/techmap/techmap_chtype.ys @@ -0,0 +1,33 @@ +read_verilog < Date: Wed, 27 Mar 2024 23:54:51 +0100 Subject: [PATCH 009/499] cellmatch: New pass --- passes/techmap/Makefile.inc | 1 + passes/techmap/cellmatch.cc | 340 ++++++++++++++++++++++++++++++++++++ 2 files changed, 341 insertions(+) create mode 100644 passes/techmap/cellmatch.cc diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc index 9d57e3d71af..74813bca93f 100644 --- a/passes/techmap/Makefile.inc +++ b/passes/techmap/Makefile.inc @@ -48,6 +48,7 @@ OBJS += passes/techmap/dfflegalize.o OBJS += passes/techmap/dffunmap.o OBJS += passes/techmap/flowmap.o OBJS += passes/techmap/extractinv.o +OBJS += passes/techmap/cellmatch.o endif ifeq ($(DISABLE_SPAWN),0) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc new file mode 100644 index 00000000000..7c75418e3bc --- /dev/null +++ b/passes/techmap/cellmatch.cc @@ -0,0 +1,340 @@ +#include "kernel/celltypes.h" +#include "kernel/register.h" +#include "kernel/rtlil.h" +#include "kernel/sigtools.h" +#include "kernel/utils.h" + +#include + +USING_YOSYS_NAMESPACE +YOSYS_NAMESPACE_BEGIN + +// return module's inputs in canonical order +SigSpec module_inputs(Module *m) +{ + SigSpec ret; + for (auto port : m->ports) { + Wire *w = m->wire(port); + if (!w->port_input) + continue; + if (w->width != 1) + log_error("Unsupported wide port (%s) of non-unit width found in module %s.\n", + log_id(w), log_id(m)); + ret.append(w); + } + return ret; +} + +// return module's outputs in canonical order +SigSpec module_outputs(Module *m) +{ + SigSpec ret; + for (auto port : m->ports) { + Wire *w = m->wire(port); + if (!w->port_output) + continue; + if (w->width != 1) + log_error("Unsupported wide port (%s) of non-unit width found in module %s.\n", + log_id(w), log_id(m)); + ret.append(w); + } + return ret; +} + +uint64_t permute_lut(uint64_t lut, const std::vector &varmap) +{ + int k = varmap.size(); + uint64_t ret = 0; + for (int j = 0; j < 1 << k; j++) { + int m = 0; + for (int l = 0; l < k; l++) + if (j & 1 << l) + m |= 1 << varmap[l]; + if (lut & 1 << m) + ret |= 1 << j; + } + return ret; +} + +uint64_t p_class(int k, uint64_t lut) +{ + std::vector map; + for (int j = 0; j < k; j++) + map.push_back(j); + + uint64_t repr = ~(uint64_t) 0; + std::vector repr_vars; + while (true) { + uint64_t perm = permute_lut(lut, map); + if (perm <= repr) { + repr = perm; + repr_vars = map; + } + if (!std::next_permutation(map.begin(), map.end())) + break; + } + return repr; +} + +bool derive_module_luts(Module *m, std::vector &luts) +{ + SigMap sigmap(m); + CellTypes ff_types; + ff_types.setup_stdcells_mem(); + + dict driver; + for (auto cell : m->selected_cells()) { + if (cell->type.in(ID($specify2), ID($specify3), ID($specrule))) + continue; + + if (ff_types.cell_known(cell->type)) { + log("Ignoring module '%s' which isn't purely combinational.\n", log_id(m)); + return false; + } + + if (!cell->type.in(ID($_NOT_), ID($_AND_))) + log_error("Unsupported cell in module '%s': %s of type %s\n", + log_id(m), log_id(cell), log_id(cell->type)); + + driver[sigmap(cell->getPort(ID::Y))] = cell; + } + + TopoSort sort; + for (auto cell : m->cells()) + if (cell->type.in(ID($_NOT_), ID($_AND_))) { + sort.node(cell); + SigSpec inputs = cell->type == ID($_AND_) + ? SigSpec({cell->getPort(ID::B), cell->getPort(ID::A)}) + : cell->getPort(ID::A); + for (auto bit : sigmap(inputs)) + if (driver.count(bit)) + sort.edge(driver.at(bit), cell); + } + + if (!sort.sort()) + log_error("Module %s contains combinational loops.\n", log_id(m)); + + dict states; + states[State::S0] = 0; + states[State::S1] = ~(uint64_t) 1; + + { + uint64_t sieves[6] = { + 0xaaaaaaaaaaaaaaaa, + 0xcccccccccccccccc, + 0xf0f0f0f0f0f0f0f0, + 0xff00ff00ff00ff00, + 0xffff0000ffff0000, + 0xffffffff00000000, + }; + + SigSpec inputs = sigmap(module_inputs(m)); + if (inputs.size() > 6) { + log_warning("Skipping module %s with more than 6 inputs bits.\n", log_id(m)); + return false; + } + + for (int i = 0; i < inputs.size(); i++) + states[inputs[i]] = sieves[i] & ((((uint64_t) 1) << (1 << inputs.size())) - 1); + } + + for (auto cell : sort.sorted) { + if (cell->type.in(ID($specify2), ID($specify3), ID($specrule))) + continue; + + if (cell->type == ID($_AND_)) { + SigSpec a = sigmap(cell->getPort(ID::A)); + SigSpec b = sigmap(cell->getPort(ID::B)); + if (!states.count(a) || !states.count(b)) + log_error("Cell %s in module %s sources an undriven wire!", + log_id(cell), log_id(m)); + states[sigmap(cell->getPort(ID::Y))] = \ + states.at(a) & states.at(b); + } else if (cell->type == ID($_NOT_)) { + SigSpec a = sigmap(cell->getPort(ID::A)); + if (!states.count(a)) + log_error("Cell %s in module %s sources an undriven wire!", + log_id(cell), log_id(m)); + states[sigmap(cell->getPort(ID::Y))] = ~states.at(a); + } else { + log_abort(); + } + } + + for (auto bit : module_outputs(m)) { + if (!states.count(sigmap(bit))) + log_error("Output port %s in module %s is undriven!", + log_signal(bit), log_id(m)); + luts.push_back(states.at(sigmap(bit))); + } + return true; +} + +struct CellmatchPass : Pass { + CellmatchPass() : Pass("cellmatch", "match cells to their targets in cell library") {} + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" cellmatch -lib [module selection]\n"); + log("\n"); + log("This pass identifies functionally equivalent counterparts between each of the\n"); + log("selected modules and a module from the secondary design . For every such\n"); + log("correspondence found, a techmap rule is generated for mapping instances of the\n"); + log("former to instances of the latter. This techmap rule is saved in yet another\n"); + log("design called '$cellmatch_map', which is created if non-existent.\n"); + log("\n"); + log("This pass restricts itself to combinational modules which must be modeled with an\n"); + log("and-inverter graph. Run 'aigmap' first if necessary. Modules are functionally\n"); + log("equivalent as long as their truth tables are identical upto a permutation of\n"); + log("inputs and outputs. The number of inputs is limited to 6.\n"); + log("\n"); + } + void execute(std::vector args, RTLIL::Design *d) override + { + log_header(d, "Executing CELLMATCH pass. (match cells)\n"); + + size_t argidx; + bool lut_attrs = false; + Design *lib = NULL; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-lut_attrs") { + // an undocumented debugging option + lut_attrs = true; + } else if (args[argidx] == "-lib" && argidx + 1 < args.size()) { + if (!saved_designs.count(args[++argidx])) + log_cmd_error("No design '%s' found!\n", args[argidx].c_str()); + lib = saved_designs.at(args[argidx]); + } else { + break; + } + } + extra_args(args, argidx, d); + + if (!lib && !lut_attrs) + log_cmd_error("Missing required -lib option.\n"); + + struct Target { + Module *module; + std::vector luts; + }; + + dict, std::vector> targets; + + if (lib) + for (auto m : lib->modules()) { + pool p_classes; + + // produce a fingerprint in p_classes + int ninputs = module_inputs(m).size(); + std::vector luts; + if (!derive_module_luts(m, luts)) + continue; + for (auto lut : luts) + p_classes.insert(p_class(ninputs, lut)); + + // save as a viable target + targets[p_classes].push_back(Target{m, luts}); + } + + auto r = saved_designs.emplace("$cellmatch_map", nullptr); + if (r.second) + r.first->second = new Design; + Design *map_design = r.first->second; + + for (auto m : d->selected_whole_modules_warn()) { + std::vector luts; + if (!derive_module_luts(m, luts)) + continue; + + SigSpec inputs = module_inputs(m); + SigSpec outputs = module_outputs(m); + + if (lut_attrs) { + int no = 0; + for (auto bit : outputs) { + log_assert(bit.is_wire()); + bit.wire->attributes[ID(p_class)] = p_class(inputs.size(), luts[no]); + bit.wire->attributes[ID(lut)] = luts[no++]; + } + } + + // fingerprint + pool p_classes; + for (auto lut : luts) + p_classes.insert(p_class(inputs.size(), lut)); + + for (auto target : targets[p_classes]) { + log_debug("Candidate %s for matching to %s\n", log_id(target.module), log_id(m)); + + SigSpec target_inputs = module_inputs(target.module); + SigSpec target_outputs = module_outputs(target.module); + + if (target_inputs.size() != inputs.size()) + continue; + + if (target_outputs.size() != outputs.size()) + continue; + + std::vector input_map; + for (int i = 0; i < inputs.size(); i++) + input_map.push_back(i); + + bool found_match = false; + while (!found_match) { + std::vector output_map; + for (int i = 0; i < outputs.size(); i++) + output_map.push_back(i); + + while (!found_match) { + int out_no = 0; + bool match = true; + for (auto lut : luts) { + if (permute_lut(target.luts[output_map[out_no++]], input_map) != lut) { + match = false; + break; + } + } + + if (match) { + log("Module %s matches %s\n", log_id(m), log_id(target.module)); + Module *map = map_design->addModule(stringf("\\_60_%s_%s", log_id(m), log_id(target.module))); + Cell *cell = map->addCell(ID::_TECHMAP_REPLACE_, target.module->name); + + map->attributes[ID(techmap_celltype)] = m->name.str(); + + for (int i = 0; i < outputs.size(); i++) { + log_assert(outputs[i].is_wire()); + Wire *w = map->addWire(outputs[i].wire->name, 1); + w->port_id = outputs[i].wire->port_id; + w->port_output = true; + log_assert(target_outputs[output_map[i]].is_wire()); + cell->setPort(target_outputs[output_map[i]].wire->name, w); + } + + for (int i = 0; i < inputs.size(); i++) { + log_assert(inputs[i].is_wire()); + Wire *w = map->addWire(inputs[i].wire->name, 1); + w->port_id = inputs[i].wire->port_id; + w->port_input = true; + log_assert(target_inputs[input_map[i]].is_wire()); + cell->setPort(target_inputs[input_map[i]].wire->name, w); + } + + map->fixup_ports(); + found_match = true; + } + + if (!std::next_permutation(output_map.begin(), output_map.end())) + break; + } + + if (!std::next_permutation(input_map.begin(), input_map.end())) + break; + } + } + } + } +} CellmatchPass; + +YOSYS_NAMESPACE_END From 6a9858cdad96322ddca73d50602ce643c82edc04 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Sat, 13 Apr 2024 16:56:36 +0200 Subject: [PATCH 010/499] cellmatch: Delegate evaluation to `ConstEval` --- passes/techmap/cellmatch.cc | 107 ++++++++++-------------------------- 1 file changed, 30 insertions(+), 77 deletions(-) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc index 7c75418e3bc..9459c112fe7 100644 --- a/passes/techmap/cellmatch.cc +++ b/passes/techmap/cellmatch.cc @@ -2,6 +2,7 @@ #include "kernel/register.h" #include "kernel/rtlil.h" #include "kernel/sigtools.h" +#include "kernel/consteval.h" #include "kernel/utils.h" #include @@ -78,95 +79,48 @@ uint64_t p_class(int k, uint64_t lut) bool derive_module_luts(Module *m, std::vector &luts) { - SigMap sigmap(m); CellTypes ff_types; ff_types.setup_stdcells_mem(); - - dict driver; - for (auto cell : m->selected_cells()) { - if (cell->type.in(ID($specify2), ID($specify3), ID($specrule))) - continue; - + for (auto cell : m->cells()) { if (ff_types.cell_known(cell->type)) { log("Ignoring module '%s' which isn't purely combinational.\n", log_id(m)); return false; } - - if (!cell->type.in(ID($_NOT_), ID($_AND_))) - log_error("Unsupported cell in module '%s': %s of type %s\n", - log_id(m), log_id(cell), log_id(cell->type)); - - driver[sigmap(cell->getPort(ID::Y))] = cell; } - TopoSort sort; - for (auto cell : m->cells()) - if (cell->type.in(ID($_NOT_), ID($_AND_))) { - sort.node(cell); - SigSpec inputs = cell->type == ID($_AND_) - ? SigSpec({cell->getPort(ID::B), cell->getPort(ID::A)}) - : cell->getPort(ID::A); - for (auto bit : sigmap(inputs)) - if (driver.count(bit)) - sort.edge(driver.at(bit), cell); - } - - if (!sort.sort()) - log_error("Module %s contains combinational loops.\n", log_id(m)); - - dict states; - states[State::S0] = 0; - states[State::S1] = ~(uint64_t) 1; - - { - uint64_t sieves[6] = { - 0xaaaaaaaaaaaaaaaa, - 0xcccccccccccccccc, - 0xf0f0f0f0f0f0f0f0, - 0xff00ff00ff00ff00, - 0xffff0000ffff0000, - 0xffffffff00000000, - }; - - SigSpec inputs = sigmap(module_inputs(m)); - if (inputs.size() > 6) { - log_warning("Skipping module %s with more than 6 inputs bits.\n", log_id(m)); - return false; - } + SigSpec inputs = module_inputs(m); + SigSpec outputs = module_outputs(m); + int ninputs = inputs.size(), noutputs = outputs.size(); - for (int i = 0; i < inputs.size(); i++) - states[inputs[i]] = sieves[i] & ((((uint64_t) 1) << (1 << inputs.size())) - 1); + if (ninputs > 6) { + log_warning("Skipping module %s with more than 6 inputs bits.\n", log_id(m)); + return false; } - for (auto cell : sort.sorted) { - if (cell->type.in(ID($specify2), ID($specify3), ID($specrule))) - continue; + luts.clear(); + luts.resize(noutputs); + + ConstEval ceval(m); + for (int i = 0; i < 1 << ninputs; i++) { + ceval.clear(); + for (int j = 0; j < ninputs; j++) + ceval.set(inputs[j], (i & (1 << j)) ? State::S1 : State::S0); + for (int j = 0; j < noutputs; j++) { + SigSpec bit = outputs[j]; + + if (!ceval.eval(bit)) { + log("Failed to evaluate output '%s' in module '%s'.\n", + log_signal(outputs[j]), log_id(m)); + return false; + } - if (cell->type == ID($_AND_)) { - SigSpec a = sigmap(cell->getPort(ID::A)); - SigSpec b = sigmap(cell->getPort(ID::B)); - if (!states.count(a) || !states.count(b)) - log_error("Cell %s in module %s sources an undriven wire!", - log_id(cell), log_id(m)); - states[sigmap(cell->getPort(ID::Y))] = \ - states.at(a) & states.at(b); - } else if (cell->type == ID($_NOT_)) { - SigSpec a = sigmap(cell->getPort(ID::A)); - if (!states.count(a)) - log_error("Cell %s in module %s sources an undriven wire!", - log_id(cell), log_id(m)); - states[sigmap(cell->getPort(ID::Y))] = ~states.at(a); - } else { - log_abort(); + log_assert(ceval.eval(bit)); + + if (bit[0] == State::S1) + luts[j] |= 1 << i; } } - for (auto bit : module_outputs(m)) { - if (!states.count(sigmap(bit))) - log_error("Output port %s in module %s is undriven!", - log_signal(bit), log_id(m)); - luts.push_back(states.at(sigmap(bit))); - } return true; } @@ -184,10 +138,9 @@ struct CellmatchPass : Pass { log("former to instances of the latter. This techmap rule is saved in yet another\n"); log("design called '$cellmatch_map', which is created if non-existent.\n"); log("\n"); - log("This pass restricts itself to combinational modules which must be modeled with an\n"); - log("and-inverter graph. Run 'aigmap' first if necessary. Modules are functionally\n"); + log("This pass restricts itself to combinational modules. Modules are functionally\n"); log("equivalent as long as their truth tables are identical upto a permutation of\n"); - log("inputs and outputs. The number of inputs is limited to 6.\n"); + log("inputs and outputs. The supported number of inputs is limited to 6.\n"); log("\n"); } void execute(std::vector args, RTLIL::Design *d) override From c0e68dcc4d232542272d1ad436767175a6f04481 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Sat, 13 Apr 2024 16:56:44 +0200 Subject: [PATCH 011/499] cellmatch: Add debug print --- passes/techmap/cellmatch.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc index 9459c112fe7..5301cc99bfd 100644 --- a/passes/techmap/cellmatch.cc +++ b/passes/techmap/cellmatch.cc @@ -185,6 +185,8 @@ struct CellmatchPass : Pass { continue; for (auto lut : luts) p_classes.insert(p_class(ninputs, lut)); + + log_debug("Registered %s\n", log_id(m)); // save as a viable target targets[p_classes].push_back(Target{m, luts}); From 913bc87c4419303e32f4ca86ed437fe1e8ee015e Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Sat, 13 Apr 2024 17:12:53 +0200 Subject: [PATCH 012/499] cellmatch: Add test --- tests/techmap/cellmatch.ys | 79 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 79 insertions(+) create mode 100644 tests/techmap/cellmatch.ys diff --git a/tests/techmap/cellmatch.ys b/tests/techmap/cellmatch.ys new file mode 100644 index 00000000000..46960fc1430 --- /dev/null +++ b/tests/techmap/cellmatch.ys @@ -0,0 +1,79 @@ +read_verilog < Date: Sat, 13 Apr 2024 17:20:32 +0200 Subject: [PATCH 013/499] cellmatch: Rename the special design to `$cellmatch` --- passes/techmap/cellmatch.cc | 4 ++-- tests/techmap/cellmatch.ys | 2 +- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc index 5301cc99bfd..d1da6babd63 100644 --- a/passes/techmap/cellmatch.cc +++ b/passes/techmap/cellmatch.cc @@ -136,7 +136,7 @@ struct CellmatchPass : Pass { log("selected modules and a module from the secondary design . For every such\n"); log("correspondence found, a techmap rule is generated for mapping instances of the\n"); log("former to instances of the latter. This techmap rule is saved in yet another\n"); - log("design called '$cellmatch_map', which is created if non-existent.\n"); + log("design called '$cellmatch', which is created if non-existent.\n"); log("\n"); log("This pass restricts itself to combinational modules. Modules are functionally\n"); log("equivalent as long as their truth tables are identical upto a permutation of\n"); @@ -192,7 +192,7 @@ struct CellmatchPass : Pass { targets[p_classes].push_back(Target{m, luts}); } - auto r = saved_designs.emplace("$cellmatch_map", nullptr); + auto r = saved_designs.emplace("$cellmatch", nullptr); if (r.second) r.first->second = new Design; Design *map_design = r.first->second; diff --git a/tests/techmap/cellmatch.ys b/tests/techmap/cellmatch.ys index 46960fc1430..bea2f598d94 100644 --- a/tests/techmap/cellmatch.ys +++ b/tests/techmap/cellmatch.ys @@ -61,7 +61,7 @@ prep cellmatch -lib gatelib FA A:gate design -save gold -techmap -map %$cellmatch_map +techmap -map %$cellmatch design -save gate select -assert-none ripple_carry/t:FA From e939182e68edc26b4267f011f644067e29c7c25a Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 3 May 2024 12:11:55 +0200 Subject: [PATCH 014/499] cellmatch: add comments --- passes/techmap/cellmatch.cc | 23 ++++++++++++++++++++--- 1 file changed, 20 insertions(+), 3 deletions(-) diff --git a/passes/techmap/cellmatch.cc b/passes/techmap/cellmatch.cc index d1da6babd63..a21a4fbadc2 100644 --- a/passes/techmap/cellmatch.cc +++ b/passes/techmap/cellmatch.cc @@ -42,10 +42,16 @@ SigSpec module_outputs(Module *m) return ret; } +// Permute the inputs of a single-output k-LUT according to varmap uint64_t permute_lut(uint64_t lut, const std::vector &varmap) { int k = varmap.size(); uint64_t ret = 0; + // Index j iterates over all bits in lut. + // When (j & 1 << n) is true, + // (lut & 1 << j) represents an output value where input var n is set. + // We use this fact to permute the LUT such that + // every variable n is remapped to varmap[n]. for (int j = 0; j < 1 << k; j++) { int m = 0; for (int l = 0; l < k; l++) @@ -57,6 +63,10 @@ uint64_t permute_lut(uint64_t lut, const std::vector &varmap) return ret; } +// Find the LUT with the minimum integer representation +// such that it is a permutation of the given lut. +// The resulting LUT becomes the "fingerprint" of the "permutation class". +// This function checks all possible input permutations. uint64_t p_class(int k, uint64_t lut) { std::vector map; @@ -77,6 +87,9 @@ uint64_t p_class(int k, uint64_t lut) return repr; } +// Represent module m as N single-output k-LUTs +// where k is the number of module inputs, +// and N is the number of module outputs. bool derive_module_luts(Module *m, std::vector &luts) { CellTypes ff_types; @@ -185,7 +198,7 @@ struct CellmatchPass : Pass { continue; for (auto lut : luts) p_classes.insert(p_class(ninputs, lut)); - + log_debug("Registered %s\n", log_id(m)); // save as a viable target @@ -210,7 +223,7 @@ struct CellmatchPass : Pass { for (auto bit : outputs) { log_assert(bit.is_wire()); bit.wire->attributes[ID(p_class)] = p_class(inputs.size(), luts[no]); - bit.wire->attributes[ID(lut)] = luts[no++]; + bit.wire->attributes[ID(lut)] = luts[no++]; } } @@ -236,11 +249,13 @@ struct CellmatchPass : Pass { input_map.push_back(i); bool found_match = false; + // For each input_map while (!found_match) { std::vector output_map; for (int i = 0; i < outputs.size(); i++) output_map.push_back(i); + // For each output_map while (!found_match) { int out_no = 0; bool match = true; @@ -253,6 +268,8 @@ struct CellmatchPass : Pass { if (match) { log("Module %s matches %s\n", log_id(m), log_id(target.module)); + // Add target.module to map_design ("$cellmatch") + // as a techmap rule to match m and replace it with target.module Module *map = map_design->addModule(stringf("\\_60_%s_%s", log_id(m), log_id(target.module))); Cell *cell = map->addCell(ID::_TECHMAP_REPLACE_, target.module->name); @@ -281,7 +298,7 @@ struct CellmatchPass : Pass { } if (!std::next_permutation(output_map.begin(), output_map.end())) - break; + break; } if (!std::next_permutation(input_map.begin(), input_map.end())) From 4c000d3aba7ab080a95ed0a4b3de5c756f69646b Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Wed, 10 Apr 2024 15:20:01 +0200 Subject: [PATCH 015/499] Add new `bbox_derive` command for blackbox derivation --- passes/cmds/Makefile.inc | 1 + passes/cmds/bbox_derive.cc | 90 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 91 insertions(+) create mode 100644 passes/cmds/bbox_derive.cc diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc index d7e572462b0..b1c9c67f0d0 100644 --- a/passes/cmds/Makefile.inc +++ b/passes/cmds/Makefile.inc @@ -48,3 +48,4 @@ OBJS += passes/cmds/clean_zerowidth.o OBJS += passes/cmds/xprop.o OBJS += passes/cmds/dft_tag.o OBJS += passes/cmds/future.o +OBJS += passes/cmds/bbox_derive.o diff --git a/passes/cmds/bbox_derive.cc b/passes/cmds/bbox_derive.cc new file mode 100644 index 00000000000..de0869cb1eb --- /dev/null +++ b/passes/cmds/bbox_derive.cc @@ -0,0 +1,90 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2024 Martin Povišer + * + * Permission to use, copy, modify, and/or distribute this software for any + * purpose with or without fee is hereby granted, provided that the above + * copyright notice and this permission notice appear in all copies. + * + * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES + * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF + * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR + * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES + * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN + * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF + * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE. + * + */ +#include "kernel/yosys.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct BboxDerivePass : Pass { + BboxDerivePass() : Pass("bbox_derive", "derive blackbox modules") {} + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" bbox_derive [-base ] [-naming_attr ] [selection]\n"); + log("\n"); + } + void execute(std::vector args, RTLIL::Design *d) override + { + log_header(d, "Executing BBOX_DERIVE pass. (derive modules for blackboxes)\n"); + + size_t argidx; + IdString naming_attr; + IdString base_name; + for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-naming_attr" && argidx + 1 < args.size()) + naming_attr = RTLIL::escape_id(args[++argidx]); + else if (args[argidx] == "-base" && argidx + 1 < args.size()) + base_name = RTLIL::escape_id(args[++argidx]); + else + break; + } + extra_args(args, argidx, d); + + Module *base_override; + if (!base_name.empty()) { + base_override = d->module(base_name); + if (!base_override) + log_cmd_error("Base module %s not found.\n", log_id(base_name)); + } + + dict, Module*> done; + + for (auto module : d->selected_modules()) { + for (auto cell : module->selected_cells()) { + Module *inst_module = d->module(cell->type); + if (!inst_module || !inst_module->get_blackbox_attribute()) + continue; + + if (cell->parameters.empty() || done.count(cell->parameters)) + continue; + + Module *base = inst_module; + if (base_override) + base = base_override; + + IdString derived_type = base->derive(d, cell->parameters); + Module *derived = d->module(derived_type); + + if (!naming_attr.empty() && derived->has_attribute(naming_attr)) { + IdString new_name = RTLIL::escape_id(derived->get_string_attribute(naming_attr)); + if (!new_name.isPublic()) + log_error("Derived module %s cannot be renamed to private name %s.\n", + log_id(derived), log_id(new_name)); + derived->attributes.erase(naming_attr); + d->rename(derived, new_name); + } + + done[cell->parameters] = derived; + } + } + } +} BboxDerivePass; + +PRIVATE_NAMESPACE_END From e8c58a55280192db2c35006734f42c7983cd9b81 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 3 May 2024 20:41:42 +0200 Subject: [PATCH 016/499] bbox_derive: fix unininitialized memory UB when run with no named args --- passes/cmds/bbox_derive.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/cmds/bbox_derive.cc b/passes/cmds/bbox_derive.cc index de0869cb1eb..758f793004a 100644 --- a/passes/cmds/bbox_derive.cc +++ b/passes/cmds/bbox_derive.cc @@ -47,7 +47,7 @@ struct BboxDerivePass : Pass { } extra_args(args, argidx, d); - Module *base_override; + Module *base_override = nullptr; if (!base_name.empty()) { base_override = d->module(base_name); if (!base_override) From 44b0fdc2bf8bac019641f4f5c5f9d29294fc0624 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Fri, 3 May 2024 20:43:01 +0200 Subject: [PATCH 017/499] bbox_derive: add assert and debug print --- passes/cmds/bbox_derive.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/cmds/bbox_derive.cc b/passes/cmds/bbox_derive.cc index 758f793004a..a35e9629058 100644 --- a/passes/cmds/bbox_derive.cc +++ b/passes/cmds/bbox_derive.cc @@ -71,6 +71,8 @@ struct BboxDerivePass : Pass { IdString derived_type = base->derive(d, cell->parameters); Module *derived = d->module(derived_type); + log_assert(derived && "Failed to derive module\n"); + log_debug("derived %s\n", derived_type.c_str()); if (!naming_attr.empty() && derived->has_attribute(naming_attr)) { IdString new_name = RTLIL::escape_id(derived->get_string_attribute(naming_attr)); From 0f9ee20ea2c9b377f9b28b862f77b197e6485e00 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Sat, 4 May 2024 00:16:00 +0000 Subject: [PATCH 018/499] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 2dbce272dc6..56efaf5eb0f 100644 --- a/Makefile +++ b/Makefile @@ -142,7 +142,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.40+45 +YOSYS_VER := 0.40+50 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From bb0be8c7a20335f8e03597cfcf052609f8a1f4a4 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 4 May 2024 16:51:29 +1200 Subject: [PATCH 019/499] Docs: Set release to YOSYS_VER If building from read the docs, and the current build is "latest", add `-dev` to the version string. Requires `YOSYS_VER` to be exported by .readthedocs.yaml. --- docs/source/conf.py | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/docs/source/conf.py b/docs/source/conf.py index 29d36d9c45f..aed3fddff7c 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -63,6 +63,14 @@ extensions.append('sphinx.ext.todo') todo_include_todos = False +# attempt to get version +env_yosys_ver = os.getenv("YOSYS_VER") +if env_yosys_ver: + if os.getenv("READTHEDOCS") and os.getenv("READTHEDOCS_VERSION") == "latest": + release = env_yosys_ver + "-dev" + else: + release = env_yosys_ver + # custom cmd-ref parsing/linking sys.path += [os.path.dirname(__file__) + "/../"] extensions.append('util.cmdref') From fe27240b3a9c0be98dd16b3fc27cef61ddb50946 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 4 May 2024 16:51:38 +1200 Subject: [PATCH 020/499] Makefile: Export YOSYS_VER --- Makefile | 1 + 1 file changed, 1 insertion(+) diff --git a/Makefile b/Makefile index 56efaf5eb0f..2e93bcc8dc3 100644 --- a/Makefile +++ b/Makefile @@ -143,6 +143,7 @@ endif endif YOSYS_VER := 0.40+50 +export YOSYS_VER # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo From 6eb49ee9e830545e212f9aefe90d5bd130afa7a4 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Tue, 7 May 2024 10:23:22 +1200 Subject: [PATCH 021/499] Makefile: Export YOSYS_VER only for make docs --- Makefile | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/Makefile b/Makefile index 2e93bcc8dc3..6711751b62d 100644 --- a/Makefile +++ b/Makefile @@ -143,7 +143,6 @@ endif endif YOSYS_VER := 0.40+50 -export YOSYS_VER # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -1013,7 +1012,7 @@ docs/reqs: DOC_TARGET ?= html docs: docs/source/cmd/abc.rst docs/gen_examples docs/gen_images docs/guidelines docs/usage docs/reqs - $(Q) $(MAKE) -C docs $(DOC_TARGET) + $(Q) YOSYS_VER=$(YOSYS_VER) $(MAKE) -C docs $(DOC_TARGET) clean: rm -rf share From b4034a881e0cf476bbdc19e984a9762bb260ad39 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 7 May 2024 15:35:25 +0200 Subject: [PATCH 022/499] Keep docs version in conf.py --- Makefile | 2 +- docs/source/conf.py | 19 +++++++++---------- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/Makefile b/Makefile index 6711751b62d..56efaf5eb0f 100644 --- a/Makefile +++ b/Makefile @@ -1012,7 +1012,7 @@ docs/reqs: DOC_TARGET ?= html docs: docs/source/cmd/abc.rst docs/gen_examples docs/gen_images docs/guidelines docs/usage docs/reqs - $(Q) YOSYS_VER=$(YOSYS_VER) $(MAKE) -C docs $(DOC_TARGET) + $(Q) $(MAKE) -C docs $(DOC_TARGET) clean: rm -rf share diff --git a/docs/source/conf.py b/docs/source/conf.py index aed3fddff7c..4e46cfad1b8 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -4,7 +4,8 @@ project = 'YosysHQ Yosys' author = 'YosysHQ GmbH' -copyright ='2022 YosysHQ GmbH' +copyright ='2024 YosysHQ GmbH' +yosys_ver = "0.40" # select HTML theme html_theme = 'furo' @@ -46,12 +47,18 @@ autosectionlabel_prefix_document = True autosectionlabel_maxdepth = 1 +# set version +if os.getenv("READTHEDOCS") and os.getenv("READTHEDOCS_VERSION") == "latest": + release = yosys_ver + "-dev" +else: + release = yosys_ver + # assign figure numbers numfig = True bibtex_bibfiles = ['literature.bib'] - latex_elements = { + 'releasename': ' ', 'preamble': r''' \usepackage{lmodern} \usepackage{comment} @@ -63,14 +70,6 @@ extensions.append('sphinx.ext.todo') todo_include_todos = False -# attempt to get version -env_yosys_ver = os.getenv("YOSYS_VER") -if env_yosys_ver: - if os.getenv("READTHEDOCS") and os.getenv("READTHEDOCS_VERSION") == "latest": - release = env_yosys_ver + "-dev" - else: - release = env_yosys_ver - # custom cmd-ref parsing/linking sys.path += [os.path.dirname(__file__) + "/../"] extensions.append('util.cmdref') From 71f2540cd840046499e1dd84c76ea64c437140d3 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 7 May 2024 15:55:52 +0200 Subject: [PATCH 023/499] docs conf.py change Release -> Version --- docs/source/conf.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/source/conf.py b/docs/source/conf.py index 4e46cfad1b8..182d033f8ce 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -58,7 +58,7 @@ bibtex_bibfiles = ['literature.bib'] latex_elements = { - 'releasename': ' ', + 'releasename': 'Version', 'preamble': r''' \usepackage{lmodern} \usepackage{comment} From a52088b6af5c4467835de173d83a00645546eddf Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 7 May 2024 17:57:37 +0200 Subject: [PATCH 024/499] smtbmc: Improvements for --incremental and .yw fixes This extends the experimental incremental JSON API to allow arbitrary smtlib subexpressions, defining smtlib constants and to allow access of signals by their .yw path. It also fixes a bug during .yw writing where values would be re-emitted in later cycles if they have no newer defined value and a potential crash when using --track-assumes. --- backends/smt2/smtbmc.py | 203 +++++++++++++++++----------- backends/smt2/smtbmc_incremental.py | 147 ++++++++++++++++++-- backends/smt2/smtio.py | 21 ++- 3 files changed, 279 insertions(+), 92 deletions(-) diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index e6b4088dbd7..995a714c926 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -199,7 +199,6 @@ def help(): --minimize-assumes when using --track-assumes, solve for a minimal set of sufficient assumptions. - """ + so.helpmsg()) def usage(): @@ -670,18 +669,12 @@ def print_msg(msg): ywfile_hierwitness_cache = None -def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): +def ywfile_hierwitness(): global ywfile_hierwitness_cache - if map_steps is None: - map_steps = {} - - with open(inywfile, "r") as f: - inyw = ReadWitness(f) - - if ywfile_hierwitness_cache is None: - ywfile_hierwitness_cache = smt.hierwitness(topmod, allregs=True, blackbox=True) + if ywfile_hierwitness_cache is None: + ywfile_hierwitness = smt.hierwitness(topmod, allregs=True, blackbox=True) - inits, seqs, clocks, mems = ywfile_hierwitness_cache + inits, seqs, clocks, mems = ywfile_hierwitness smt_wires = defaultdict(list) smt_mems = defaultdict(list) @@ -692,91 +685,147 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): for mem in mems: smt_mems[mem["path"]].append(mem) - addr_re = re.compile(r'\\\[[0-9]+\]$') - bits_re = re.compile(r'[01?]*$') + ywfile_hierwitness_cache = inits, seqs, clocks, mems, smt_wires, smt_mems - max_t = -1 + return ywfile_hierwitness_cache - for t, step in inyw.steps(): - present_signals, missing = step.present_signals(inyw.sigmap) - for sig in present_signals: - bits = step[sig] - if skip_x: - bits = bits.replace('x', '?') - if not bits_re.match(bits): - raise ValueError("unsupported bit value in Yosys witness file") +def_bits_re = re.compile(r'([01]+)') - sig_end = sig.offset + len(bits) - if sig.path in smt_wires: - for wire in smt_wires[sig.path]: - width, offset = wire["width"], wire["offset"] +def smt_extract_mask(smt_expr, mask): + chunks = [] + def_bits = '' - smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 + mask_index_order = mask[::-1] - offset = max(offset, 0) + for matched in def_bits_re.finditer(mask_index_order): + chunks.append(matched.span()) + def_bits += matched[0] - end = width + offset - common_offset = max(sig.offset, offset) - common_end = min(sig_end, end) - if common_end <= common_offset: - continue + if not chunks: + return - smt_expr = smt.witness_net_expr(topmod, f"s{map_steps.get(t, t)}", wire) + if len(chunks) == 1: + start, end = chunks[0] + if start == 0 and end == len(mask_index_order): + combined_chunks = smt_expr + else: + combined_chunks = '((_ extract %d %d) %s)' % (end - 1, start, smt_expr) + else: + combined_chunks = '(let ((x %s)) (concat %s))' % (smt_expr, ' '.join( + '((_ extract %d %d) x)' % (end - 1, start) + for start, end in reversed(chunks) + )) - if not smt_bool: - slice_high = common_end - offset - 1 - slice_low = common_offset - offset - smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr) + return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1] - bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)] +def smt_concat(exprs): + if not exprs: + return "" + if len(exprs) == 1: + return exprs[1] + return "(concat %s)" % ' '.join(exprs) - if bit_slice.count("?") == len(bit_slice): - continue +def ywfile_signal(sig, step, mask=None): + assert sig.width > 0 - if smt_bool: - assert width == 1 - smt_constr = "(= %s %s)" % (smt_expr, "true" if bit_slice == "1" else "false") - else: - if "?" in bit_slice: - mask = bit_slice.replace("0", "1").replace("?", "0") - bit_slice = bit_slice.replace("?", "0") - smt_expr = "(bvand %s #b%s)" % (smt_expr, mask) + inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness() + sig_end = sig.offset + sig.width - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) + output = [] - constr_assumes[t].append((inywfile, smt_constr)) + if sig.path in smt_wires: + for wire in smt_wires[sig.path]: + width, offset = wire["width"], wire["offset"] - if sig.memory_path: - if sig.memory_path in smt_mems: - for mem in smt_mems[sig.memory_path]: - width, size, bv = mem["width"], mem["size"], mem["statebv"] + smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 - smt_expr = smt.net_expr(topmod, f"s{map_steps.get(t, t)}", mem["smtpath"]) + offset = max(offset, 0) - if bv: - word_low = sig.memory_addr * width - word_high = word_low + width - 1 - smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr) - else: - addr_width = (size - 1).bit_length() - addr_bits = f"{sig.memory_addr:0{addr_width}b}" - smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits) + end = width + offset + common_offset = max(sig.offset, offset) + common_end = min(sig_end, end) + if common_end <= common_offset: + continue - if len(bits) < width: - slice_high = sig.offset + len(bits) - 1 - smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) + smt_expr = smt.witness_net_expr(topmod, f"s{step}", wire) - bit_slice = bits + if not smt_bool: + slice_high = common_end - offset - 1 + slice_low = common_offset - offset + smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr) + else: + smt_expr = "(ite %s #b1 #b0)" % smt_expr - if "?" in bit_slice: - mask = bit_slice.replace("0", "1").replace("?", "0") - bit_slice = bit_slice.replace("?", "0") - smt_expr = "(bvand %s #b%s)" % (smt_expr, mask) + output.append(((common_offset - sig.offset), (common_end - sig.offset), smt_expr)) - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) - constr_assumes[t].append((inywfile, smt_constr)) - max_t = t + if sig.memory_path: + if sig.memory_path in smt_mems: + for mem in smt_mems[sig.memory_path]: + width, size, bv = mem["width"], mem["size"], mem["statebv"] + + smt_expr = smt.net_expr(topmod, f"s{step}", mem["smtpath"]) + + if bv: + word_low = sig.memory_addr * width + word_high = word_low + width - 1 + smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr) + else: + addr_width = (size - 1).bit_length() + addr_bits = f"{sig.memory_addr:0{addr_width}b}" + smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits) + + if sig.width < width: + slice_high = sig.offset + sig.width - 1 + smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) + output.append((0, sig.width, smt_expr)) + + output.sort() + + output = [chunk for chunk in output if chunk[0] != chunk[1]] + + pos = 0 + + for start, end, smt_expr in output: + assert start == pos + pos = end + + assert pos == sig.width + + if len(output) == 1: + return output[0][-1] + return smt_concat(smt_expr for start, end, smt_expr in reversed(output)) + +def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False): + global ywfile_hierwitness_cache + if map_steps is None: + map_steps = {} + + with open(inywfile, "r") as f: + inyw = ReadWitness(f) + + inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness() + + bits_re = re.compile(r'[01?]*$') + max_t = -1 + + for t, step in inyw.steps(): + present_signals, missing = step.present_signals(inyw.sigmap) + for sig in present_signals: + bits = step[sig] + if skip_x: + bits = bits.replace('x', '?') + if not bits_re.match(bits): + raise ValueError("unsupported bit value in Yosys witness file") + + smt_expr = ywfile_signal(sig, map_steps.get(t, t)) + + smt_expr, bits = smt_extract_mask(smt_expr, bits) + + smt_constr = "(= %s #b%s)" % (smt_expr, bits) + constr_assumes[t].append((inywfile, smt_constr)) + + max_t = t return max_t if inywfile is not None: @@ -1367,11 +1416,11 @@ def write_yw_trace(steps, index, allregs=False, filename=None): exprs.extend(smt.witness_net_expr(topmod, f"s{k}", sig) for sig in sigs) - all_sigs.append(sigs) + all_sigs.append((step_values, sigs)) bvs = iter(smt.get_list(exprs)) - for sigs in all_sigs: + for (step_values, sigs) in all_sigs: for sig in sigs: value = smt.bv2bin(next(bvs)) step_values[sig["sig"]] = value diff --git a/backends/smt2/smtbmc_incremental.py b/backends/smt2/smtbmc_incremental.py index f43e878f31c..0bd280b4a48 100644 --- a/backends/smt2/smtbmc_incremental.py +++ b/backends/smt2/smtbmc_incremental.py @@ -1,7 +1,7 @@ from collections import defaultdict import json import typing -from functools import partial +import ywio if typing.TYPE_CHECKING: import smtbmc @@ -34,6 +34,7 @@ def __init__(self): self._witness_index = None self._yw_constraints = {} + self._define_sorts = {} def setup(self): generic_assert_map = smtbmc.get_assert_map( @@ -175,11 +176,7 @@ def expr_andor(self, expr, smt_out): if len(expr) == 1: smt_out.push({"and": "true", "or": "false"}[expr[0]]) elif len(expr) == 2: - arg_sort = self.expr(expr[1], smt_out) - if arg_sort != "Bool": - raise InteractiveError( - f"arguments of {json.dumps(expr[0])} must have sort Bool" - ) + self.expr(expr[1], smt_out, required_sort="Bool") else: sep = f"({expr[0]} " for arg in expr[1:]: @@ -189,7 +186,51 @@ def expr_andor(self, expr, smt_out): smt_out.append(")") return "Bool" + def expr_bv_binop(self, expr, smt_out): + self.expr_arg_len(expr, 2) + + smt_out.append(f"({expr[0]} ") + arg_sort = self.expr(expr[1], smt_out, required_sort=("BitVec", None)) + smt_out.append(" ") + self.expr(expr[2], smt_out, required_sort=arg_sort) + smt_out.append(")") + return arg_sort + + def expr_extract(self, expr, smt_out): + self.expr_arg_len(expr, 3) + + hi = expr[1] + lo = expr[2] + + smt_out.append(f"((_ extract {hi} {lo}) ") + + arg_sort = self.expr(expr[3], smt_out, required_sort=("BitVec", None)) + smt_out.append(")") + + if not (isinstance(hi, int) and 0 <= hi < arg_sort[1]): + raise InteractiveError( + f"high bit index must be 0 <= index < {arg_sort[1]}, is {hi!r}" + ) + if not (isinstance(lo, int) and 0 <= lo <= hi): + raise InteractiveError( + f"low bit index must be 0 <= index < {hi}, is {lo!r}" + ) + + return "BitVec", hi - lo + 1 + + def expr_bv(self, expr, smt_out): + self.expr_arg_len(expr, 1) + + arg = expr[1] + if not isinstance(arg, str) or arg.count("0") + arg.count("1") != len(arg): + raise InteractiveError("bv argument must contain only 0 or 1 bits") + + smt_out.append("#b" + arg) + + return "BitVec", len(arg) + def expr_yw(self, expr, smt_out): + self.expr_arg_len(expr, 1, 2) if len(expr) == 2: name = None step = expr[1] @@ -219,6 +260,40 @@ def expr_yw(self, expr, smt_out): return "Bool" + def expr_yw_sig(self, expr, smt_out): + self.expr_arg_len(expr, 3, 4) + + step = expr[1] + path = expr[2] + offset = expr[3] + width = expr[4] if len(expr) == 5 else 1 + + if not isinstance(offset, int) or offset < 0: + raise InteractiveError( + f"offset must be a non-negative integer, got {json.dumps(offset)}" + ) + + if not isinstance(width, int) or width <= 0: + raise InteractiveError( + f"width must be a positive integer, got {json.dumps(width)}" + ) + + if not isinstance(path, list) or not all(isinstance(s, str) for s in path): + raise InteractiveError( + f"path must be a string list, got {json.dumps(path)}" + ) + + if step not in self.state_set: + raise InteractiveError(f"step {step} not declared") + + smt_expr = smtbmc.ywfile_signal( + ywio.WitnessSig(path=path, offset=offset, width=width), step + ) + + smt_out.append(smt_expr) + + return "BitVec", width + def expr_smtlib(self, expr, smt_out): self.expr_arg_len(expr, 2) @@ -231,10 +306,15 @@ def expr_smtlib(self, expr, smt_out): f"got {json.dumps(smtlib_expr)}" ) - if not isinstance(sort, str): - raise InteractiveError( - f"raw SMT-LIB sort has to be a string, got {json.dumps(sort)}" - ) + if ( + isinstance(sort, list) + and len(sort) == 2 + and sort[0] == "BitVec" + and (sort[1] is None or isinstance(sort[1], int)) + ): + sort = tuple(sort) + elif not isinstance(sort, str): + raise InteractiveError(f"unsupported raw SMT-LIB sort {json.dumps(sort)}") smt_out.append(smtlib_expr) return sort @@ -258,6 +338,14 @@ def expr_label(self, expr, smt_out): return sort + def expr_def(self, expr, smt_out): + self.expr_arg_len(expr, 1) + sort = self._define_sorts.get(expr[1]) + if sort is None: + raise InteractiveError(f"unknown definition {json.dumps(expr)}") + smt_out.append(expr[1]) + return sort + expr_handlers = { "step": expr_step, "cell": expr_cell, @@ -270,8 +358,15 @@ def expr_label(self, expr, smt_out): "not": expr_not, "and": expr_andor, "or": expr_andor, + "bv": expr_bv, + "bvand": expr_bv_binop, + "bvor": expr_bv_binop, + "bvxor": expr_bv_binop, + "extract": expr_extract, + "def": expr_def, "=": expr_eq, "yw": expr_yw, + "yw_sig": expr_yw_sig, "smtlib": expr_smtlib, "!": expr_label, } @@ -305,10 +400,13 @@ def expr(self, expr, smt_out, required_sort=None): raise InteractiveError(f"unknown expression {json.dumps(expr[0])}") def expr_smt(self, expr, required_sort): + return self.expr_smt_and_sort(expr, required_sort)[0] + + def expr_smt_and_sort(self, expr, required_sort=None): smt_out = [] - self.expr(expr, smt_out, required_sort=required_sort) + output_sort = self.expr(expr, smt_out, required_sort=required_sort) out = "".join(smt_out) - return out + return out, output_sort def cmd_new_step(self, cmd): step = self.arg_step(cmd, declare=True) @@ -338,7 +436,6 @@ def cmd_update_assumptions(self, cmd): expr = cmd.get("expr") key = cmd.get("key") - key = mkkey(key) result = smtbmc.smt.smt2_assumptions.pop(key, None) @@ -348,7 +445,7 @@ def cmd_update_assumptions(self, cmd): return result def cmd_get_unsat_assumptions(self, cmd): - return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get('minimize'))) + return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get("minimize"))) def cmd_push(self, cmd): smtbmc.smt_push() @@ -370,6 +467,27 @@ def cmd_smtlib(self, cmd): if response: return smtbmc.smt.read() + def cmd_define(self, cmd): + expr = cmd.get("expr") + if expr is None: + raise InteractiveError("'define' copmmand requires 'expr' parameter") + + expr, sort = self.expr_smt_and_sort(expr) + + if isinstance(sort, tuple) and sort[0] == "module": + raise InteractiveError("'define' does not support module sorts") + + define_name = f"|inc def {len(self._define_sorts)}|" + + self._define_sorts[define_name] = sort + + if isinstance(sort, tuple): + sort = f"(_ {' '.join(map(str, sort))})" + + smtbmc.smt.write(f"(define-const {define_name} {sort} {expr})") + + return {"name": define_name} + def cmd_design_hierwitness(self, cmd=None): allregs = (cmd is None) or bool(cmd.get("allreges", False)) if self._cached_hierwitness[allregs] is not None: @@ -451,6 +569,7 @@ def cmd_ping(self, cmd): "pop": cmd_pop, "check": cmd_check, "smtlib": cmd_smtlib, + "define": cmd_define, "design_hierwitness": cmd_design_hierwitness, "write_yw_trace": cmd_write_yw_trace, "read_yw_trace": cmd_read_yw_trace, diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e32f43c60a0..5fc3ab5a424 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -160,6 +160,7 @@ def __init__(self, opts=None): self.noincr = opts.noincr self.info_stmts = opts.info_stmts self.nocomments = opts.nocomments + self.smt2_options.update(opts.smt2_options) else: self.solver = "yices" @@ -959,6 +960,8 @@ def bv2int(self, v): return int(self.bv2bin(v), 2) def get_raw_unsat_assumptions(self): + if not self.smt2_assumptions: + return [] self.write("(get-unsat-assumptions)") exprs = set(self.unparse(part) for part in self.parse(self.read())) unsat_assumptions = [] @@ -973,6 +976,10 @@ def get_raw_unsat_assumptions(self): def get_unsat_assumptions(self, minimize=False): if not minimize: return self.get_raw_unsat_assumptions() + orig_assumptions = self.smt2_assumptions + + self.smt2_assumptions = dict(orig_assumptions) + required_assumptions = {} while True: @@ -998,6 +1005,7 @@ def get_unsat_assumptions(self, minimize=False): required_assumptions[candidate_key] = candidate_assume if candidate_assumptions is not None: + self.smt2_assumptions = orig_assumptions return list(required_assumptions) def get(self, expr): @@ -1146,7 +1154,7 @@ def wait(self): class SmtOpts: def __init__(self): self.shortopts = "s:S:v" - self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"] + self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments", "smt2-option="] self.solver = "yices" self.solver_opts = list() self.debug_print = False @@ -1159,6 +1167,7 @@ def __init__(self): self.logic = None self.info_stmts = list() self.nocomments = False + self.smt2_options = {} def handle(self, o, a): if o == "-s": @@ -1185,6 +1194,13 @@ def handle(self, o, a): self.info_stmts.append(a) elif o == "--nocomments": self.nocomments = True + elif o == "--smt2-option": + args = a.split('=', 1) + if len(args) != 2: + print("--smt2-option expects an