From 9315f02c17ef5b3149a4767d9851045f2cee15cb Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Mon, 25 Mar 2024 11:33:52 +0000 Subject: [PATCH 01/36] ezsat: New Sat class to call an external command --- Makefile | 2 + libs/ezsat/ezcommand.cc | 83 +++++++++++++++++++++++++++++++++++++++++ libs/ezsat/ezcommand.h | 36 ++++++++++++++++++ 3 files changed, 121 insertions(+) create mode 100644 libs/ezsat/ezcommand.cc create mode 100644 libs/ezsat/ezcommand.h diff --git a/Makefile b/Makefile index 8205bb3ed..afe559712 100644 --- a/Makefile +++ b/Makefile @@ -638,6 +638,7 @@ $(eval $(call add_include_file,kernel/yosys_common.h)) $(eval $(call add_include_file,kernel/yw.h)) $(eval $(call add_include_file,libs/ezsat/ezsat.h)) $(eval $(call add_include_file,libs/ezsat/ezminisat.h)) +$(eval $(call add_include_file,libs/ezsat/ezcommand.h)) ifeq ($(ENABLE_ZLIB),1) $(eval $(call add_include_file,libs/fst/fstapi.h)) endif @@ -683,6 +684,7 @@ OBJS += libs/json11/json11.o OBJS += libs/ezsat/ezsat.o OBJS += libs/ezsat/ezminisat.o +OBJS += libs/ezsat/ezcommand.o OBJS += libs/minisat/Options.o OBJS += libs/minisat/SimpSolver.o diff --git a/libs/ezsat/ezcommand.cc b/libs/ezsat/ezcommand.cc new file mode 100644 index 000000000..10104a2cd --- /dev/null +++ b/libs/ezsat/ezcommand.cc @@ -0,0 +1,83 @@ + +#include "ezcommand.h" + +#include "../../kernel/yosys.h" + +ezSATCommand::ezSATCommand(const std::string &cmd) : command(cmd) {} + +ezSATCommand::~ezSATCommand() {} + +bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) +{ + if (!assumptions.empty()) { + Yosys::log_error("Assumptions are not supported yet by command-based Sat solver\n"); + } + const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX"); + const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str()); + const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str()); + FILE *dimacs = fopen(cnf_filename.c_str(), "w"); + printDIMACS(dimacs); + fclose(dimacs); + + std::vector modelIdx; + for (auto id : modelExpressions) + modelIdx.push_back(bind(id)); + + bool status_sat = false; + bool status_unsat = false; + std::vector values; + + auto line_callback = [&](const std::string &line) { + if (line.empty()) { + return; + } + if (line[0] == 's') { + if (line.substr(0, 5) == "s SAT") { + status_sat = true; + } + if (line.substr(0, 7) == "s UNSAT") { + status_unsat = true; + } + return; + } + if (line[0] == 'v') { + std::stringstream ss(line.substr(1)); + int lit; + while (ss >> lit) { + if (lit == 0) { + return; + } + bool val = lit >= 0; + int ind = lit >= 0 ? lit - 1 : -lit - 1; + if (Yosys::GetSize(values) <= ind) { + values.resize(ind + 1); + } + values[ind] = val; + } + } + }; + if (Yosys::run_command(sat_command, line_callback) != 0) { + Yosys::log_cmd_error("Shell command failed!\n"); + } + + modelValues.clear(); + modelValues.resize(modelIdx.size()); + + if (!status_sat && !status_unsat) { + solverTimoutStatus = true; + } + if (!status_sat) { + return false; + } + + for (size_t i = 0; i < modelIdx.size(); i++) { + int idx = modelIdx[i]; + bool refvalue = true; + + if (idx < 0) + idx = -idx, refvalue = false; + + modelValues[i] = (values.at(idx - 1) == refvalue); + } + return true; +} \ No newline at end of file diff --git a/libs/ezsat/ezcommand.h b/libs/ezsat/ezcommand.h new file mode 100644 index 000000000..a0e3de4ed --- /dev/null +++ b/libs/ezsat/ezcommand.h @@ -0,0 +1,36 @@ +/* + * ezSAT -- A simple and easy to use CNF generator for SAT solvers + * + * Copyright (C) 2013 Claire Xenia Wolf + * + * 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. + * + */ + +#ifndef EZSATCOMMAND_H +#define EZSATCOMMAND_H + +#include "ezsat.h" + +class ezSATCommand : public ezSAT +{ +private: + std::string command; + +public: + ezSATCommand(const std::string &cmd); + virtual ~ezSATCommand(); + bool solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) override; +}; + +#endif From 12315c0d17c911a971298e233c4a1d1aa291c9c7 Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Thu, 28 Mar 2024 09:56:48 +0000 Subject: [PATCH 02/36] ezsat: Support for assumptions in Sat command --- libs/ezsat/ezcommand.cc | 11 ++++++----- libs/ezsat/ezsat.cc | 6 ++++-- libs/ezsat/ezsat.h | 2 +- 3 files changed, 11 insertions(+), 8 deletions(-) diff --git a/libs/ezsat/ezcommand.cc b/libs/ezsat/ezcommand.cc index 10104a2cd..c2925b647 100644 --- a/libs/ezsat/ezcommand.cc +++ b/libs/ezsat/ezcommand.cc @@ -9,19 +9,20 @@ ezSATCommand::~ezSATCommand() {} bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) { - if (!assumptions.empty()) { - Yosys::log_error("Assumptions are not supported yet by command-based Sat solver\n"); - } const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX"); const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str()); const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str()); FILE *dimacs = fopen(cnf_filename.c_str(), "w"); - printDIMACS(dimacs); - fclose(dimacs); std::vector modelIdx; for (auto id : modelExpressions) modelIdx.push_back(bind(id)); + std::vector> extraClauses; + for (auto id : assumptions) + extraClauses.push_back({bind(id)}); + + printDIMACS(dimacs, false, extraClauses); + fclose(dimacs); bool status_sat = false; bool status_unsat = false; diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 20a210abe..fbdfc20f6 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -1222,7 +1222,7 @@ ezSATvec ezSAT::vec(const std::vector &vec) return ezSATvec(*this, vec); } -void ezSAT::printDIMACS(FILE *f, bool verbose) const +void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector> &extraClauses) const { if (cnfConsumed) { fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!"); @@ -1259,8 +1259,10 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const std::vector> all_clauses; getFullCnf(all_clauses); assert(cnfClausesCount == int(all_clauses.size())); + for (auto c : extraClauses) + all_clauses.push_back(c); - fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount); + fprintf(f, "p cnf %d %d\n", cnfVariableCount, (int) all_clauses.size()); int maxClauseLen = 0; for (auto &clause : all_clauses) maxClauseLen = std::max(int(clause.size()), maxClauseLen); diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 7f3bdf68d..507708cb2 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -295,7 +295,7 @@ public: // printing CNF and internal state - void printDIMACS(FILE *f, bool verbose = false) const; + void printDIMACS(FILE *f, bool verbose = false, const std::vector> &extraClauses = std::vector>()) const; void printInternalState(FILE *f) const; // more sophisticated constraints (designed to be used directly with assume(..)) From 6565bf3ebfeba59bd17acce26632bc0ae6858304 Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Thu, 28 Mar 2024 10:14:30 +0000 Subject: [PATCH 03/36] ezsat: Fix build for emscripten/wasi --- libs/ezsat/ezcommand.cc | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/libs/ezsat/ezcommand.cc b/libs/ezsat/ezcommand.cc index c2925b647..2040d3c1a 100644 --- a/libs/ezsat/ezcommand.cc +++ b/libs/ezsat/ezcommand.cc @@ -9,6 +9,7 @@ ezSATCommand::~ezSATCommand() {} bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) { +#if !defined(YOSYS_DISABLE_SPAWN) const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX"); const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str()); const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str()); @@ -81,4 +82,7 @@ bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector< modelValues[i] = (values.at(idx - 1) == refvalue); } return true; +#else + Yosys::log_error("SAT solver command not available in this build!\n"); +#endif } \ No newline at end of file From d2b6bd00b1eb73d1d800544fcd16e21050f35a80 Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Thu, 28 Mar 2024 17:25:19 +0000 Subject: [PATCH 04/36] ezsat: Rename files and class for ezCmdlineSat --- Makefile | 4 ++-- libs/ezsat/{ezcommand.cc => ezcmdline.cc} | 10 +++++----- libs/ezsat/{ezcommand.h => ezcmdline.h} | 6 +++--- 3 files changed, 10 insertions(+), 10 deletions(-) rename libs/ezsat/{ezcommand.cc => ezcmdline.cc} (91%) rename libs/ezsat/{ezcommand.h => ezcmdline.h} (92%) diff --git a/Makefile b/Makefile index afe559712..0fe20288b 100644 --- a/Makefile +++ b/Makefile @@ -638,7 +638,7 @@ $(eval $(call add_include_file,kernel/yosys_common.h)) $(eval $(call add_include_file,kernel/yw.h)) $(eval $(call add_include_file,libs/ezsat/ezsat.h)) $(eval $(call add_include_file,libs/ezsat/ezminisat.h)) -$(eval $(call add_include_file,libs/ezsat/ezcommand.h)) +$(eval $(call add_include_file,libs/ezsat/ezcmdline.h)) ifeq ($(ENABLE_ZLIB),1) $(eval $(call add_include_file,libs/fst/fstapi.h)) endif @@ -684,7 +684,7 @@ OBJS += libs/json11/json11.o OBJS += libs/ezsat/ezsat.o OBJS += libs/ezsat/ezminisat.o -OBJS += libs/ezsat/ezcommand.o +OBJS += libs/ezsat/ezcmdline.o OBJS += libs/minisat/Options.o OBJS += libs/minisat/SimpSolver.o diff --git a/libs/ezsat/ezcommand.cc b/libs/ezsat/ezcmdline.cc similarity index 91% rename from libs/ezsat/ezcommand.cc rename to libs/ezsat/ezcmdline.cc index 2040d3c1a..1b5278fab 100644 --- a/libs/ezsat/ezcommand.cc +++ b/libs/ezsat/ezcmdline.cc @@ -1,13 +1,13 @@ -#include "ezcommand.h" +#include "ezcmdline.h" #include "../../kernel/yosys.h" -ezSATCommand::ezSATCommand(const std::string &cmd) : command(cmd) {} +ezCmdlineSAT::ezCmdlineSAT(const std::string &cmd) : command(cmd) {} -ezSATCommand::~ezSATCommand() {} +ezCmdlineSAT::~ezCmdlineSAT() {} -bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) +bool ezCmdlineSAT::solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) { #if !defined(YOSYS_DISABLE_SPAWN) const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX"); @@ -85,4 +85,4 @@ bool ezSATCommand::solver(const std::vector &modelExpressions, std::vector< #else Yosys::log_error("SAT solver command not available in this build!\n"); #endif -} \ No newline at end of file +} diff --git a/libs/ezsat/ezcommand.h b/libs/ezsat/ezcmdline.h similarity index 92% rename from libs/ezsat/ezcommand.h rename to libs/ezsat/ezcmdline.h index a0e3de4ed..8ec8c7043 100644 --- a/libs/ezsat/ezcommand.h +++ b/libs/ezsat/ezcmdline.h @@ -22,14 +22,14 @@ #include "ezsat.h" -class ezSATCommand : public ezSAT +class ezCmdlineSAT : public ezSAT { private: std::string command; public: - ezSATCommand(const std::string &cmd); - virtual ~ezSATCommand(); + ezCmdlineSAT(const std::string &cmd); + virtual ~ezCmdlineSAT(); bool solver(const std::vector &modelExpressions, std::vector &modelValues, const std::vector &assumptions) override; }; From 979b673f206bb92e2f76b0c59afe27741b516717 Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Tue, 9 Apr 2024 15:56:36 +0100 Subject: [PATCH 05/36] ezsat: Fix handling of error codes --- libs/ezsat/ezcmdline.cc | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/libs/ezsat/ezcmdline.cc b/libs/ezsat/ezcmdline.cc index 1b5278fab..dddec1067 100644 --- a/libs/ezsat/ezcmdline.cc +++ b/libs/ezsat/ezcmdline.cc @@ -58,7 +58,8 @@ bool ezCmdlineSAT::solver(const std::vector &modelExpressions, std::vector< } } }; - if (Yosys::run_command(sat_command, line_callback) != 0) { + int return_code = Yosys::run_command(sat_command, line_callback); + if (return_code != 0 && return_code != 10 && return_code != 20) { Yosys::log_cmd_error("Shell command failed!\n"); } From 0f6ef777750e9c537d71b37a1698c08d38add2b7 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 20 Jan 2026 09:28:00 -0800 Subject: [PATCH 06/36] Add test for ezCmdlineSAT --- tests/various/.gitignore | 2 + tests/various/ezcmdline_dummy_solver | 61 ++++++++++++++++++++++++++++ tests/various/ezcmdline_plugin.cc | 53 ++++++++++++++++++++++++ tests/various/ezcmdline_plugin.sh | 8 ++++ 4 files changed, 124 insertions(+) create mode 100755 tests/various/ezcmdline_dummy_solver create mode 100644 tests/various/ezcmdline_plugin.cc create mode 100644 tests/various/ezcmdline_plugin.sh diff --git a/tests/various/.gitignore b/tests/various/.gitignore index e116179ae..9296a04c0 100644 --- a/tests/various/.gitignore +++ b/tests/various/.gitignore @@ -4,6 +4,8 @@ /plugin.so /plugin_search /plugin.so.dSYM +/ezcmdline_plugin.so +/ezcmdline_plugin.so.dSYM /temp /smtlib2_module.smt2 /smtlib2_module-filtered.smt2 diff --git a/tests/various/ezcmdline_dummy_solver b/tests/various/ezcmdline_dummy_solver new file mode 100755 index 000000000..db5b21b8e --- /dev/null +++ b/tests/various/ezcmdline_dummy_solver @@ -0,0 +1,61 @@ +#!/bin/sh +# Dummy SAT solver for ezCmdlineSAT tests. +# Accepts exactly two CNF shapes: +# - SAT: p cnf 1 1; clause: "1 0" -> exits 10 with v 1 +# - UNSAT: p cnf 1 2; clauses: "1 0" and "-1 0" -> exits 20 +set -e + +if [ "$#" -ne 1 ]; then + echo "usage: $0 " >&2 + exit 1 +fi + +awk ' +BEGIN { + vars = 0; + clauses = 0; + clause_count = 0; + clause_data = ""; + current = ""; +} +$1 == "c" { + next; +} +$1 == "p" && $2 == "cnf" { + vars = $3; + clauses = $4; + next; +} +{ + for (i = 1; i <= NF; i++) { + lit = $i; + if (lit == 0) { + clause_count++; + if (clause_data != "") + clause_data = clause_data ";" current; + else + clause_data = current; + current = ""; + } else { + if (current == "") + current = lit; + else + current = current "," lit; + } + } +} +END { + if (vars == 1 && clause_count == 1 && clause_data == "1") { + print "s SATISFIABLE"; + print "v 1 0"; + exit 10; + } + if (vars == 1 && clause_count == 2 && clause_data == "1;-1") { + print "s UNSATISFIABLE"; + exit 20; + } + print "c unexpected CNF for dummy solver"; + print "c vars=" vars " header_clauses=" clauses " parsed_clauses=" clause_count " data=" clause_data; + exit 1; +} +' "$1" diff --git a/tests/various/ezcmdline_plugin.cc b/tests/various/ezcmdline_plugin.cc new file mode 100644 index 000000000..b775829b3 --- /dev/null +++ b/tests/various/ezcmdline_plugin.cc @@ -0,0 +1,53 @@ +#include "kernel/yosys.h" +#include "libs/ezsat/ezcmdline.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct EzCmdlineTestPass : public Pass { + EzCmdlineTestPass() : Pass("ezcmdline_test", "smoke-test ezCmdlineSAT") { } + void execute(std::vector args, RTLIL::Design *design) override + { + std::string cmd; + size_t argidx = 1; + + while (argidx < args.size()) { + if (args[argidx] == "-cmd" && argidx + 1 < args.size()) { + cmd = args[argidx + 1]; + argidx += 2; + continue; + } + break; + } + + extra_args(args, argidx, design); + + if (cmd.empty()) + log_error("Missing -cmd argument.\n"); + + ezCmdlineSAT sat(cmd); + sat.non_incremental(); + + // assume("A") adds a permanent CNF clause "A". + sat.assume(sat.VAR("A")); + + std::vector model_expressions; + std::vector model_values; + model_expressions.push_back(sat.VAR("A")); + + // Expect SAT with A=true. + if (!sat.solve(model_expressions, model_values)) + log_error("ezCmdlineSAT SAT case failed.\n"); + if (model_values.size() != 1 || !model_values[0]) + log_error("ezCmdlineSAT SAT model mismatch.\n"); + + // Passing NOT("A") here adds a temporary unit clause for this solve call, + // so the solver sees A && !A and must return UNSAT. + if (sat.solve(model_expressions, model_values, sat.NOT("A"))) + log_error("ezCmdlineSAT UNSAT case failed.\n"); + + log("ezcmdline_test passed!\n"); + } +} EzCmdlineTestPass; + +PRIVATE_NAMESPACE_END diff --git a/tests/various/ezcmdline_plugin.sh b/tests/various/ezcmdline_plugin.sh new file mode 100644 index 000000000..cc1ed4bc9 --- /dev/null +++ b/tests/various/ezcmdline_plugin.sh @@ -0,0 +1,8 @@ +set -e + +DIR=$(cd "$(dirname "$0")" && pwd) +BASEDIR=$(cd "$DIR/../.." && pwd) +rm -f "$DIR/ezcmdline_plugin.so" +chmod +x "$DIR/ezcmdline_dummy_solver" +"$BASEDIR/yosys-config" --build "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc" +"$BASEDIR/yosys" -m "$DIR/ezcmdline_plugin.so" -p "ezcmdline_test -cmd $DIR/ezcmdline_dummy_solver" | grep -q "ezcmdline_test passed!" From bd9dbea4eac201c4fee2e93785e357c1b837c5e3 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 20 Jan 2026 10:07:44 -0800 Subject: [PATCH 07/36] Add -I --- tests/various/ezcmdline_plugin.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/various/ezcmdline_plugin.sh b/tests/various/ezcmdline_plugin.sh index cc1ed4bc9..58dc7d9c8 100644 --- a/tests/various/ezcmdline_plugin.sh +++ b/tests/various/ezcmdline_plugin.sh @@ -4,5 +4,5 @@ DIR=$(cd "$(dirname "$0")" && pwd) BASEDIR=$(cd "$DIR/../.." && pwd) rm -f "$DIR/ezcmdline_plugin.so" chmod +x "$DIR/ezcmdline_dummy_solver" -"$BASEDIR/yosys-config" --build "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc" +"$BASEDIR/yosys-config" --build "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc" -I"$BASEDIR" "$BASEDIR/yosys" -m "$DIR/ezcmdline_plugin.so" -p "ezcmdline_test -cmd $DIR/ezcmdline_dummy_solver" | grep -q "ezcmdline_test passed!" From 9ed56ac72c3d391119174a9f9029a5b71caf8e70 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 20 Jan 2026 10:44:47 -0800 Subject: [PATCH 08/36] Mimic pattern of how other tests build plugins Seems like using --build isn't supported in CI --- tests/various/ezcmdline_plugin.sh | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/tests/various/ezcmdline_plugin.sh b/tests/various/ezcmdline_plugin.sh index 58dc7d9c8..cad0475a8 100644 --- a/tests/various/ezcmdline_plugin.sh +++ b/tests/various/ezcmdline_plugin.sh @@ -4,5 +4,9 @@ DIR=$(cd "$(dirname "$0")" && pwd) BASEDIR=$(cd "$DIR/../.." && pwd) rm -f "$DIR/ezcmdline_plugin.so" chmod +x "$DIR/ezcmdline_dummy_solver" -"$BASEDIR/yosys-config" --build "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc" -I"$BASEDIR" +CXXFLAGS=$("$BASEDIR/yosys-config" --cxxflags) +DATDIR=$("$BASEDIR/yosys-config" --datdir) +DATDIR=${DATDIR//\//\\\/} +CXXFLAGS=${CXXFLAGS//$DATDIR/..\/..\/share} +"$BASEDIR/yosys-config" --exec --cxx ${CXXFLAGS} -I"$BASEDIR" --ldflags -shared -o "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc" "$BASEDIR/yosys" -m "$DIR/ezcmdline_plugin.so" -p "ezcmdline_test -cmd $DIR/ezcmdline_dummy_solver" | grep -q "ezcmdline_test passed!" From 808ec8c04b37e0e6c73b8873d4051c19dc41fa25 Mon Sep 17 00:00:00 2001 From: Maxim Kudinov Date: Sun, 25 Jan 2026 22:10:08 +0300 Subject: [PATCH 09/36] gowin: synth_gowin: Add MULT inference for GW1N and GW2A --- techlibs/gowin/Makefile.inc | 1 + techlibs/gowin/dsp_map.v | 70 +++++++++++++++++++++++++++++++++++ techlibs/gowin/synth_gowin.cc | 44 +++++++++++++++++++++- 3 files changed, 114 insertions(+), 1 deletion(-) create mode 100644 techlibs/gowin/dsp_map.v diff --git a/techlibs/gowin/Makefile.inc b/techlibs/gowin/Makefile.inc index df1b79317..0744b1389 100644 --- a/techlibs/gowin/Makefile.inc +++ b/techlibs/gowin/Makefile.inc @@ -12,3 +12,4 @@ $(eval $(call add_share_file,share/gowin,techlibs/gowin/brams_map_gw5a.v)) $(eval $(call add_share_file,share/gowin,techlibs/gowin/brams.txt)) $(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams_map.v)) $(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams.txt)) +$(eval $(call add_share_file,share/gowin,techlibs/gowin/dsp_map.v)) diff --git a/techlibs/gowin/dsp_map.v b/techlibs/gowin/dsp_map.v new file mode 100644 index 000000000..dfde0b6a1 --- /dev/null +++ b/techlibs/gowin/dsp_map.v @@ -0,0 +1,70 @@ +module \$__MUL9X9 (input [8:0] A, input [8:0] B, output [17:0] Y); + + parameter A_WIDTH = 9; + parameter B_WIDTH = 9; + parameter Y_WIDTH = 18; + parameter A_SIGNED = 0; + parameter B_SIGNED = 0; + + MULT9X9 __TECHMAP_REPLACE__ ( + .CLK(1'b0), + .CE(1'b0), + .RESET(1'b0), + .A(A), + .SIA({A_WIDTH{1'b0}}), + .ASEL(1'b0), + .ASIGN(A_SIGNED ? 1'b1 : 1'b0), + .B(B), + .SIB({B_WIDTH{1'b0}}), + .BSEL(1'b0), + .BSIGN(B_SIGNED ? 1'b1 : 1'b0), + .DOUT(Y) + ); + +endmodule + +module \$__MUL18X18 (input [17:0] A, input [17:0] B, output [35:0] Y); + + parameter A_WIDTH = 18; + parameter B_WIDTH = 18; + parameter Y_WIDTH = 36; + parameter A_SIGNED = 0; + parameter B_SIGNED = 0; + + MULT18X18 __TECHMAP_REPLACE__ ( + .CLK(1'b0), + .CE(1'b0), + .RESET(1'b0), + .A(A), + .SIA({A_WIDTH{1'b0}}), + .ASEL(1'b0), + .ASIGN(A_SIGNED ? 1'b1 : 1'b0), + .B(B), + .SIB({B_WIDTH{1'b0}}), + .BSEL(1'b0), + .BSIGN(B_SIGNED ? 1'b1 : 1'b0), + .DOUT(Y) + ); + +endmodule + +module \$__MUL36X36 (input [35:0] A, input [35:0] B, output [71:0] Y); + + parameter A_WIDTH = 36; + parameter B_WIDTH = 36; + parameter Y_WIDTH = 72; + parameter A_SIGNED = 0; + parameter B_SIGNED = 0; + + MULT36X36 __TECHMAP_REPLACE__ ( + .CLK(1'b0), + .RESET(1'b0), + .CE(1'b0), + .A(A), + .ASIGN(A_SIGNED ? 1'b1 : 1'b0), + .B(B), + .BSIGN(B_SIGNED ? 1'b1 : 1'b0), + .DOUT(Y) + ); + +endmodule diff --git a/techlibs/gowin/synth_gowin.cc b/techlibs/gowin/synth_gowin.cc index b9902659c..9cc213945 100644 --- a/techlibs/gowin/synth_gowin.cc +++ b/techlibs/gowin/synth_gowin.cc @@ -29,6 +29,21 @@ struct SynthGowinPass : public ScriptPass { SynthGowinPass() : ScriptPass("synth_gowin", "synthesis for Gowin FPGAs") { } + struct DSPRule { + int a_maxwidth; + int b_maxwidth; + int a_minwidth; + int b_minwidth; + std::string prim; + }; + + const std::vector dsp_rules = { + {36, 36, 22, 22, "$__MUL36X36"}, + {18, 18, 10, 4, "$__MUL18X18"}, + {18, 18, 4, 10, "$__MUL18X18"}, + {9, 9, 4, 4, "$__MUL9X9"}, + }; + void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| @@ -249,7 +264,34 @@ struct SynthGowinPass : public ScriptPass if (check_label("coarse")) { - run("synth -run coarse" + no_rw_check_opt); + run("proc"); + run("opt_expr"); + run("opt_clean"); + run("check"); + run("opt -nodffe -nosdff"); + run("fsm"); + run("opt"); + run("wreduce"); + run("peepopt"); + run("opt_clean"); + run("share"); + + if (help_mode) { + run("techmap -map +/mul2dsp.v [...]", "(if -family gw1n or gw2a)"); + run("techmap -map +/gowin/dsp_map.v", "(if -family gw1n or gw2a)"); + } else if (family == "gw1n" || family == "gw2a") { + for (const auto &rule : dsp_rules) { + run(stringf("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=%d -D DSP_B_MAXWIDTH=%d -D DSP_A_MINWIDTH=%d -D DSP_B_MINWIDTH=%d -D DSP_NAME=%s", + rule.a_maxwidth, rule.b_maxwidth, rule.a_minwidth, rule.b_minwidth, rule.prim)); + run("chtype -set $mul t:$__soft_mul"); + } + run("techmap -map +/gowin/dsp_map.v"); + } + + run("alumacc"); + run("opt"); + run("memory -nomap" + no_rw_check_opt); + run("opt_clean"); } if (check_label("map_ram")) From 44afd4bbdd2094144fa178f3bbfb4f92c135850c Mon Sep 17 00:00:00 2001 From: Jeppe Johansen Date: Wed, 24 Aug 2022 18:31:45 +0200 Subject: [PATCH 10/36] Add support for subtraction in preadder --- techlibs/xilinx/xilinx_dsp.cc | 20 +++++++++++++------- techlibs/xilinx/xilinx_dsp.pmg | 32 +++++++++++++++++++++++++++++++- 2 files changed, 44 insertions(+), 8 deletions(-) diff --git a/techlibs/xilinx/xilinx_dsp.cc b/techlibs/xilinx/xilinx_dsp.cc index 22e6bce5b..194b9ac10 100644 --- a/techlibs/xilinx/xilinx_dsp.cc +++ b/techlibs/xilinx/xilinx_dsp.cc @@ -263,6 +263,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm) log("Analysing %s.%s for Xilinx DSP packing.\n", log_id(pm.module), log_id(st.dsp)); log_debug("preAdd: %s\n", log_id(st.preAdd, "--")); + log_debug("preSub: %s\n", log_id(st.preSub, "--")); log_debug("ffAD: %s\n", log_id(st.ffAD, "--")); log_debug("ffA2: %s\n", log_id(st.ffA2, "--")); log_debug("ffA1: %s\n", log_id(st.ffA1, "--")); @@ -278,17 +279,22 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm) Cell *cell = st.dsp; - if (st.preAdd) { - log(" preadder %s (%s)\n", log_id(st.preAdd), log_id(st.preAdd->type)); - bool A_SIGNED = st.preAdd->getParam(ID::A_SIGNED).as_bool(); - bool D_SIGNED = st.preAdd->getParam(ID::B_SIGNED).as_bool(); - if (st.sigA == st.preAdd->getPort(ID::B)) + if (st.preAdd || st.preSub) { + Cell* preAdder = st.preAdd ? st.preAdd : st.preSub; + + log(" preadder %s (%s)\n", log_id(preAdder), log_id(preAdder->type)); + bool A_SIGNED = preAdder->getParam(ID::A_SIGNED).as_bool(); + bool D_SIGNED = preAdder->getParam(ID::B_SIGNED).as_bool(); + if (st.sigA == preAdder->getPort(ID::B)) std::swap(A_SIGNED, D_SIGNED); st.sigA.extend_u0(30, A_SIGNED); st.sigD.extend_u0(25, D_SIGNED); cell->setPort(ID::A, st.sigA); cell->setPort(ID::D, st.sigD); - cell->setPort(ID(INMODE), Const::from_string("00100")); + if (preAdder->type == ID($add)) + cell->setPort(ID(INMODE), Const::from_string("00100")); + else + cell->setPort(ID(INMODE), Const::from_string("01100")); if (st.ffAD) { if (st.ffAD->type.in(ID($dffe), ID($sdffe))) { @@ -303,7 +309,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm) cell->setParam(ID(USE_DPORT), Const("TRUE")); - pm.autoremove(st.preAdd); + pm.autoremove(preAdder); } if (st.postAdd) { log(" postadder %s (%s)\n", log_id(st.postAdd), log_id(st.postAdd->type)); diff --git a/techlibs/xilinx/xilinx_dsp.pmg b/techlibs/xilinx/xilinx_dsp.pmg index ef0157621..6ec891290 100644 --- a/techlibs/xilinx/xilinx_dsp.pmg +++ b/techlibs/xilinx/xilinx_dsp.pmg @@ -6,6 +6,8 @@ // If ADREG matched, treat 'A' input as input of ADREG // ( 3) Match the driver of the 'A' and 'D' inputs for a possible $add cell // (pre-adder) +// (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell +// (pre-adder) // ( 4) If pre-adder was present, find match 'A' input for A2REG // If pre-adder was not present, move ADREG to A2REG // If A2REG, then match 'A' input for A1REG @@ -152,13 +154,41 @@ code sigA sigD } endcode +// (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell +// (pre-adder) +match preSub + if sigD.empty() || sigD.is_fully_zero() + // Ensure that preAdder not already used + if param(dsp, \USE_DPORT).decode_string() == "FALSE" + if port(dsp, \INMODE, Const(0, 5)).is_fully_zero() + + select preSub->type.in($sub) + // Output has to be 25 bits or less + select GetSize(port(preSub, \Y)) <= 25 + select nusers(port(preSub, \Y)) == 2 + // D port has to be 25 bits or less + select GetSize(port(preSub, \A)) <= 25 + // A port has to be 30 bits or less + select GetSize(port(preSub, \B)) <= 30 + index port(preSub, \Y) === sigA + + optional +endmatch + +code sigA sigD + if (preSub) { + sigD = port(preSub, \A); + sigA = port(preSub, \B); + } +endcode + // (4) If pre-adder was present, find match 'A' input for A2REG // If pre-adder was not present, move ADREG to A2REG // Then match 'A' input for A1REG code argQ ffAD sigA clock ffA2 ffA1 // Only search for ffA2 if there was a pre-adder // (otherwise ffA2 would have been matched as ffAD) - if (preAdd) { + if (preAdd || preSub) { if (param(dsp, \AREG).as_int() == 0) { argQ = sigA; subpattern(in_dffe); From 3f01d7a33ae27df8f1d120dce082b02e526e8a0c Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 3 Feb 2026 14:41:08 -0800 Subject: [PATCH 11/36] Add test --- tests/arch/xilinx/dsp_preadder_sub.ys | 41 +++++++++++++++++++++++++++ 1 file changed, 41 insertions(+) create mode 100644 tests/arch/xilinx/dsp_preadder_sub.ys diff --git a/tests/arch/xilinx/dsp_preadder_sub.ys b/tests/arch/xilinx/dsp_preadder_sub.ys new file mode 100644 index 000000000..04e5e9da0 --- /dev/null +++ b/tests/arch/xilinx/dsp_preadder_sub.ys @@ -0,0 +1,41 @@ +read_verilog < Date: Sat, 7 Feb 2026 12:12:13 +1300 Subject: [PATCH 12/36] Sanitize ABC global and per-run temporary directory names in logs --- passes/techmap/abc.cc | 56 ++++++++++++---------- tests/techmap/abc_temp_dir_sanitization.ys | 13 +++++ 2 files changed, 45 insertions(+), 24 deletions(-) create mode 100644 tests/techmap/abc_temp_dir_sanitization.ys diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index f7fa095a0..6e5b1fba8 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -285,7 +285,7 @@ using AbcSigMap = SigValMap; struct RunAbcState { const AbcConfig &config; - std::string tempdir_name; + std::string per_run_tempdir_name; std::vector signal_list; bool did_run = false; bool err = false; @@ -836,16 +836,23 @@ std::string fold_abc_cmd(std::string str) return new_str; } -std::string replace_tempdir(std::string text, std::string tempdir_name, bool show_tempdir) +std::string replace_tempdir(std::string text, std::string_view global_tempdir_name, std::string_view per_run_tempdir_name, bool show_tempdir) { if (show_tempdir) return text; while (1) { - size_t pos = text.find(tempdir_name); + size_t pos = text.find(global_tempdir_name); if (pos == std::string::npos) break; - text = text.substr(0, pos) + "" + text.substr(pos + GetSize(tempdir_name)); + text = text.substr(0, pos) + "" + text.substr(pos + GetSize(global_tempdir_name)); + } + + while (1) { + size_t pos = text.find(per_run_tempdir_name); + if (pos == std::string::npos) + break; + text = text.substr(0, pos) + "" + text.substr(pos + GetSize(per_run_tempdir_name)); } std::string selfdir_name = proc_self_dirname(); @@ -867,11 +874,12 @@ struct abc_output_filter bool got_cr; int escape_seq_state; std::string linebuf; - std::string tempdir_name; + std::string global_tempdir_name; + std::string per_run_tempdir_name; bool show_tempdir; - abc_output_filter(RunAbcState& state, std::string tempdir_name, bool show_tempdir) - : state(state), tempdir_name(tempdir_name), show_tempdir(show_tempdir) + abc_output_filter(RunAbcState& state, std::string global_tempdir_name, std::string per_run_tempdir_name, bool show_tempdir) + : state(state), global_tempdir_name(global_tempdir_name), per_run_tempdir_name(per_run_tempdir_name), show_tempdir(show_tempdir) { got_cr = false; escape_seq_state = 0; @@ -898,7 +906,7 @@ struct abc_output_filter return; } if (ch == '\n') { - state.logs.log("ABC: %s\n", replace_tempdir(linebuf, tempdir_name, show_tempdir)); + state.logs.log("ABC: %s\n", replace_tempdir(linebuf, global_tempdir_name, per_run_tempdir_name, show_tempdir)); got_cr = false, linebuf.clear(); return; } @@ -999,15 +1007,15 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module const AbcConfig &config = run_abc.config; if (config.cleanup) - run_abc.tempdir_name = get_base_tmpdir() + "/"; + run_abc.per_run_tempdir_name = get_base_tmpdir() + "/"; else - run_abc.tempdir_name = "_tmp_"; - run_abc.tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX"; - run_abc.tempdir_name = make_temp_dir(run_abc.tempdir_name); + run_abc.per_run_tempdir_name = "_tmp_"; + run_abc.per_run_tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX"; + run_abc.per_run_tempdir_name = make_temp_dir(run_abc.per_run_tempdir_name); log_header(design, "Extracting gate netlist of module `%s' to `%s/input.blif'..\n", - module->name.c_str(), replace_tempdir(run_abc.tempdir_name, run_abc.tempdir_name, config.show_tempdir).c_str()); + module->name.c_str(), replace_tempdir(run_abc.per_run_tempdir_name, config.global_tempdir_name, run_abc.per_run_tempdir_name, config.show_tempdir).c_str()); - std::string abc_script = stringf("read_blif \"%s/input.blif\"; ", run_abc.tempdir_name); + std::string abc_script = stringf("read_blif \"%s/input.blif\"; ", run_abc.per_run_tempdir_name); if (!config.liberty_files.empty() || !config.genlib_files.empty()) { std::string dont_use_args; @@ -1073,8 +1081,8 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos)) abc_script = abc_script.substr(0, pos) + config.lutin_shared + abc_script.substr(pos+3); if (config.abc_dress) - abc_script += stringf("; dress \"%s/input.blif\"", run_abc.tempdir_name); - abc_script += stringf("; write_blif %s/output.blif", run_abc.tempdir_name); + abc_script += stringf("; dress \"%s/input.blif\"", run_abc.per_run_tempdir_name); + abc_script += stringf("; write_blif %s/output.blif", run_abc.per_run_tempdir_name); abc_script = add_echos_to_abc_cmd(abc_script); #if defined(REUSE_YOSYS_ABC_PROCESSES) if (config.is_yosys_abc()) @@ -1085,7 +1093,7 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module if (abc_script[i] == ';' && abc_script[i+1] == ' ') abc_script[i+1] = '\n'; - std::string buffer = stringf("%s/abc.script", run_abc.tempdir_name); + std::string buffer = stringf("%s/abc.script", run_abc.per_run_tempdir_name); FILE *f = fopen(buffer.c_str(), "wt"); if (f == nullptr) log_error("Opening %s for writing failed: %s\n", buffer, strerror(errno)); @@ -1220,7 +1228,7 @@ void RunAbcState::run(ConcurrentStack &process_pool) void RunAbcState::run(ConcurrentStack &) #endif { - std::string buffer = stringf("%s/input.blif", tempdir_name); + std::string buffer = stringf("%s/input.blif", per_run_tempdir_name); FILE *f = fopen(buffer.c_str(), "wt"); if (f == nullptr) { logs.log("Opening %s for writing failed: %s\n", buffer, strerror(errno)); @@ -1348,14 +1356,14 @@ void RunAbcState::run(ConcurrentStack &) return; } int ret; - std::string tmp_script_name = stringf("%s/abc.script", tempdir_name); + std::string tmp_script_name = stringf("%s/abc.script", per_run_tempdir_name); do { - logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, tempdir_name, config.show_tempdir)); + logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir)); errno = 0; - abc_output_filter filt(*this, tempdir_name, config.show_tempdir); + abc_output_filter filt(*this, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir); #ifdef YOSYS_LINK_ABC - string temp_stdouterr_name = stringf("%s/stdouterr.txt", tempdir_name); + string temp_stdouterr_name = stringf("%s/stdouterr.txt", per_run_tempdir_name); FILE *temp_stdouterr_w = fopen(temp_stdouterr_name.c_str(), "w"); if (temp_stdouterr_w == NULL) log_error("ABC: cannot open a temporary file for output redirection"); @@ -1502,7 +1510,7 @@ void AbcModuleState::extract(AbcSigMap &assign_map, RTLIL::Design *design, RTLIL return; } - std::string buffer = stringf("%s/%s", run_abc.tempdir_name, "output.blif"); + std::string buffer = stringf("%s/%s", run_abc.per_run_tempdir_name, "output.blif"); std::ifstream ifs; ifs.open(buffer); if (ifs.fail()) @@ -1789,7 +1797,7 @@ void AbcModuleState::finish() if (run_abc.config.cleanup) { log("Removing temp directory.\n"); - remove_directory(run_abc.tempdir_name); + remove_directory(run_abc.per_run_tempdir_name); } log_pop(); } diff --git a/tests/techmap/abc_temp_dir_sanitization.ys b/tests/techmap/abc_temp_dir_sanitization.ys new file mode 100644 index 000000000..ed87ff980 --- /dev/null +++ b/tests/techmap/abc_temp_dir_sanitization.ys @@ -0,0 +1,13 @@ +read_verilog < Date: Fri, 6 Feb 2026 17:26:08 -0800 Subject: [PATCH 13/36] Typo --- libs/ezsat/ezcmdline.cc | 2 +- libs/ezsat/ezminisat.cc | 4 ++-- libs/ezsat/ezsat.cc | 2 +- libs/ezsat/ezsat.h | 6 +++--- passes/sat/sat.cc | 4 ++-- 5 files changed, 9 insertions(+), 9 deletions(-) diff --git a/libs/ezsat/ezcmdline.cc b/libs/ezsat/ezcmdline.cc index dddec1067..2eef1b06d 100644 --- a/libs/ezsat/ezcmdline.cc +++ b/libs/ezsat/ezcmdline.cc @@ -67,7 +67,7 @@ bool ezCmdlineSAT::solver(const std::vector &modelExpressions, std::vector< modelValues.resize(modelIdx.size()); if (!status_sat && !status_unsat) { - solverTimoutStatus = true; + solverTimeoutStatus = true; } if (!status_sat) { return false; diff --git a/libs/ezsat/ezminisat.cc b/libs/ezsat/ezminisat.cc index 30df625cb..1f4b8855f 100644 --- a/libs/ezsat/ezminisat.cc +++ b/libs/ezsat/ezminisat.cc @@ -103,7 +103,7 @@ bool ezMiniSAT::solver(const std::vector &modelExpressions, std::vector 0) { if (alarmHandlerTimeout == 0) - solverTimoutStatus = true; + solverTimeoutStatus = true; alarm(0); sigaction(SIGALRM, &old_sig_action, NULL); alarm(old_alarm_timeout); diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index fbdfc20f6..3e63d3e84 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -54,7 +54,7 @@ ezSAT::ezSAT() cnfClausesCount = 0; solverTimeout = 0; - solverTimoutStatus = false; + solverTimeoutStatus = false; literal("CONST_TRUE"); literal("CONST_FALSE"); diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h index 507708cb2..445c8edba 100644 --- a/libs/ezsat/ezsat.h +++ b/libs/ezsat/ezsat.h @@ -78,7 +78,7 @@ protected: public: int solverTimeout; - bool solverTimoutStatus; + bool solverTimeoutStatus; ezSAT(); virtual ~ezSAT(); @@ -153,8 +153,8 @@ public: solverTimeout = newTimeoutSeconds; } - bool getSolverTimoutStatus() { - return solverTimoutStatus; + bool getSolverTimeoutStatus() { + return solverTimeoutStatus; } // manage CNF (usually only accessed by SAT solvers) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 90b85d709..bb7b9ee29 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -441,7 +441,7 @@ struct SatHelper log_assert(gotTimeout == false); ez->setSolverTimeout(timeout); bool success = ez->solve(modelExpressions, modelValues, assumptions); - if (ez->getSolverTimoutStatus()) + if (ez->getSolverTimeoutStatus()) gotTimeout = true; return success; } @@ -451,7 +451,7 @@ struct SatHelper log_assert(gotTimeout == false); ez->setSolverTimeout(timeout); bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f); - if (ez->getSolverTimoutStatus()) + if (ez->getSolverTimeoutStatus()) gotTimeout = true; return success; } From 2bb352a86171ac2bb36d3baa9ac3fb3046a521f5 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Fri, 6 Feb 2026 17:45:00 -0800 Subject: [PATCH 14/36] Missing newline --- libs/ezsat/ezsat.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 3e63d3e84..69a59c8cd 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -1225,7 +1225,7 @@ ezSATvec ezSAT::vec(const std::vector &vec) void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector> &extraClauses) const { if (cnfConsumed) { - fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!"); + fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!\n"); abort(); } From b2f9ac4fb5d5a79515b9f905bf76a493b301fad3 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Fri, 6 Feb 2026 18:18:03 -0800 Subject: [PATCH 15/36] Check for dimacs nullptr on file creation+fn call --- libs/ezsat/ezcmdline.cc | 3 +++ libs/ezsat/ezsat.cc | 5 +++++ 2 files changed, 8 insertions(+) diff --git a/libs/ezsat/ezcmdline.cc b/libs/ezsat/ezcmdline.cc index 2eef1b06d..57800591c 100644 --- a/libs/ezsat/ezcmdline.cc +++ b/libs/ezsat/ezcmdline.cc @@ -14,6 +14,9 @@ bool ezCmdlineSAT::solver(const std::vector &modelExpressions, std::vector< const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str()); const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str()); FILE *dimacs = fopen(cnf_filename.c_str(), "w"); + if (dimacs == nullptr) { + Yosys::log_cmd_error("Failed to create CNF file `%s`.\n", cnf_filename.c_str()); + } std::vector modelIdx; for (auto id : modelExpressions) diff --git a/libs/ezsat/ezsat.cc b/libs/ezsat/ezsat.cc index 69a59c8cd..8e3114705 100644 --- a/libs/ezsat/ezsat.cc +++ b/libs/ezsat/ezsat.cc @@ -1224,6 +1224,11 @@ ezSATvec ezSAT::vec(const std::vector &vec) void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector> &extraClauses) const { + if (f == nullptr) { + fprintf(stderr, "Usage error: printDIMACS() must not be called with a null FILE pointer\n"); + abort(); + } + if (cnfConsumed) { fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!\n"); abort(); From 1502e233715854c8835563b3f0d26fb7c84f49d3 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Fri, 6 Feb 2026 19:26:32 -0800 Subject: [PATCH 16/36] Set solver from scratchpad or command line --- kernel/satgen.h | 1 + passes/sat/sat.cc | 46 +++++++++++++++++++++++++++++++++++++++++----- 2 files changed, 42 insertions(+), 5 deletions(-) diff --git a/kernel/satgen.h b/kernel/satgen.h index 7815847b3..c53d20fe0 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -59,6 +59,7 @@ struct SatSolver struct ezSatPtr : public std::unique_ptr { ezSatPtr() : unique_ptr(yosys_satsolver->create()) { } + explicit ezSatPtr(SatSolver *solver) : unique_ptr((solver ? solver : yosys_satsolver)->create()) { } }; struct SatGen diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index bb7b9ee29..8a0a45dcf 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -31,6 +31,22 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN +static SatSolver *find_satsolver(const std::string &name) +{ + for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next) + if (solver->name == name) + return solver; + return nullptr; +} + +static std::string list_satsolvers() +{ + std::string result; + for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next) + result += result.empty() ? solver->name : ", " + solver->name; + return result; +} + struct SatHelper { RTLIL::Design *design; @@ -60,8 +76,8 @@ struct SatHelper int max_timestep, timeout; bool gotTimeout; - SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) : - design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap) + SatHelper(RTLIL::Design *design, RTLIL::Module *module, SatSolver *solver, bool enable_undef, bool set_def_formal) : + design(design), module(module), sigmap(module), ct(design), ez(solver), satgen(ez.get(), &sigmap) { this->enable_undef = enable_undef; satgen.model_undef = enable_undef; @@ -1066,6 +1082,10 @@ struct SatPass : public Pass { log(" -timeout \n"); log(" Maximum number of seconds a single SAT instance may take.\n"); log("\n"); + log(" -select-solver \n"); + log(" Select SAT solver implementation for this invocation.\n"); + log(" If not given, uses scratchpad key 'sat.solver' if set, otherwise default.\n"); + log("\n"); log(" -verify\n"); log(" Return an error and stop the synthesis script if the proof fails.\n"); log("\n"); @@ -1097,8 +1117,14 @@ struct SatPass : public Pass { log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n"); + std::string solver_name = design->scratchpad_get_string("sat.solver", ""); + size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { + if (args[argidx] == "-select-solver" && argidx+1 < args.size()) { + solver_name = args[++argidx]; + continue; + } if (args[argidx] == "-all") { loopcount = -1; continue; @@ -1336,6 +1362,14 @@ struct SatPass : public Pass { } extra_args(args, argidx, design); + SatSolver *solver = yosys_satsolver; + if (!solver_name.empty()) { + solver = find_satsolver(solver_name); + if (solver == nullptr) + log_cmd_error("Unknown SAT solver '%s'. Available solvers: %s\n", + solver_name, list_satsolvers()); + } + RTLIL::Module *module = NULL; for (auto mod : design->selected_modules()) { if (module) @@ -1398,13 +1432,15 @@ struct SatPass : public Pass { shows.push_back(wire->name.str()); } + log("Using SAT solver `%s`.\n", solver->name.c_str()); + if (tempinduct) { if (loopcount > 0 || max_undef) log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n"); - SatHelper basecase(design, module, enable_undef, set_def_formal); - SatHelper inductstep(design, module, enable_undef, set_def_formal); + SatHelper basecase(design, module, solver, enable_undef, set_def_formal); + SatHelper inductstep(design, module, solver, enable_undef, set_def_formal); basecase.sets = sets; basecase.set_assumes = set_assumes; @@ -1593,7 +1629,7 @@ struct SatPass : public Pass { if (maxsteps > 0) log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n"); - SatHelper sathelper(design, module, enable_undef, set_def_formal); + SatHelper sathelper(design, module, solver, enable_undef, set_def_formal); sathelper.sets = sets; sathelper.set_assumes = set_assumes; From 6f6fa49d3cac7f2d379a162b0dc6dc3ea49faa54 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 9 Feb 2026 09:05:56 -0800 Subject: [PATCH 17/36] Typo --- passes/cmds/scratchpad.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/cmds/scratchpad.cc b/passes/cmds/scratchpad.cc index f64ce943c..24ab5cfd8 100644 --- a/passes/cmds/scratchpad.cc +++ b/passes/cmds/scratchpad.cc @@ -37,7 +37,7 @@ struct ScratchpadPass : public Pass { log("\n"); log(" scratchpad [options]\n"); log("\n"); - log("This pass allows to read and modify values from the scratchpad of the current\n"); + log("This pass allows reading and modifying values from the scratchpad of the current\n"); log("design. Options:\n"); log("\n"); log(" -get \n"); From b04948a8cdd2f13838f2472b7af4afa1ad516f6f Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 9 Feb 2026 09:38:45 -0800 Subject: [PATCH 18/36] Simplify test --- tests/arch/xilinx/dsp_preadder_sub.ys | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/tests/arch/xilinx/dsp_preadder_sub.ys b/tests/arch/xilinx/dsp_preadder_sub.ys index 04e5e9da0..0e23ac373 100644 --- a/tests/arch/xilinx/dsp_preadder_sub.ys +++ b/tests/arch/xilinx/dsp_preadder_sub.ys @@ -1,23 +1,11 @@ read_verilog < Date: Tue, 10 Feb 2026 00:38:43 +0000 Subject: [PATCH 19/36] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 81f9e0652..d0ca321e3 100644 --- a/Makefile +++ b/Makefile @@ -161,7 +161,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.62+9 +YOSYS_VER := 0.62+14 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2) From a6a07fb39c0f3e79aea7b543ffb2e36a04e887b3 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 00:59:12 +0100 Subject: [PATCH 20/36] Dockerfile: remove --- Dockerfile | 58 ------------------------------------------------------ 1 file changed, 58 deletions(-) delete mode 100644 Dockerfile diff --git a/Dockerfile b/Dockerfile deleted file mode 100644 index 9806696e0..000000000 --- a/Dockerfile +++ /dev/null @@ -1,58 +0,0 @@ -ARG IMAGE="python:3-slim-buster" - -#--- - -FROM $IMAGE AS base - -RUN apt-get update -qq \ - && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ - ca-certificates \ - clang \ - lld \ - curl \ - libffi-dev \ - libreadline-dev \ - tcl-dev \ - graphviz \ - xdot \ - && apt-get autoclean && apt-get clean && apt-get -y autoremove \ - && update-ca-certificates \ - && rm -rf /var/lib/apt/lists - -#--- - -FROM base AS build - -RUN apt-get update -qq \ - && DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \ - bison \ - flex \ - gawk \ - gcc \ - git \ - iverilog \ - pkg-config \ - && apt-get autoclean && apt-get clean && apt-get -y autoremove \ - && rm -rf /var/lib/apt/lists - -COPY . /yosys - -ENV PREFIX /opt/yosys - -RUN cd /yosys \ - && make \ - && make install \ - && make test - -#--- - -FROM base - -COPY --from=build /opt/yosys /opt/yosys - -ENV PATH /opt/yosys/bin:$PATH - -RUN useradd -m yosys -USER yosys - -CMD ["yosys"] From 5a46106a46a739fb4a4a164353349e6fb3077221 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 01:04:50 +0100 Subject: [PATCH 21/36] abc9: remove -liberty --- passes/techmap/abc9.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index 8b61a9299..138fa0aee 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -221,7 +221,7 @@ struct Abc9Pass : public ScriptPass if ((arg == "-exe" || arg == "-script" || arg == "-D" || /*arg == "-S" ||*/ arg == "-lut" || arg == "-luts" || /*arg == "-box" ||*/ arg == "-W" || arg == "-genlib" || - arg == "-constr" || arg == "-dont_use" || arg == "-liberty") && + arg == "-constr" || arg == "-dont_use") && argidx+1 < args.size()) { if (arg == "-lut" || arg == "-luts") lut_mode = true; From c4094e457b5013d64c60342444c7cd204382c3c7 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 11:34:54 +0100 Subject: [PATCH 22/36] abc9: remove -genlib, -constr --- passes/techmap/abc9.cc | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index 138fa0aee..7ed94617e 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -219,9 +219,8 @@ struct Abc9Pass : public ScriptPass for (argidx = 1; argidx < args.size(); argidx++) { std::string arg = args[argidx]; if ((arg == "-exe" || arg == "-script" || arg == "-D" || - /*arg == "-S" ||*/ arg == "-lut" || arg == "-luts" || - /*arg == "-box" ||*/ arg == "-W" || arg == "-genlib" || - arg == "-constr" || arg == "-dont_use") && + arg == "-lut" || arg == "-luts" || + arg == "-W" || arg == "-dont_use") && argidx+1 < args.size()) { if (arg == "-lut" || arg == "-luts") lut_mode = true; From 915912cc761cb5b059bcb823df1646424cf3b42a Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 11:39:09 +0100 Subject: [PATCH 23/36] abc9: remove -dont_use --- passes/techmap/abc9.cc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index 7ed94617e..16df82bb6 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -219,8 +219,7 @@ struct Abc9Pass : public ScriptPass for (argidx = 1; argidx < args.size(); argidx++) { std::string arg = args[argidx]; if ((arg == "-exe" || arg == "-script" || arg == "-D" || - arg == "-lut" || arg == "-luts" || - arg == "-W" || arg == "-dont_use") && + arg == "-lut" || arg == "-luts" || arg == "-W") && argidx+1 < args.size()) { if (arg == "-lut" || arg == "-luts") lut_mode = true; From 12ace45b89035e128ba41b10938ed2665ae30c2a Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Wed, 22 Jun 2022 10:57:46 -0700 Subject: [PATCH 24/36] Support param. default values in JSON FE and SV BE --- abc | 2 +- backends/verilog/verilog_backend.cc | 11 +++++++++++ frontends/json/jsonparse.cc | 3 +++ 3 files changed, 15 insertions(+), 1 deletion(-) diff --git a/abc b/abc index 734f64d5b..799ba6322 160000 --- a/abc +++ b/abc @@ -1 +1 @@ -Subproject commit 734f64d5b907158dc4337ee82b3b74566d74ba08 +Subproject commit 799ba632239b2a4db2bacda81de4e6efdc486b0c diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 3d451117c..b3029b051 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -421,6 +421,14 @@ void dump_attributes(std::ostream &f, std::string indent, dictattributes, "\n", /*modattr=*/false, /*regattr=*/reg_wires.count(wire->name)); @@ -2438,6 +2446,9 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) f << indent + " " << "reg " << id(initial_id) << " = 0;\n"; } + for (auto p : module->parameter_default_values) + dump_parameter(f, indent + " ", p.first, p.second); + // first dump input / output according to their order in module->ports for (auto port : module->ports) dump_wire(f, indent + " ", module->wire(port)); diff --git a/frontends/json/jsonparse.cc b/frontends/json/jsonparse.cc index 743ac5d9e..803931f32 100644 --- a/frontends/json/jsonparse.cc +++ b/frontends/json/jsonparse.cc @@ -302,6 +302,9 @@ void json_import(Design *design, string &modname, JsonNode *node) if (node->data_dict.count("attributes")) json_parse_attr_param(module->attributes, node->data_dict.at("attributes")); + if (node->data_dict.count("parameter_default_values")) + json_parse_attr_param(module->parameter_default_values, node->data_dict.at("parameter_default_values")); + dict signal_bits; if (node->data_dict.count("ports")) From 9ad7aed4a53e3467a89808544a2ac8701c6a5c9f Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 6 Jan 2026 09:37:13 -0800 Subject: [PATCH 25/36] Update backends/verilog/verilog_backend.cc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Marcelina Kościelnicka <236399+mwkmwkmwk@users.noreply.github.com> --- backends/verilog/verilog_backend.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index b3029b051..6284cdf33 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -426,7 +426,7 @@ void dump_parameter(std::ostream &f, std::string indent, RTLIL::IdString id_stri f << stringf("%sparameter %s", indent.c_str(), id(id_string).c_str()); f << stringf(" = "); dump_const(f, parameter); - f << stringf(";\n"); + f << ";\n"; } void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire) From 1ede98797f7eee220cba4fad695e41cdec05684e Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 6 Jan 2026 09:37:21 -0800 Subject: [PATCH 26/36] Update backends/verilog/verilog_backend.cc MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Marcelina Kościelnicka <236399+mwkmwkmwk@users.noreply.github.com> --- backends/verilog/verilog_backend.cc | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 6284cdf33..13f6acec4 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -423,8 +423,7 @@ void dump_attributes(std::ostream &f, std::string indent, dict Date: Tue, 6 Jan 2026 10:38:03 -0800 Subject: [PATCH 27/36] Add tests --- tests/various/json_param_defaults.v | 10 ++++++++++ tests/various/json_param_defaults.ys | 8 ++++++++ 2 files changed, 18 insertions(+) create mode 100644 tests/various/json_param_defaults.v create mode 100644 tests/various/json_param_defaults.ys diff --git a/tests/various/json_param_defaults.v b/tests/various/json_param_defaults.v new file mode 100644 index 000000000..7d3b94a68 --- /dev/null +++ b/tests/various/json_param_defaults.v @@ -0,0 +1,10 @@ +module json_param_defaults #( + parameter WIDTH = 8, + parameter SIGNED = 1 +) ( + input [WIDTH-1:0] a, + output [WIDTH-1:0] y +); + wire [WIDTH-1:0] y_int = a << SIGNED; + assign y = y_int; +endmodule diff --git a/tests/various/json_param_defaults.ys b/tests/various/json_param_defaults.ys new file mode 100644 index 000000000..2624ab884 --- /dev/null +++ b/tests/various/json_param_defaults.ys @@ -0,0 +1,8 @@ +! mkdir -p temp +read_verilog -sv json_param_defaults.v +write_json temp/json_param_defaults.json +design -reset +read_json temp/json_param_defaults.json +write_verilog -noattr temp/json_param_defaults.v +! grep -qF "parameter WIDTH = 32'd8" temp/json_param_defaults.v +! grep -qF "parameter SIGNED = 32'd1" temp/json_param_defaults.v From be9c857e7252751b77bc1548fdbde0f11906a1e8 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Wed, 11 Feb 2026 08:12:38 -0800 Subject: [PATCH 28/36] Fix ABC after merge --- abc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/abc b/abc index 799ba6322..734f64d5b 160000 --- a/abc +++ b/abc @@ -1 +1 @@ -Subproject commit 799ba632239b2a4db2bacda81de4e6efdc486b0c +Subproject commit 734f64d5b907158dc4337ee82b3b74566d74ba08 From a13b5c421108fd1dfe6cd1aff0070777a31c2ec5 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 11 Feb 2026 17:30:08 +0100 Subject: [PATCH 29/36] Update ABC as per 2026-02-11 --- abc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/abc b/abc index 734f64d5b..c18b835ef 160000 --- a/abc +++ b/abc @@ -1 +1 @@ -Subproject commit 734f64d5b907158dc4337ee82b3b74566d74ba08 +Subproject commit c18b835ef140217c84a26ba510f98f69d54dd48e From 7a0774c3bb200d8b5d3278c7c69f9e5d893af43c Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Wed, 11 Feb 2026 08:33:39 -0800 Subject: [PATCH 30/36] Don't dump params by default --- backends/verilog/verilog_backend.cc | 17 ++++++++++++++--- tests/various/json_param_defaults.ys | 2 +- 2 files changed, 15 insertions(+), 4 deletions(-) diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 13f6acec4..73ffcbf3e 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -95,7 +95,8 @@ bool VERILOG_BACKEND::id_is_verilog_escaped(const std::string &str) { PRIVATE_NAMESPACE_BEGIN -bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, noparallelcase; +bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, + noparallelcase, default_params; int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter; dict auto_name_map; std::set reg_wires; @@ -2445,8 +2446,9 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) f << indent + " " << "reg " << id(initial_id) << " = 0;\n"; } - for (auto p : module->parameter_default_values) - dump_parameter(f, indent + " ", p.first, p.second); + if (default_params) + for (auto p : module->parameter_default_values) + dump_parameter(f, indent + " ", p.first, p.second); // first dump input / output according to their order in module->ports for (auto port : module->ports) @@ -2555,6 +2557,10 @@ struct VerilogBackend : public Backend { log(" use 'defparam' statements instead of the Verilog-2001 syntax for\n"); log(" cell parameters.\n"); log("\n"); + log(" -default_params\n"); + log(" emit module parameter declarations from\n"); + log(" parameter_default_values.\n"); + log("\n"); log(" -blackboxes\n"); log(" usually modules with the 'blackbox' attribute are ignored. with\n"); log(" this option set only the modules with the 'blackbox' attribute\n"); @@ -2592,6 +2598,7 @@ struct VerilogBackend : public Backend { siminit = false; simple_lhs = false; noparallelcase = false; + default_params = false; auto_prefix = ""; bool blackboxes = false; @@ -2652,6 +2659,10 @@ struct VerilogBackend : public Backend { defparam = true; continue; } + if (arg == "-defaultparams") { + default_params = true; + continue; + } if (arg == "-decimal") { decimal = true; continue; diff --git a/tests/various/json_param_defaults.ys b/tests/various/json_param_defaults.ys index 2624ab884..45e312de2 100644 --- a/tests/various/json_param_defaults.ys +++ b/tests/various/json_param_defaults.ys @@ -3,6 +3,6 @@ read_verilog -sv json_param_defaults.v write_json temp/json_param_defaults.json design -reset read_json temp/json_param_defaults.json -write_verilog -noattr temp/json_param_defaults.v +write_verilog -noattr -defaultparams temp/json_param_defaults.v ! grep -qF "parameter WIDTH = 32'd8" temp/json_param_defaults.v ! grep -qF "parameter SIGNED = 32'd1" temp/json_param_defaults.v From 1319112913c48983b8bbfb000f43b2715e148b7d Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Thu, 12 Feb 2026 00:32:36 +0000 Subject: [PATCH 31/36] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 5bf66c1a9..02fe61004 100644 --- a/Makefile +++ b/Makefile @@ -161,7 +161,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.62+14 +YOSYS_VER := 0.62+39 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2) From 5ea073d45e3988d6115616f56a82547b5befea7d Mon Sep 17 00:00:00 2001 From: Maxim Kudinov Date: Tue, 3 Feb 2026 19:04:31 +0300 Subject: [PATCH 32/36] gowin: format MULT instances --- techlibs/gowin/dsp_map.v | 76 ++++++++++++++++++++-------------------- 1 file changed, 38 insertions(+), 38 deletions(-) diff --git a/techlibs/gowin/dsp_map.v b/techlibs/gowin/dsp_map.v index dfde0b6a1..f03bcdff0 100644 --- a/techlibs/gowin/dsp_map.v +++ b/techlibs/gowin/dsp_map.v @@ -6,20 +6,20 @@ module \$__MUL9X9 (input [8:0] A, input [8:0] B, output [17:0] Y); parameter A_SIGNED = 0; parameter B_SIGNED = 0; - MULT9X9 __TECHMAP_REPLACE__ ( - .CLK(1'b0), - .CE(1'b0), - .RESET(1'b0), - .A(A), - .SIA({A_WIDTH{1'b0}}), - .ASEL(1'b0), - .ASIGN(A_SIGNED ? 1'b1 : 1'b0), - .B(B), - .SIB({B_WIDTH{1'b0}}), - .BSEL(1'b0), - .BSIGN(B_SIGNED ? 1'b1 : 1'b0), - .DOUT(Y) - ); + MULT9X9 __TECHMAP_REPLACE__ ( + .CLK(1'b0), + .CE(1'b0), + .RESET(1'b0), + .A(A), + .SIA({A_WIDTH{1'b0}}), + .ASEL(1'b0), + .ASIGN(A_SIGNED ? 1'b1 : 1'b0), + .B(B), + .SIB({B_WIDTH{1'b0}}), + .BSEL(1'b0), + .BSIGN(B_SIGNED ? 1'b1 : 1'b0), + .DOUT(Y) + ); endmodule @@ -31,20 +31,20 @@ module \$__MUL18X18 (input [17:0] A, input [17:0] B, output [35:0] Y); parameter A_SIGNED = 0; parameter B_SIGNED = 0; - MULT18X18 __TECHMAP_REPLACE__ ( - .CLK(1'b0), - .CE(1'b0), - .RESET(1'b0), - .A(A), - .SIA({A_WIDTH{1'b0}}), - .ASEL(1'b0), - .ASIGN(A_SIGNED ? 1'b1 : 1'b0), - .B(B), - .SIB({B_WIDTH{1'b0}}), - .BSEL(1'b0), - .BSIGN(B_SIGNED ? 1'b1 : 1'b0), - .DOUT(Y) - ); + MULT18X18 __TECHMAP_REPLACE__ ( + .CLK(1'b0), + .CE(1'b0), + .RESET(1'b0), + .A(A), + .SIA({A_WIDTH{1'b0}}), + .ASEL(1'b0), + .ASIGN(A_SIGNED ? 1'b1 : 1'b0), + .B(B), + .SIB({B_WIDTH{1'b0}}), + .BSEL(1'b0), + .BSIGN(B_SIGNED ? 1'b1 : 1'b0), + .DOUT(Y) + ); endmodule @@ -56,15 +56,15 @@ module \$__MUL36X36 (input [35:0] A, input [35:0] B, output [71:0] Y); parameter A_SIGNED = 0; parameter B_SIGNED = 0; - MULT36X36 __TECHMAP_REPLACE__ ( - .CLK(1'b0), - .RESET(1'b0), - .CE(1'b0), - .A(A), - .ASIGN(A_SIGNED ? 1'b1 : 1'b0), - .B(B), - .BSIGN(B_SIGNED ? 1'b1 : 1'b0), - .DOUT(Y) - ); + MULT36X36 __TECHMAP_REPLACE__ ( + .CLK(1'b0), + .RESET(1'b0), + .CE(1'b0), + .A(A), + .ASIGN(A_SIGNED ? 1'b1 : 1'b0), + .B(B), + .BSIGN(B_SIGNED ? 1'b1 : 1'b0), + .DOUT(Y) + ); endmodule From 542b29fa6a1fe52631d15b7c29632d7532f0acd9 Mon Sep 17 00:00:00 2001 From: Maxim Kudinov Date: Tue, 3 Feb 2026 19:55:47 +0300 Subject: [PATCH 33/36] gowin: synth_gowin: Merge flatten label with coarse --- techlibs/gowin/synth_gowin.cc | 12 ++++-------- 1 file changed, 4 insertions(+), 8 deletions(-) diff --git a/techlibs/gowin/synth_gowin.cc b/techlibs/gowin/synth_gowin.cc index 9cc213945..2bf21cbc9 100644 --- a/techlibs/gowin/synth_gowin.cc +++ b/techlibs/gowin/synth_gowin.cc @@ -254,17 +254,13 @@ struct SynthGowinPass : public ScriptPass run(stringf("hierarchy -check %s", help_mode ? "-top " : top_opt)); } - if (flatten && check_label("flatten", "(unless -noflatten)")) - { - run("proc"); - run("flatten"); - run("tribuf -logic"); - run("deminout"); - } - if (check_label("coarse")) { run("proc"); + if (flatten || help_mode) + run("flatten", "(unless -noflatten)"); + run("tribuf -logic"); + run("deminout"); run("opt_expr"); run("opt_clean"); run("check"); From 5b94a97fb37787aa34a4808abd3df9de0842583b Mon Sep 17 00:00:00 2001 From: Maxim Kudinov Date: Thu, 12 Feb 2026 13:57:34 +0300 Subject: [PATCH 34/36] gowin: synth_gowin: Add -nodsp option --- techlibs/gowin/synth_gowin.cc | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/techlibs/gowin/synth_gowin.cc b/techlibs/gowin/synth_gowin.cc index 2bf21cbc9..cdc7d20f0 100644 --- a/techlibs/gowin/synth_gowin.cc +++ b/techlibs/gowin/synth_gowin.cc @@ -112,13 +112,16 @@ struct SynthGowinPass : public ScriptPass log(" -setundef\n"); log(" set undriven wires and parameters to zero\n"); log("\n"); + log(" -nodsp\n"); + log(" do not infer DSP multipliers\n"); + log("\n"); log("The following commands are executed by this synthesis command:\n"); help_script(); log("\n"); } string top_opt, vout_file, json_file, family; - bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef; + bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef, nodsp; void clear_flags() override { @@ -138,6 +141,7 @@ struct SynthGowinPass : public ScriptPass noalu = false; no_rw_check = false; setundef = false; + nodsp = false; } void execute(std::vector args, RTLIL::Design *design) override @@ -224,6 +228,10 @@ struct SynthGowinPass : public ScriptPass setundef = true; continue; } + if (args[argidx] == "-nodsp") { + nodsp = true; + continue; + } break; } extra_args(args, argidx, design); @@ -273,9 +281,9 @@ struct SynthGowinPass : public ScriptPass run("share"); if (help_mode) { - run("techmap -map +/mul2dsp.v [...]", "(if -family gw1n or gw2a)"); - run("techmap -map +/gowin/dsp_map.v", "(if -family gw1n or gw2a)"); - } else if (family == "gw1n" || family == "gw2a") { + run("techmap -map +/mul2dsp.v [...]", "(unless -nodsp and if -family gw1n or gw2a)"); + run("techmap -map +/gowin/dsp_map.v", "(unless -nodsp and if -family gw1n or gw2a)"); + } else if (!nodsp && (family == "gw1n" || family == "gw2a")) { for (const auto &rule : dsp_rules) { run(stringf("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=%d -D DSP_B_MAXWIDTH=%d -D DSP_A_MINWIDTH=%d -D DSP_B_MINWIDTH=%d -D DSP_NAME=%s", rule.a_maxwidth, rule.b_maxwidth, rule.a_minwidth, rule.b_minwidth, rule.prim)); From b055ea05fd314a6a928f0c2e3f777d6e8bf5f7d8 Mon Sep 17 00:00:00 2001 From: Maxim Kudinov Date: Thu, 12 Feb 2026 14:12:32 +0300 Subject: [PATCH 35/36] gowin: dsp: Add mult inference tests --- tests/arch/gowin/mul_gw1n.ys | 53 ++++++++++++++++++++++++++++++++++++ tests/arch/gowin/mul_gw2a.ys | 53 ++++++++++++++++++++++++++++++++++++ 2 files changed, 106 insertions(+) create mode 100644 tests/arch/gowin/mul_gw1n.ys create mode 100644 tests/arch/gowin/mul_gw2a.ys diff --git a/tests/arch/gowin/mul_gw1n.ys b/tests/arch/gowin/mul_gw1n.ys new file mode 100644 index 000000000..9b1748255 --- /dev/null +++ b/tests/arch/gowin/mul_gw1n.ys @@ -0,0 +1,53 @@ +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +# equivalence checking is somewhat slow (and missing simulation models) +synth_gowin -family gw1n +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT9X9 + + +# Make sure that DSPs are not inferred with -nodsp option +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +synth_gowin -family gw1n -nodsp +cd top # Constrain all select calls below inside the top module +select -assert-none t:MULT9X9 + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32 +hierarchy -top top +proc +synth_gowin -family gw1n +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT18X18 + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_gowin +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT36X36 + + +# We end up with two 18x18 multipliers +# 36x36 min width is 22 +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_gowin +cd top # Constrain all select calls below inside the top module +select -assert-count 2 t:MULT18X18 diff --git a/tests/arch/gowin/mul_gw2a.ys b/tests/arch/gowin/mul_gw2a.ys new file mode 100644 index 000000000..895c580b7 --- /dev/null +++ b/tests/arch/gowin/mul_gw2a.ys @@ -0,0 +1,53 @@ +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +# equivalence checking is somewhat slow (and missing simulation models) +synth_gowin -family gw2a +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT9X9 + + +# Make sure that DSPs are not inferred with -nodsp option +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16 +hierarchy -top top +proc +synth_gowin -family gw2a -nodsp +cd top # Constrain all select calls below inside the top module +select -assert-none t:MULT9X9 + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32 +hierarchy -top top +proc +synth_gowin -family gw2a +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT18X18 + + +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_gowin -family gw2a +cd top # Constrain all select calls below inside the top module +select -assert-count 1 t:MULT36X36 + + +# We end up with two 18x18 multipliers +# 36x36 min width is 22 +design -reset +read_verilog ../common/mul.v +chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48 +hierarchy -top top +proc +# equivalence checking is too slow here +synth_gowin -family gw2a +cd top # Constrain all select calls below inside the top module +select -assert-count 2 t:MULT18X18 From e2f0c4d9a04dcc2b2e5667471635073db6102517 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Fri, 13 Feb 2026 00:35:27 +0000 Subject: [PATCH 36/36] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 02fe61004..0f76cdbef 100644 --- a/Makefile +++ b/Makefile @@ -161,7 +161,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.62+39 +YOSYS_VER := 0.62+55 YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1) YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1) YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2)