From 5a9d73369abd5e1ca03ce09ff748901cb8e83cfb Mon Sep 17 00:00:00 2001 From: Lofty Date: Tue, 20 Jan 2026 09:51:53 +0000 Subject: [PATCH 01/87] abc9: verify post-mapping equivalence by default --- passes/techmap/abc9_exe.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc index 4449065f8..2baf53a02 100644 --- a/passes/techmap/abc9_exe.cc +++ b/passes/techmap/abc9_exe.cc @@ -248,7 +248,7 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe } abc9_script += stringf("; &ps -l; &write -n %s/output.aig", tempdir_name); - if (design->scratchpad_get_bool("abc9.verify")) { + if (design->scratchpad_get_bool("abc9.verify", true)) { if (dff_mode) abc9_script += "; &verify -s"; else From 9315f02c17ef5b3149a4767d9851045f2cee15cb Mon Sep 17 00:00:00 2001 From: Gabriel Gouvine Date: Mon, 25 Mar 2024 11:33:52 +0000 Subject: [PATCH 02/87] 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 03/87] 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 04/87] 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 05/87] 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 06/87] 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 07/87] 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 08/87] 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 09/87] 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 10/87] 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 11/87] 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 000be270ca3272dd660dcd82b8a142b9fd593411 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 17:54:46 +0100 Subject: [PATCH 12/87] equiv_simple, equiv_induct: refactor --- passes/equiv/equiv.h | 73 ++++++++++++++++++++++ passes/equiv/equiv_induct.cc | 66 +++++--------------- passes/equiv/equiv_simple.cc | 118 ++++++++++++++--------------------- 3 files changed, 136 insertions(+), 121 deletions(-) create mode 100644 passes/equiv/equiv.h diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h new file mode 100644 index 000000000..b255042ba --- /dev/null +++ b/passes/equiv/equiv.h @@ -0,0 +1,73 @@ +#ifndef EQUIV_H +#define EQUIV_H + +#include "kernel/log.h" +#include "kernel/yosys_common.h" +#include "kernel/sigtools.h" +#include "kernel/satgen.h" + +YOSYS_NAMESPACE_BEGIN + +static void report_missing_model(bool warn_only, RTLIL::Cell* cell) +{ + std::string s; + if (cell->is_builtin_ff()) + s = stringf("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); + else + s = stringf("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); + + if (warn_only) { + log_formatted_warning_noprefix(s); + } else { + log_formatted_error(s); + } +} + +struct EquivWorker { + RTLIL::Module *module; + + ezSatPtr ez; + SatGen satgen; + + struct Config { + bool model_undef = false; + int max_seq = 1; + bool set_assumes = false; + + bool parse(const std::vector& args, size_t& idx) { + if (args[idx] == "-undef") { + model_undef = true; + return true; + } + if (args[idx] == "-seq" && idx+1 < args.size()) { + max_seq = atoi(args[++idx].c_str()); + return true; + } + if (args[idx] == "-set-assumes") { + set_assumes = true; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return stringf( + " -undef\n" + " enable modelling of undef states\n" + "\n" + " -seq \n" + " the max. number of time steps to be considered (default = %s)\n" + "\n" + " -set-assumes\n" + " set all assumptions provided via $assume cells\n" + , default_seq); + } + }; + Config cfg; + + EquivWorker(RTLIL::Module *module, const SigMap *sigmap, Config cfg) : module(module), satgen(ez.get(), sigmap), cfg(cfg) { + satgen.model_undef = cfg.model_undef; + } +}; + +YOSYS_NAMESPACE_END +#endif // EQUIV_H diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index e1a3a7990..c91501719 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -18,49 +18,34 @@ */ #include "kernel/yosys.h" -#include "kernel/satgen.h" -#include "kernel/sigtools.h" +#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivInductWorker +struct EquivInductWorker : public EquivWorker { - Module *module; SigMap sigmap; vector cells; pool workset; - ezSatPtr ez; - SatGen satgen; - - int max_seq; int success_counter; - bool set_assumes; dict ez_step_is_consistent; - pool cell_warn_cache; SigPool undriven_signals; - EquivInductWorker(Module *module, const pool &unproven_equiv_cells, bool model_undef, int max_seq, bool set_assumes) : module(module), sigmap(module), + EquivInductWorker(Module *module, const pool &unproven_equiv_cells, Config cfg) : EquivWorker(module, &sigmap, cfg), sigmap(module), cells(module->selected_cells()), workset(unproven_equiv_cells), - satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0), set_assumes(set_assumes) - { - satgen.model_undef = model_undef; - } + success_counter(0) {} void create_timestep(int step) { vector ez_equal_terms; for (auto cell : cells) { - if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) { - if (cell->is_builtin_ff()) - log_warning("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); - else - log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); - cell_warn_cache.insert(cell); + if (!satgen.importCell(cell, step)) { + report_missing_model(true, cell); } if (cell->type == ID($equiv)) { SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit(); @@ -78,7 +63,7 @@ struct EquivInductWorker } } - if (set_assumes) { + if (cfg.set_assumes) { if (step == 1) { RTLIL::SigSpec assumes_a, assumes_en; satgen.getAssumes(assumes_a, assumes_en, step); @@ -123,7 +108,7 @@ struct EquivInductWorker GetSize(satgen.initial_state), GetSize(undriven_signals)); } - for (int step = 1; step <= max_seq; step++) + for (int step = 1; step <= cfg.max_seq; step++) { ez->assume(ez_step_is_consistent[step]); @@ -146,7 +131,7 @@ struct EquivInductWorker return; } - log(" Proof for induction step failed. %s\n", step != max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset."); + log(" Proof for induction step failed. %s\n", step != cfg.max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset."); } workset.sort(); @@ -158,12 +143,12 @@ struct EquivInductWorker log(" Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort(ID::Y)))); - int ez_a = satgen.importSigBit(bit_a, max_seq+1); - int ez_b = satgen.importSigBit(bit_b, max_seq+1); + int ez_a = satgen.importSigBit(bit_a, cfg.max_seq+1); + int ez_b = satgen.importSigBit(bit_b, cfg.max_seq+1); int cond = ez->XOR(ez_a, ez_b); if (satgen.model_undef) - cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, max_seq+1))); + cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, cfg.max_seq+1))); if (!ez->solve(cond)) { log(" success!\n"); @@ -189,14 +174,7 @@ struct EquivInductPass : public Pass { log("Only selected $equiv cells are proven and only selected cells are used to\n"); log("perform the proof.\n"); log("\n"); - log(" -undef\n"); - log(" enable modelling of undef states\n"); - log("\n"); - log(" -seq \n"); - log(" the max. number of time steps to be considered (default = 4)\n"); - log("\n"); - log(" -set-assumes\n"); - log(" set all assumptions provided via $assume cells\n"); + EquivWorker::Config::help("4"); log("\n"); log("This command is very effective in proving complex sequential circuits, when\n"); log("the internal state of the circuit quickly propagates to $equiv cells.\n"); @@ -214,25 +192,15 @@ struct EquivInductPass : public Pass { void execute(std::vector args, Design *design) override { int success_counter = 0; - bool model_undef = false, set_assumes = false; - int max_seq = 4; + EquivWorker::Config cfg; + cfg.max_seq = 4; log_header(design, "Executing EQUIV_INDUCT pass.\n"); size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-undef") { - model_undef = true; + if (cfg.parse(args, argidx)) continue; - } - if (args[argidx] == "-seq" && argidx+1 < args.size()) { - max_seq = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-set-assumes") { - set_assumes = true; - continue; - } break; } extra_args(args, argidx, design); @@ -253,7 +221,7 @@ struct EquivInductPass : public Pass { continue; } - EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq, set_assumes); + EquivInductWorker worker(module, unproven_equiv_cells, cfg); worker.run(); success_counter += worker.success_counter; } diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 97f95ac63..0749d18aa 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -17,15 +17,52 @@ * */ +#include "kernel/log.h" #include "kernel/yosys.h" -#include "kernel/satgen.h" +#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivSimpleWorker +struct EquivSimpleWorker : public EquivWorker { - Module *module; + struct Config : EquivWorker::Config { + bool verbose = false; + bool short_cones = false; + bool group = true; + bool parse(const std::vector& args, size_t& idx) { + if (EquivWorker::Config::parse(args, idx)) + return true; + if (args[idx] == "-v") { + verbose = true; + return true; + } + if (args[idx] == "-short") { + short_cones = true; + return true; + } + if (args[idx] == "-nogroup") { + group = false; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return EquivWorker::Config::help(default_seq) + + " -v\n" + " verbose output\n" + "\n" + " -short\n" + " create shorter input cones that stop at shared nodes. This yields\n" + " simpler SAT problems but sometimes fails to prove equivalence.\n" + "\n" + " -nogroup\n" + " disabling grouping of $equiv cells by output wire\n" + "\n"; + } + }; + Config cfg; + const vector &equiv_cells; const vector &assume_cells; struct Cone { @@ -43,27 +80,11 @@ struct EquivSimpleWorker }; DesignModel model; - ezSatPtr ez; - SatGen satgen; - - struct Config { - bool verbose = false; - bool short_cones = false; - bool model_undef = false; - bool nogroup = false; - bool set_assumes = false; - int max_seq = 1; - }; - Config cfg; - pool> imported_cells_cache; EquivSimpleWorker(const vector &equiv_cells, const vector &assume_cells, DesignModel model, Config cfg) : - module(equiv_cells.front()->module), equiv_cells(equiv_cells), assume_cells(assume_cells), - model(model), satgen(ez.get(), &model.sigmap), cfg(cfg) - { - satgen.model_undef = cfg.model_undef; - } + EquivWorker(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells), + model(model) {} struct ConeFinder { DesignModel model; @@ -229,14 +250,6 @@ struct EquivSimpleWorker return extra_problem_cells; } - static void report_missing_model(Cell* cell) - { - if (cell->is_builtin_ff()) - log_cmd_error("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); - else - log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); - } - void prepare_ezsat(int ez_context, SigBit bit_a, SigBit bit_b) { if (satgen.model_undef) @@ -323,7 +336,7 @@ struct EquivSimpleWorker for (auto cell : problem_cells) { auto key = pair(cell, step+1); if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) { - report_missing_model(cell); + report_missing_model(true, cell); } imported_cells_cache.insert(key); } @@ -414,24 +427,7 @@ struct EquivSimplePass : public Pass { log("\n"); log("This command tries to prove $equiv cells using a simple direct SAT approach.\n"); log("\n"); - log(" -v\n"); - log(" verbose output\n"); - log("\n"); - log(" -undef\n"); - log(" enable modelling of undef states\n"); - log("\n"); - log(" -short\n"); - log(" create shorter input cones that stop at shared nodes. This yields\n"); - log(" simpler SAT problems but sometimes fails to prove equivalence.\n"); - log("\n"); - log(" -nogroup\n"); - log(" disabling grouping of $equiv cells by output wire\n"); - log("\n"); - log(" -seq \n"); - log(" the max. number of time steps to be considered (default = 1)\n"); - log("\n"); - log(" -set-assumes\n"); - log(" set all assumptions provided via $assume cells\n"); + EquivSimpleWorker::Config::help("1"); log("\n"); } void execute(std::vector args, Design *design) override @@ -443,30 +439,8 @@ struct EquivSimplePass : public Pass { size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { - if (args[argidx] == "-v") { - cfg.verbose = true; + if (cfg.parse(args, argidx)) continue; - } - if (args[argidx] == "-short") { - cfg.short_cones = true; - continue; - } - if (args[argidx] == "-undef") { - cfg.model_undef = true; - continue; - } - if (args[argidx] == "-nogroup") { - cfg.nogroup = true; - continue; - } - if (args[argidx] == "-seq" && argidx+1 < args.size()) { - cfg.max_seq = atoi(args[++argidx].c_str()); - continue; - } - if (args[argidx] == "-set-assumes") { - cfg.set_assumes = true; - continue; - } break; } extra_args(args, argidx, design); @@ -489,7 +463,7 @@ struct EquivSimplePass : public Pass { if (cell->type == ID($equiv) && cell->getPort(ID::A) != cell->getPort(ID::B)) { auto bit = sigmap(cell->getPort(ID::Y).as_bit()); auto bit_group = bit; - if (!cfg.nogroup && bit_group.wire) + if (cfg.group && bit_group.wire) bit_group.offset = 0; unproven_equiv_cells[bit_group][bit] = cell; unproven_cells_counter++; From 8e73e2a306809369c2f71d6037f1671e36e69d4e Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 17:56:10 +0100 Subject: [PATCH 13/87] sat: add -ignore-unknown-cells instead of -ignore_unknown_cells for consistency --- passes/sat/sat.cc | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 90b85d709..ffebdd01c 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -961,10 +961,10 @@ struct SatPass : public Pass { log(" -show-regs, -show-public, -show-all\n"); log(" show all registers, show signals with 'public' names, show all signals\n"); log("\n"); - log(" -ignore_div_by_zero\n"); + log(" -ignore-div-by-zero\n"); log(" ignore all solutions that involve a division by zero\n"); log("\n"); - log(" -ignore_unknown_cells\n"); + log(" -ignore-unknown-cells\n"); log(" ignore all cells that can not be matched to a SAT model\n"); log("\n"); log("The following options can be used to set up a sequential problem:\n"); @@ -1141,7 +1141,7 @@ struct SatPass : public Pass { stepsize = max(1, atoi(args[++argidx].c_str())); continue; } - if (args[argidx] == "-ignore_div_by_zero") { + if (args[argidx] == "-ignore-div-by-zero" || args[argidx] == "-ignore_div_by_zero") { ignore_div_by_zero = true; continue; } @@ -1316,7 +1316,7 @@ struct SatPass : public Pass { show_all = true; continue; } - if (args[argidx] == "-ignore_unknown_cells") { + if (args[argidx] == "-ignore-unknown-cells" || args[argidx] == "-ignore_unknown_cells") { ignore_unknown_cells = true; continue; } From 8d1c1faf82ec085c9756a31010ed9d50d06334d3 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 17:59:31 +0100 Subject: [PATCH 14/87] equiv_simple, equiv_induct: error by default on missing model, add -ignore-unknown-cells --- passes/equiv/equiv.h | 8 ++++++++ passes/equiv/equiv_induct.cc | 2 +- passes/equiv/equiv_simple.cc | 2 +- 3 files changed, 10 insertions(+), 2 deletions(-) diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h index b255042ba..8a24b2fcd 100644 --- a/passes/equiv/equiv.h +++ b/passes/equiv/equiv.h @@ -33,6 +33,7 @@ struct EquivWorker { bool model_undef = false; int max_seq = 1; bool set_assumes = false; + bool ignore_unknown_cells = false; bool parse(const std::vector& args, size_t& idx) { if (args[idx] == "-undef") { @@ -47,6 +48,10 @@ struct EquivWorker { set_assumes = true; return true; } + if (args[idx] == "-ignore-unknown-cells") { + ignore_unknown_cells = true; + return true; + } return false; } static std::string help(const char* default_seq) { @@ -59,6 +64,9 @@ struct EquivWorker { "\n" " -set-assumes\n" " set all assumptions provided via $assume cells\n" + "\n" + " -ignore-unknown-cells\n" + " ignore all cells that can not be matched to a SAT model\n" , default_seq); } }; diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index c91501719..f7ceb78a3 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -45,7 +45,7 @@ struct EquivInductWorker : public EquivWorker for (auto cell : cells) { if (!satgen.importCell(cell, step)) { - report_missing_model(true, cell); + report_missing_model(cfg.ignore_unknown_cells, cell); } if (cell->type == ID($equiv)) { SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit(); diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 0749d18aa..f345e9794 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -336,7 +336,7 @@ struct EquivSimpleWorker : public EquivWorker for (auto cell : problem_cells) { auto key = pair(cell, step+1); if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) { - report_missing_model(true, cell); + report_missing_model(cfg.ignore_unknown_cells, cell); } imported_cells_cache.insert(key); } From d199195785fb058eb1c92502787e79be3ea56943 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:00:45 +0100 Subject: [PATCH 15/87] satgen: cover $input_port --- kernel/satgen.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/satgen.cc b/kernel/satgen.cc index f2c1e00c2..b8b850bb3 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -1378,7 +1378,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) return true; } - if (cell->type == ID($scopeinfo)) + if (cell->type == ID($scopeinfo) || cell->type == ID($input_port)) { return true; } From 2efd0247a10192fb1240c0c7a6778b2979b3377d Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:09:51 +0100 Subject: [PATCH 16/87] opt_hier: fix test --- tests/opt/opt_hier.tcl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/opt/opt_hier.tcl b/tests/opt/opt_hier.tcl index 65d8f9809..d006759f5 100644 --- a/tests/opt/opt_hier.tcl +++ b/tests/opt/opt_hier.tcl @@ -27,7 +27,7 @@ foreach fn [glob opt_hier_*.v] { design -copy-from gate -as gate A:top yosys rename -hide equiv_make gold gate equiv - equiv_induct equiv + equiv_induct -ignore-unknown-cells equiv equiv_status -assert equiv log -pop From c768e55983f2077da5d0a7d1798f73a35055af8b Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:10:02 +0100 Subject: [PATCH 17/87] ice40: fix dsp_const test --- tests/arch/ice40/ice40_dsp_const.ys | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/arch/ice40/ice40_dsp_const.ys b/tests/arch/ice40/ice40_dsp_const.ys index c9c76a1ac..735f945a1 100644 --- a/tests/arch/ice40/ice40_dsp_const.ys +++ b/tests/arch/ice40/ice40_dsp_const.ys @@ -74,6 +74,7 @@ EOT techmap -wb -D EQUIV -autoproc -map +/ice40/cells_sim.v +async2sync equiv_make top ref equiv select -assert-any -module equiv t:$equiv equiv_induct From ed53ff2f4988c6fc49cefafa85b6a82ef2ca1871 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:37:39 +0100 Subject: [PATCH 18/87] equiv_simple, equiv_induct: fix config --- passes/equiv/equiv.h | 89 ++++++++++++++++++------------------ passes/equiv/equiv_induct.cc | 8 ++-- passes/equiv/equiv_simple.cc | 81 ++++++++++++++++---------------- 3 files changed, 90 insertions(+), 88 deletions(-) diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h index 8a24b2fcd..9641e65a7 100644 --- a/passes/equiv/equiv.h +++ b/passes/equiv/equiv.h @@ -23,54 +23,55 @@ static void report_missing_model(bool warn_only, RTLIL::Cell* cell) } } +struct EquivBasicConfig { + bool model_undef = false; + int max_seq = 1; + bool set_assumes = false; + bool ignore_unknown_cells = false; + + bool parse(const std::vector& args, size_t& idx) { + if (args[idx] == "-undef") { + model_undef = true; + return true; + } + if (args[idx] == "-seq" && idx+1 < args.size()) { + max_seq = atoi(args[++idx].c_str()); + return true; + } + if (args[idx] == "-set-assumes") { + set_assumes = true; + return true; + } + if (args[idx] == "-ignore-unknown-cells") { + ignore_unknown_cells = true; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return stringf( + " -undef\n" + " enable modelling of undef states\n" + "\n" + " -seq \n" + " the max. number of time steps to be considered (default = %s)\n" + "\n" + " -set-assumes\n" + " set all assumptions provided via $assume cells\n" + "\n" + " -ignore-unknown-cells\n" + " ignore all cells that can not be matched to a SAT model\n" + , default_seq); + } +}; + +template struct EquivWorker { RTLIL::Module *module; - ezSatPtr ez; + ezSatPtr ez; SatGen satgen; - - struct Config { - bool model_undef = false; - int max_seq = 1; - bool set_assumes = false; - bool ignore_unknown_cells = false; - - bool parse(const std::vector& args, size_t& idx) { - if (args[idx] == "-undef") { - model_undef = true; - return true; - } - if (args[idx] == "-seq" && idx+1 < args.size()) { - max_seq = atoi(args[++idx].c_str()); - return true; - } - if (args[idx] == "-set-assumes") { - set_assumes = true; - return true; - } - if (args[idx] == "-ignore-unknown-cells") { - ignore_unknown_cells = true; - return true; - } - return false; - } - static std::string help(const char* default_seq) { - return stringf( - " -undef\n" - " enable modelling of undef states\n" - "\n" - " -seq \n" - " the max. number of time steps to be considered (default = %s)\n" - "\n" - " -set-assumes\n" - " set all assumptions provided via $assume cells\n" - "\n" - " -ignore-unknown-cells\n" - " ignore all cells that can not be matched to a SAT model\n" - , default_seq); - } - }; - Config cfg; + Config cfg; EquivWorker(RTLIL::Module *module, const SigMap *sigmap, Config cfg) : module(module), satgen(ez.get(), sigmap), cfg(cfg) { satgen.model_undef = cfg.model_undef; diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index f7ceb78a3..d843fef67 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -23,7 +23,7 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivInductWorker : public EquivWorker +struct EquivInductWorker : public EquivWorker<> { SigMap sigmap; @@ -35,7 +35,7 @@ struct EquivInductWorker : public EquivWorker dict ez_step_is_consistent; SigPool undriven_signals; - EquivInductWorker(Module *module, const pool &unproven_equiv_cells, Config cfg) : EquivWorker(module, &sigmap, cfg), sigmap(module), + EquivInductWorker(Module *module, const pool &unproven_equiv_cells, EquivBasicConfig cfg) : EquivWorker<>(module, &sigmap, cfg), sigmap(module), cells(module->selected_cells()), workset(unproven_equiv_cells), success_counter(0) {} @@ -174,7 +174,7 @@ struct EquivInductPass : public Pass { log("Only selected $equiv cells are proven and only selected cells are used to\n"); log("perform the proof.\n"); log("\n"); - EquivWorker::Config::help("4"); + EquivBasicConfig::help("4"); log("\n"); log("This command is very effective in proving complex sequential circuits, when\n"); log("the internal state of the circuit quickly propagates to $equiv cells.\n"); @@ -192,7 +192,7 @@ struct EquivInductPass : public Pass { void execute(std::vector args, Design *design) override { int success_counter = 0; - EquivWorker::Config cfg; + EquivBasicConfig cfg {}; cfg.max_seq = 4; log_header(design, "Executing EQUIV_INDUCT pass.\n"); diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index f345e9794..ff6df295c 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -24,45 +24,44 @@ USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN -struct EquivSimpleWorker : public EquivWorker -{ - struct Config : EquivWorker::Config { - bool verbose = false; - bool short_cones = false; - bool group = true; - bool parse(const std::vector& args, size_t& idx) { - if (EquivWorker::Config::parse(args, idx)) - return true; - if (args[idx] == "-v") { - verbose = true; - return true; - } - if (args[idx] == "-short") { - short_cones = true; - return true; - } - if (args[idx] == "-nogroup") { - group = false; - return true; - } - return false; +struct EquivSimpleConfig : EquivBasicConfig { + bool verbose = false; + bool short_cones = false; + bool group = true; + bool parse(const std::vector& args, size_t& idx) { + if (EquivBasicConfig::parse(args, idx)) + return true; + if (args[idx] == "-v") { + verbose = true; + return true; } - static std::string help(const char* default_seq) { - return EquivWorker::Config::help(default_seq) + - " -v\n" - " verbose output\n" - "\n" - " -short\n" - " create shorter input cones that stop at shared nodes. This yields\n" - " simpler SAT problems but sometimes fails to prove equivalence.\n" - "\n" - " -nogroup\n" - " disabling grouping of $equiv cells by output wire\n" - "\n"; + if (args[idx] == "-short") { + short_cones = true; + return true; } - }; - Config cfg; + if (args[idx] == "-nogroup") { + group = false; + return true; + } + return false; + } + static std::string help(const char* default_seq) { + return EquivBasicConfig::help(default_seq) + + " -v\n" + " verbose output\n" + "\n" + " -short\n" + " create shorter input cones that stop at shared nodes. This yields\n" + " simpler SAT problems but sometimes fails to prove equivalence.\n" + "\n" + " -nogroup\n" + " disabling grouping of $equiv cells by output wire\n" + "\n"; + } +}; +struct EquivSimpleWorker : public EquivWorker +{ const vector &equiv_cells; const vector &assume_cells; struct Cone { @@ -82,8 +81,8 @@ struct EquivSimpleWorker : public EquivWorker pool> imported_cells_cache; - EquivSimpleWorker(const vector &equiv_cells, const vector &assume_cells, DesignModel model, Config cfg) : - EquivWorker(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells), + EquivSimpleWorker(const vector &equiv_cells, const vector &assume_cells, DesignModel model, EquivSimpleConfig cfg) : + EquivWorker(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells), model(model) {} struct ConeFinder { @@ -270,7 +269,9 @@ struct EquivSimpleWorker : public EquivWorker } void construct_ezsat(const pool& input_bits, int step) { + log("ezsat\n"); if (cfg.set_assumes) { + log("yep assume\n"); if (cfg.verbose && step == cfg.max_seq) { RTLIL::SigSpec assumes_a, assumes_en; satgen.getAssumes(assumes_a, assumes_en, step+1); @@ -427,12 +428,12 @@ struct EquivSimplePass : public Pass { log("\n"); log("This command tries to prove $equiv cells using a simple direct SAT approach.\n"); log("\n"); - EquivSimpleWorker::Config::help("1"); + EquivSimpleConfig::help("1"); log("\n"); } void execute(std::vector args, Design *design) override { - EquivSimpleWorker::Config cfg = {}; + EquivSimpleConfig cfg {}; int success_counter = 0; log_header(design, "Executing EQUIV_SIMPLE pass.\n"); From 91b226b4d40815109f0ac1223bc2fafdf0aa0d03 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Tue, 3 Feb 2026 18:40:32 +0100 Subject: [PATCH 19/87] specify: fix test --- tests/various/specify.ys | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/various/specify.ys b/tests/various/specify.ys index d7260d524..86471de5e 100644 --- a/tests/various/specify.ys +++ b/tests/various/specify.ys @@ -43,7 +43,7 @@ select n:C_* -assert-count 2 equiv_make gold gate equiv hierarchy -top equiv equiv_struct -equiv_induct -seq 5 +equiv_induct -ignore-unknown-cells -seq 5 equiv_status -assert design -reset @@ -57,7 +57,7 @@ select n:B_* -assert-count 2 equiv_make gold gate equiv hierarchy -top equiv equiv_struct -equiv_induct -seq 5 +equiv_induct -ignore-unknown-cells -seq 5 equiv_status -assert design -reset From 3f01d7a33ae27df8f1d120dce082b02e526e8a0c Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Tue, 3 Feb 2026 14:41:08 -0800 Subject: [PATCH 20/87] 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 21/87] 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 22/87] 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 23/87] 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 24/87] 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 25/87] 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 b8ee50d77f92da71420186a9ab2918918b32b809 Mon Sep 17 00:00:00 2001 From: Rowan Goemans Date: Mon, 9 Feb 2026 14:13:40 +0100 Subject: [PATCH 26/87] kernel/celledges: cover more cell types --- kernel/celledges.cc | 144 +++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 136 insertions(+), 8 deletions(-) diff --git a/kernel/celledges.cc b/kernel/celledges.cc index c39ced95a..195d4b15b 100644 --- a/kernel/celledges.cc +++ b/kernel/celledges.cc @@ -112,6 +112,41 @@ void reduce_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) db->add_edge(cell, ID::A, i, ID::Y, 0, -1); } +void logic_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int a_width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + + for (int i = 0; i < a_width; i++) + db->add_edge(cell, ID::A, i, ID::Y, 0, -1); + for (int i = 0; i < b_width; i++) + db->add_edge(cell, ID::B, i, ID::Y, 0, -1); +} + +void concat_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int a_width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + + for (int i = 0; i < a_width; i++) + db->add_edge(cell, ID::A, i, ID::Y, i, -1); + for (int i = 0; i < b_width; i++) + db->add_edge(cell, ID::B, i, ID::Y, a_width + i, -1); +} + +void slice_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int offset = cell->getParam(ID::OFFSET).as_int(); + int a_width = GetSize(cell->getPort(ID::A)); + int y_width = GetSize(cell->getPort(ID::Y)); + + for (int i = 0; i < y_width; i++) { + int a_bit = offset + i; + if (a_bit >= 0 && a_bit < a_width) + db->add_edge(cell, ID::A, a_bit, ID::Y, i, -1); + } +} + void compare_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) { int a_width = GetSize(cell->getPort(ID::A)); @@ -254,7 +289,7 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) int skip = 1 << (k + 1); int base = skip -1; if (i % skip != base && i - a_width + 2 < 1 << b_width_capped) - db->add_edge(cell, ID::B, k, ID::Y, i, -1); + db->add_edge(cell, ID::B, k, ID::Y, i, -1); } else if (is_signed) { if (i - a_width + 2 < 1 << b_width_capped) db->add_edge(cell, ID::B, k, ID::Y, i, -1); @@ -388,6 +423,64 @@ void ff_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) db->add_edge(cell, ID::ARST, 0, ID::Q, k, -1); } +void full_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + std::vector input_ports; + std::vector output_ports; + + for (auto &conn : cell->connections()) + { + RTLIL::IdString port = conn.first; + RTLIL::PortDir dir = cell->port_dir(port); + if (cell->input(port) || dir == RTLIL::PortDir::PD_INOUT) + input_ports.push_back(port); + if (cell->output(port) || dir == RTLIL::PortDir::PD_INOUT) + output_ports.push_back(port); + } + + for (auto out_port : output_ports) + { + int out_width = GetSize(cell->getPort(out_port)); + for (int out_bit = 0; out_bit < out_width; out_bit++) + { + for (auto in_port : input_ports) + { + int in_width = GetSize(cell->getPort(in_port)); + for (int in_bit = 0; in_bit < in_width; in_bit++) + db->add_edge(cell, in_port, in_bit, out_port, out_bit, -1); + } + } + } +} + +void bweqx_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int width = GetSize(cell->getPort(ID::Y)); + int a_width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + int max_width = std::min(width, std::min(a_width, b_width)); + + for (int i = 0; i < max_width; i++) { + db->add_edge(cell, ID::A, i, ID::Y, i, -1); + db->add_edge(cell, ID::B, i, ID::Y, i, -1); + } +} + +void bwmux_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell) +{ + int width = GetSize(cell->getPort(ID::Y)); + int a_width = GetSize(cell->getPort(ID::A)); + int b_width = GetSize(cell->getPort(ID::B)); + int s_width = GetSize(cell->getPort(ID::S)); + int max_width = std::min(width, std::min(a_width, std::min(b_width, s_width))); + + for (int i = 0; i < max_width; i++) { + db->add_edge(cell, ID::A, i, ID::Y, i, -1); + db->add_edge(cell, ID::B, i, ID::Y, i, -1); + db->add_edge(cell, ID::S, i, ID::Y, i, -1); + } +} + PRIVATE_NAMESPACE_END bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL::Cell *cell) @@ -417,6 +510,21 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return true; } + if (cell->type.in(ID($logic_and), ID($logic_or))) { + logic_op(this, cell); + return true; + } + + if (cell->type == ID($slice)) { + slice_op(this, cell); + return true; + } + + if (cell->type == ID($concat)) { + concat_op(this, cell); + return true; + } + if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) { shift_op(this, cell); return true; @@ -442,6 +550,16 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return true; } + if (cell->type == ID($bweqx)) { + bweqx_op(this, cell); + return true; + } + + if (cell->type == ID($bwmux)) { + bwmux_op(this, cell); + return true; + } + if (cell->type.in(ID($mem_v2), ID($memrd), ID($memrd_v2), ID($memwr), ID($memwr_v2), ID($meminit))) { mem_op(this, cell); return true; @@ -452,13 +570,24 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return true; } - // FIXME: $mul $div $mod $divfloor $modfloor $slice $concat - // FIXME: $lut $sop $alu $lcu $macc $macc_v2 $fa - // FIXME: $mul $div $mod $divfloor $modfloor $pow $slice $concat $bweqx - // FIXME: $lut $sop $alu $lcu $macc $fa $logic_and $logic_or $bwmux + if (cell->type.in(ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow))) { + full_op(this, cell); + return true; + } - // FIXME: $_BUF_ $_NOT_ $_AND_ $_NAND_ $_OR_ $_NOR_ $_XOR_ $_XNOR_ $_ANDNOT_ $_ORNOT_ - // FIXME: $_MUX_ $_NMUX_ $_MUX4_ $_MUX8_ $_MUX16_ $_AOI3_ $_OAI3_ $_AOI4_ $_OAI4_ + if (cell->type.in(ID($lut), ID($sop), ID($alu), ID($lcu), ID($macc), ID($macc_v2))) { + full_op(this, cell); + return true; + } + + if (cell->type.in( + ID($_BUF_), ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), + ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_), ID($_MUX_), ID($_NMUX_), + ID($_MUX4_), ID($_MUX8_), ID($_MUX16_), ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), + ID($_OAI4_), ID($_TBUF_))) { + full_op(this, cell); + return true; + } // FIXME: $specify2 $specify3 $specrule ??? // FIXME: $equiv $set_tag $get_tag $overwrite_tag $original_tag @@ -468,4 +597,3 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL return false; } - From 6f6fa49d3cac7f2d379a162b0dc6dc3ea49faa54 Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Mon, 9 Feb 2026 09:05:56 -0800 Subject: [PATCH 27/87] 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 28/87] 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: Mon, 9 Feb 2026 23:16:47 +0100 Subject: [PATCH 29/87] Makefile: test target requires unit-test, add vanilla-test for old test target --- .github/workflows/test-sanitizers.yml | 4 +- .github/workflows/test-verific.yml | 4 +- Makefile | 6 +- README.md | 4 +- .../extending_yosys/test_suites.rst | 55 +++++++++++++------ 5 files changed, 47 insertions(+), 26 deletions(-) diff --git a/.github/workflows/test-sanitizers.yml b/.github/workflows/test-sanitizers.yml index 11a339cd3..c6b3d8db0 100644 --- a/.github/workflows/test-sanitizers.yml +++ b/.github/workflows/test-sanitizers.yml @@ -65,7 +65,7 @@ jobs: - name: Run tests shell: bash run: | - make -j$procs test TARGETS= EXTRA_TARGETS= + make -j$procs vanilla-test TARGETS= EXTRA_TARGETS= - name: Report errors if: ${{ failure() }} @@ -76,4 +76,4 @@ jobs: - name: Run unit tests shell: bash run: | - make -j$procs unit-test ENABLE_LIBYOSYS=1 + make -j$procs unit-test diff --git a/.github/workflows/test-verific.yml b/.github/workflows/test-verific.yml index adc6f59d8..feba3c0f9 100644 --- a/.github/workflows/test-verific.yml +++ b/.github/workflows/test-verific.yml @@ -68,7 +68,7 @@ jobs: - name: Run Yosys tests run: | - make -j$procs test + make -j$procs vanilla-test - name: Run Verific specific Yosys tests run: | @@ -83,7 +83,7 @@ jobs: - name: Run unit tests shell: bash run: | - make -j$procs unit-test ENABLE_LTO=1 ENABLE_LIBYOSYS=1 + make -j$procs unit-test ENABLE_LTO=1 test-pyosys: needs: pre-job diff --git a/Makefile b/Makefile index 364e1ce8d..7ce3153df 100644 --- a/Makefile +++ b/Makefile @@ -977,9 +977,11 @@ makefile-tests/%: %/run-test.mk $(TARGETS) $(EXTRA_TARGETS) $(MAKE) -C $* -f run-test.mk +@echo "...passed tests in $*" -test: makefile-tests abcopt-tests seed-tests +test: vanilla-test unit-test + +vanilla-test: makefile-tests abcopt-tests seed-tests @echo "" - @echo " Passed \"make test\"." + @echo " Passed \"make vanilla-test\"." ifeq ($(ENABLE_VERIFIC),1) ifeq ($(YOSYS_NOVERIFIC),1) @echo " Ran tests without verific support due to YOSYS_NOVERIFIC=1." diff --git a/README.md b/README.md index 3b2f41768..df65a6a10 100644 --- a/README.md +++ b/README.md @@ -114,8 +114,8 @@ To build Yosys simply type 'make' in this directory. $ sudo make install Tests are located in the tests subdirectory and can be executed using the test -target. Note that you need gawk as well as a recent version of iverilog (i.e. -build from git). Then, execute tests via: +target. Note that you need gawk, a recent version of iverilog, and gtest. +Execute tests via: $ make test diff --git a/docs/source/yosys_internals/extending_yosys/test_suites.rst b/docs/source/yosys_internals/extending_yosys/test_suites.rst index 81a79e77f..c43dc3a84 100644 --- a/docs/source/yosys_internals/extending_yosys/test_suites.rst +++ b/docs/source/yosys_internals/extending_yosys/test_suites.rst @@ -8,7 +8,43 @@ Running the included test suite The Yosys source comes with a test suite to avoid regressions and keep everything working as expected. Tests can be run by calling ``make test`` from -the root Yosys directory. +the root Yosys directory. By default, this runs vanilla and unit tests. + +Vanilla tests +~~~~~~~~~~~~~ + +These make up the majority of our testing coverage. +They can be run with ``make vanilla-test`` and are based on calls to +make subcommands (``make makefile-tests``) and shell scripts +(``make seed-tests`` and ``make abcopt-tests``). Both use ``run-test.sh`` +files, but make-based tests only call ``tests/gen-tests-makefile.sh`` +to generate a makefile appropriate for the given directory, so only +afterwards when make is invoked do the tests actually run. + +Usually their structure looks something like this: +you write a .ys file that gets automatically run, +which runs a frontend like ``read_verilog`` or ``read_rtlil`` with +a relative path or a heredoc, then runs some commands including the command +under test, and then uses :doc:`/using_yosys/more_scripting/selections` +with ``-assert-count``. Usually it's unnecessary to "register" the test anywhere +as if it's similar to other tests it will be run together with the rest. + +Unit tests +~~~~~~~~~~ + +Running the unit tests requires the following additional packages: + +.. tab:: Ubuntu + + .. code:: console + + sudo apt-get install libgtest-dev + +.. tab:: macOS + + No additional requirements. + +Unit tests can be run with ``make unit-test``. Functional tests ~~~~~~~~~~~~~~~~ @@ -41,23 +77,6 @@ instructions `_. Then, set the :makevar:`ENABLE_FUNCTIONAL_TESTS` make variable when calling ``make test`` and the functional tests will be run as well. -Unit tests -~~~~~~~~~~ - -Running the unit tests requires the following additional packages: - -.. tab:: Ubuntu - - .. code:: console - - sudo apt-get install libgtest-dev - -.. tab:: macOS - - No additional requirements. - -Unit tests can be run with ``make unit-test``. - Docs tests ~~~~~~~~~~ From a6e33d99161d9fe0be662b51de376bfa3227e311 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 10 Feb 2026 00:38:43 +0000 Subject: [PATCH 30/87] 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 030e495c8b617ba59b4cd01393f85448450c373a Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Tue, 10 Feb 2026 15:05:17 +1300 Subject: [PATCH 31/87] test-build: Build and cache libyosys.so --- .github/workflows/test-build.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml index ab6eb3148..6cb60f1fd 100644 --- a/.github/workflows/test-build.yml +++ b/.github/workflows/test-build.yml @@ -71,7 +71,7 @@ jobs: mkdir build cd build make -f ../Makefile config-$CC - make -f ../Makefile -j$procs + make -f ../Makefile -j$procs ENABLE_LIBYOSYS=1 - name: Log yosys-config output run: | @@ -81,7 +81,7 @@ jobs: shell: bash run: | cd build - tar -cvf ../build.tar share/ yosys yosys-* + tar -cvf ../build.tar share/ yosys yosys-* libyosys.so - name: Store build artifact uses: actions/upload-artifact@v4 From 9f30f0e7d668f9caba7a53953152e4d981eadab8 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Tue, 10 Feb 2026 15:34:47 +1300 Subject: [PATCH 32/87] test-build: Don't rebuild OBJS --- .github/workflows/test-build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml index 6cb60f1fd..a14234925 100644 --- a/.github/workflows/test-build.yml +++ b/.github/workflows/test-build.yml @@ -131,7 +131,7 @@ jobs: - name: Run tests shell: bash run: | - make -j$procs test TARGETS= EXTRA_TARGETS= CONFIG=$CC + make -j$procs test OBJS= TARGETS= EXTRA_TARGETS= CONFIG=$CC - name: Report errors if: ${{ failure() }} From dfbef2fe24715bb1f8d74a0d10941afad3de3327 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 00:55:36 +0100 Subject: [PATCH 33/87] .github: run unit tests in build jobs, not test jobs --- .github/workflows/test-build.yml | 5 +++-- .github/workflows/test-sanitizers.yml | 4 ---- .github/workflows/test-verific.yml | 5 ----- 3 files changed, 3 insertions(+), 11 deletions(-) diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml index a14234925..06eb8187c 100644 --- a/.github/workflows/test-build.yml +++ b/.github/workflows/test-build.yml @@ -71,7 +71,8 @@ jobs: mkdir build cd build make -f ../Makefile config-$CC - make -f ../Makefile -j$procs ENABLE_LIBYOSYS=1 + make -f ../Makefile -j$procs + make -f ../Makefile unit-test -j$procs - name: Log yosys-config output run: | @@ -219,7 +220,7 @@ jobs: - name: Run tests shell: bash run: | - make -C docs test -j$procs + make -C docs vanilla-test -j$procs test-docs-build: name: Try build docs diff --git a/.github/workflows/test-sanitizers.yml b/.github/workflows/test-sanitizers.yml index c6b3d8db0..7650470c3 100644 --- a/.github/workflows/test-sanitizers.yml +++ b/.github/workflows/test-sanitizers.yml @@ -73,7 +73,3 @@ jobs: run: | find tests/**/*.err -print -exec cat {} \; - - name: Run unit tests - shell: bash - run: | - make -j$procs unit-test diff --git a/.github/workflows/test-verific.yml b/.github/workflows/test-verific.yml index feba3c0f9..cd2545cc8 100644 --- a/.github/workflows/test-verific.yml +++ b/.github/workflows/test-verific.yml @@ -80,11 +80,6 @@ jobs: run: | make -C sby run_ci - - name: Run unit tests - shell: bash - run: | - make -j$procs unit-test ENABLE_LTO=1 - test-pyosys: needs: pre-job if: ${{ needs.pre-job.outputs.should_skip != 'true' && github.repository == 'YosysHQ/Yosys' }} From 98c3f03497938dc1f314aa6fd8768e3a71eb4eb9 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 00:58:29 +0100 Subject: [PATCH 34/87] docs: clarify vanilla test run-test.sh --- docs/source/yosys_internals/extending_yosys/test_suites.rst | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/source/yosys_internals/extending_yosys/test_suites.rst b/docs/source/yosys_internals/extending_yosys/test_suites.rst index c43dc3a84..d3422b23a 100644 --- a/docs/source/yosys_internals/extending_yosys/test_suites.rst +++ b/docs/source/yosys_internals/extending_yosys/test_suites.rst @@ -27,7 +27,8 @@ which runs a frontend like ``read_verilog`` or ``read_rtlil`` with a relative path or a heredoc, then runs some commands including the command under test, and then uses :doc:`/using_yosys/more_scripting/selections` with ``-assert-count``. Usually it's unnecessary to "register" the test anywhere -as if it's similar to other tests it will be run together with the rest. +as if it's being added to an existing directory, depending +on how the ``run-test.sh`` in that directory works. Unit tests ~~~~~~~~~~ From a6a07fb39c0f3e79aea7b543ffb2e36a04e887b3 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 00:59:12 +0100 Subject: [PATCH 35/87] 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 36/87] 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 fe613f29b90337e1251ed2e038b78a4c299f967d Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 11:33:27 +0100 Subject: [PATCH 37/87] .github: move gtest to build dependencies --- .github/actions/setup-build-env/action.yml | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/.github/actions/setup-build-env/action.yml b/.github/actions/setup-build-env/action.yml index 60fe481e7..3c5465a9b 100644 --- a/.github/actions/setup-build-env/action.yml +++ b/.github/actions/setup-build-env/action.yml @@ -42,7 +42,7 @@ runs: if: runner.os == 'Linux' && inputs.get-build-deps == 'true' uses: awalsh128/cache-apt-pkgs-action@v1.6.0 with: - packages: bison clang flex libffi-dev libfl-dev libreadline-dev pkg-config tcl-dev zlib1g-dev + packages: bison clang flex libffi-dev libfl-dev libreadline-dev pkg-config tcl-dev zlib1g-dev libgtest-dev version: ${{ inputs.runs-on }}-buildys - name: Linux docs dependencies @@ -54,12 +54,12 @@ runs: # if updating test dependencies, make sure to update # docs/source/yosys_internals/extending_yosys/test_suites.rst to match. - - name: Linux test dependencies - if: runner.os == 'Linux' && inputs.get-test-deps == 'true' - uses: awalsh128/cache-apt-pkgs-action@v1.6.0 - with: - packages: libgtest-dev - version: ${{ inputs.runs-on }}-testys + # - name: Linux test dependencies + # if: runner.os == 'Linux' && inputs.get-test-deps == 'true' + # uses: awalsh128/cache-apt-pkgs-action@v1.6.0 + # with: + # packages: + # version: ${{ inputs.runs-on }}-testys - name: Install macOS Dependencies if: runner.os == 'macOS' From c4094e457b5013d64c60342444c7cd204382c3c7 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 11:34:54 +0100 Subject: [PATCH 38/87] 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 39/87] 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 3f1fbfdaee9049c0c274e73032e09266d6a36525 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 12:16:02 +0100 Subject: [PATCH 40/87] blifparse: add bounds check --- frontends/blif/blifparse.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 30512d324..350d7cafe 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -629,6 +629,7 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool goto try_next_value; } } + log_assert(i < lutptr->size()); lutptr->set(i, !strcmp(output, "0") ? RTLIL::State::S0 : RTLIL::State::S1); try_next_value:; } From 43a15113ff41f5a7ae40a70ca66a93e8b864f9f3 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 11 Feb 2026 12:07:41 +0100 Subject: [PATCH 41/87] aigerparse: add some bounds checks --- frontends/aiger/aigerparse.cc | 17 +++++++++++------ 1 file changed, 11 insertions(+), 6 deletions(-) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index 4df37c0cd..a27a23e79 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -286,10 +286,15 @@ end_of_header: RTLIL::IdString escaped_s = stringf("\\%s", s); RTLIL::Wire* wire; - if (c == 'i') wire = inputs[l1]; - else if (c == 'l') wire = latches[l1]; - else if (c == 'o') { + if (c == 'i') { + log_assert(l1 < inputs.size()); + wire = inputs[l1]; + } else if (c == 'l') { + log_assert(l1 < latches.size()); + wire = latches[l1]; + } else if (c == 'o') { wire = module->wire(escaped_s); + log_assert(l1 < outputs.size()); if (wire) { // Could have been renamed by a latch module->swap_names(wire, outputs[l1]); @@ -297,9 +302,9 @@ end_of_header: goto next; } wire = outputs[l1]; - } - else if (c == 'b') wire = bad_properties[l1]; - else log_abort(); + } else if (c == 'b') { + wire = bad_properties[l1]; + } else log_abort(); module->rename(wire, escaped_s); } From 2e03ee143478533968716478886634f610219f3a Mon Sep 17 00:00:00 2001 From: Lofty Date: Wed, 11 Feb 2026 11:46:17 +0000 Subject: [PATCH 42/87] aigerparse: sanity-check AIGER header --- frontends/aiger/aigerparse.cc | 3 +++ 1 file changed, 3 insertions(+) diff --git a/frontends/aiger/aigerparse.cc b/frontends/aiger/aigerparse.cc index a27a23e79..e55349aa7 100644 --- a/frontends/aiger/aigerparse.cc +++ b/frontends/aiger/aigerparse.cc @@ -657,6 +657,9 @@ void AigerReader::parse_aiger_binary() unsigned l1, l2, l3; std::string line; + if (M != I + L + A) + log_error("Binary AIGER input is malformed: maximum variable index M is %u, but number of inputs, latches and AND gates adds up to %u.\n", M, I + L + A); + // Parse inputs int digits = decimal_digits(I); for (unsigned i = 1; i <= I; ++i) { From 12ace45b89035e128ba41b10938ed2665ae30c2a Mon Sep 17 00:00:00 2001 From: Gus Smith Date: Wed, 22 Jun 2022 10:57:46 -0700 Subject: [PATCH 43/87] 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 44/87] 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 45/87] 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 46/87] 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 47/87] 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 48/87] 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 49/87] 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 50/87] 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 51/87] 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 52/87] 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 53/87] 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 54/87] 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 cc79c6a76173622aa75d1d8c1f2c206b601e24c2 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Thu, 12 Feb 2026 12:17:07 +0100 Subject: [PATCH 55/87] Support building out of tree, but keep always in tests/unit --- Makefile | 4 ++-- tests/unit/Makefile | 9 +++++---- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/Makefile b/Makefile index 7ce3153df..f20e63078 100644 --- a/Makefile +++ b/Makefile @@ -1013,11 +1013,11 @@ ystests: $(TARGETS) $(EXTRA_TARGETS) # Unit test unit-test: libyosys.so - @$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CC="$(CC)" CPPFLAGS="$(CPPFLAGS)" \ + @$(MAKE) -f $(UNITESTPATH)/Makefile CXX="$(CXX)" CC="$(CC)" CPPFLAGS="$(CPPFLAGS)" \ CXXFLAGS="$(CXXFLAGS)" LINKFLAGS="$(LINKFLAGS)" LIBS="$(LIBS)" ROOTPATH="$(CURDIR)" clean-unit-test: - @$(MAKE) -C $(UNITESTPATH) clean + @$(MAKE) -f $(UNITESTPATH)/Makefile clean install-dev: $(PROGRAM_PREFIX)yosys-config share $(INSTALL_SUDO) mkdir -p $(DESTDIR)$(BINDIR) diff --git a/tests/unit/Makefile b/tests/unit/Makefile index b275d7f41..e8f76cba9 100644 --- a/tests/unit/Makefile +++ b/tests/unit/Makefile @@ -18,10 +18,11 @@ endif EXTRAFLAGS := -lyosys -pthread -OBJTEST := objtest -BINTEST := bintest +MAKEFILE_DIR := $(dir $(abspath $(lastword $(MAKEFILE_LIST)))) +OBJTEST := $(MAKEFILE_DIR)objtest +BINTEST := $(MAKEFILE_DIR)bintest -ALLTESTFILE := $(shell find . -name '*Test.cc' | sed 's|^\./||' | tr '\n' ' ') +ALLTESTFILE := $(shell cd $(MAKEFILE_DIR) && find . -name '*Test.cc' | sed 's|^\./||' | tr '\n' ' ') TESTDIRS := $(sort $(dir $(ALLTESTFILE))) TESTS := $(addprefix $(BINTEST)/, $(basename $(ALLTESTFILE:%Test.cc=%Test.o))) @@ -34,7 +35,7 @@ $(BINTEST)/%: $(OBJTEST)/%.o | prepare $(CXX) -L$(ROOTPATH) $(RPATH) $(LINKFLAGS) -o $@ $^ $(LIBS) \ $(GTEST_LDFLAGS) $(EXTRAFLAGS) -$(OBJTEST)/%.o: $(basename $(subst $(OBJTEST),.,%)).cc | prepare +$(OBJTEST)/%.o: $(MAKEFILE_DIR)/%.cc | prepare $(CXX) -o $@ -c -I$(ROOTPATH) $(CPPFLAGS) $(CXXFLAGS) $(GTEST_CXXFLAGS) $^ .PHONY: prepare run-tests clean From c6e48f4bea903c08a99b4f5f6b91f30652155786 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Thu, 12 Feb 2026 14:06:08 +0100 Subject: [PATCH 56/87] These are tests from other Makefile --- .github/workflows/test-build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml index 06eb8187c..2a870cd29 100644 --- a/.github/workflows/test-build.yml +++ b/.github/workflows/test-build.yml @@ -220,7 +220,7 @@ jobs: - name: Run tests shell: bash run: | - make -C docs vanilla-test -j$procs + make -C docs test -j$procs test-docs-build: name: Try build docs From e5b3e9fc1f43c3c3e09ae0d4b143528a213cb1c9 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Thu, 12 Feb 2026 14:08:49 +0100 Subject: [PATCH 57/87] This one should run only vanilla-tests --- .github/workflows/test-build.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml index 2a870cd29..4f14e149c 100644 --- a/.github/workflows/test-build.yml +++ b/.github/workflows/test-build.yml @@ -132,7 +132,7 @@ jobs: - name: Run tests shell: bash run: | - make -j$procs test OBJS= TARGETS= EXTRA_TARGETS= CONFIG=$CC + make -j$procs vanilla-test OBJS= TARGETS= EXTRA_TARGETS= CONFIG=$CC - name: Report errors if: ${{ failure() }} From bb7aa7d208921fd8c1f438335822d661fe8e01ad Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Thu, 12 Feb 2026 14:56:45 +0100 Subject: [PATCH 58/87] Cleanup of yml files --- .github/actions/setup-build-env/action.yml | 9 --------- .github/workflows/test-build.yml | 2 +- 2 files changed, 1 insertion(+), 10 deletions(-) diff --git a/.github/actions/setup-build-env/action.yml b/.github/actions/setup-build-env/action.yml index 3c5465a9b..c9dc5fc22 100644 --- a/.github/actions/setup-build-env/action.yml +++ b/.github/actions/setup-build-env/action.yml @@ -52,15 +52,6 @@ runs: packages: graphviz xdot version: ${{ inputs.runs-on }}-docsys - # if updating test dependencies, make sure to update - # docs/source/yosys_internals/extending_yosys/test_suites.rst to match. - # - name: Linux test dependencies - # if: runner.os == 'Linux' && inputs.get-test-deps == 'true' - # uses: awalsh128/cache-apt-pkgs-action@v1.6.0 - # with: - # packages: - # version: ${{ inputs.runs-on }}-testys - - name: Install macOS Dependencies if: runner.os == 'macOS' shell: bash diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml index 4f14e149c..ebdeb15d8 100644 --- a/.github/workflows/test-build.yml +++ b/.github/workflows/test-build.yml @@ -132,7 +132,7 @@ jobs: - name: Run tests shell: bash run: | - make -j$procs vanilla-test OBJS= TARGETS= EXTRA_TARGETS= CONFIG=$CC + make -j$procs vanilla-test TARGETS= EXTRA_TARGETS= CONFIG=$CC - name: Report errors if: ${{ failure() }} 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 59/87] 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) From 1e852cef16f98692a8a284194ffe52bec06c7166 Mon Sep 17 00:00:00 2001 From: Chris Hathhorn Date: Thu, 12 Feb 2026 21:51:38 -0600 Subject: [PATCH 60/87] Fix segfault from shift with 0-width signed arg. Fixes #5684. --- kernel/calc.cc | 2 +- tests/various/const_shift_empty_arg.ys | 49 ++++++++++++++++++++++++++ 2 files changed, 50 insertions(+), 1 deletion(-) create mode 100644 tests/various/const_shift_empty_arg.ys diff --git a/kernel/calc.cc b/kernel/calc.cc index 9b0885db9..84ac100ab 100644 --- a/kernel/calc.cc +++ b/kernel/calc.cc @@ -291,7 +291,7 @@ static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Co if (pos < 0) result.set(i, vacant_bits); else if (pos >= BigInteger(GetSize(arg1))) - result.set(i, sign_ext ? arg1.back() : vacant_bits); + result.set(i, sign_ext && !arg1.empty() ? arg1.back() : vacant_bits); else result.set(i, arg1[pos.toInt()]); } diff --git a/tests/various/const_shift_empty_arg.ys b/tests/various/const_shift_empty_arg.ys new file mode 100644 index 000000000..4073e198d --- /dev/null +++ b/tests/various/const_shift_empty_arg.ys @@ -0,0 +1,49 @@ +# Regression test for #5684: const_shift_worker must not crash when arg1 is +# empty. + +read_json << EOF +{ + "modules": { + "sshl": { + "cells": { + "sshlCell": { + "connections": { + "A": [], + "B": [3], + "Y": [1] + }, + "parameters": { + "A_SIGNED": "1", + "A_WIDTH": "0", + "B_SIGNED": "0", + "B_WIDTH": "1", + "Y_WIDTH": "1" + }, + "port_directions": { + "A": "input", + "B": "input", + "Y": "output" + }, + "type": "$sshl" + } + }, + "ports": { + "A": { + "bits": [], + "direction": "input" + }, + "B": { + "bits": [3], + "direction": "input" + }, + "Y": { + "bits": [1], + "direction": "output" + } + } + } + } +} +EOF + +eval -set B 0 -show Y sshl From c7d88ded9424501d9196f84913a6dd31762ecab7 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 13 Feb 2026 14:21:41 +0100 Subject: [PATCH 61/87] Make version bump automatic --- Makefile | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/Makefile b/Makefile index 0f76cdbef..4c37bfb8d 100644 --- a/Makefile +++ b/Makefile @@ -161,7 +161,17 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.62+55 +YOSYS_VER := 0.62 + +ifneq (, $(shell command -v git 2>/dev/null)) +ifneq (, $(shell git rev-parse --git-dir 2>/dev/null)) + GIT_COMMIT_COUNT := $(shell git rev-list --count $(shell git describe --tags --abbrev=0)..HEAD 2>/dev/null) + ifneq ($(GIT_COMMIT_COUNT),0) + YOSYS_VER := $(YOSYS_VER)+$(GIT_COMMIT_COUNT) + endif +endif +endif + 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) @@ -185,9 +195,6 @@ endif OBJS = kernel/version_$(GIT_REV).o -bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 7326bb7.. | wc -l`/;" Makefile - ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) # set ABCEXTERNAL = to use an external ABC instance From adf8b6b0d88aff391255888a48501d8a9a696031 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 13 Feb 2026 14:22:10 +0100 Subject: [PATCH 62/87] Add +post to version if from tarbal --- Makefile | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Makefile b/Makefile index 4c37bfb8d..78066b2e0 100644 --- a/Makefile +++ b/Makefile @@ -169,6 +169,8 @@ ifneq (, $(shell git rev-parse --git-dir 2>/dev/null)) ifneq ($(GIT_COMMIT_COUNT),0) YOSYS_VER := $(YOSYS_VER)+$(GIT_COMMIT_COUNT) endif +else + YOSYS_VER := $(YOSYS_VER)+post endif endif From 0090aa96b658de655e10258f7e8b39bae54746fe Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 13 Feb 2026 14:22:33 +0100 Subject: [PATCH 63/87] Remove version bump action --- .github/workflows/version.yml | 34 ---------------------------------- 1 file changed, 34 deletions(-) delete mode 100644 .github/workflows/version.yml diff --git a/.github/workflows/version.yml b/.github/workflows/version.yml deleted file mode 100644 index 78d34db46..000000000 --- a/.github/workflows/version.yml +++ /dev/null @@ -1,34 +0,0 @@ -name: Bump version - -on: - workflow_dispatch: - schedule: - - cron: '0 0 * * *' - -jobs: - bump-version: - if: github.repository == 'YosysHQ/Yosys' - runs-on: ubuntu-latest - steps: - - name: Checkout - uses: actions/checkout@v4 - with: - fetch-depth: 0 - submodules: true - persist-credentials: false - - name: Take last commit - id: log - run: echo "message=$(git log --no-merges -1 --oneline)" >> $GITHUB_OUTPUT - - name: Bump version - if: ${{ !contains(steps.log.outputs.message, 'Bump version') }} - run: | - make bumpversion - git config --local user.email "41898282+github-actions[bot]@users.noreply.github.com" - git config --local user.name "github-actions[bot]" - git add Makefile - git commit -m "Bump version" - - name: Push changes # push the output folder to your repo - if: ${{ !contains(steps.log.outputs.message, 'Bump version') }} - uses: ad-m/github-push-action@master - with: - github_token: ${{ secrets.GITHUB_TOKEN }} From e6e57b33e36256f86697950ba6af803225c8b7e3 Mon Sep 17 00:00:00 2001 From: nella Date: Sun, 15 Feb 2026 09:00:04 +0100 Subject: [PATCH 64/87] document abc --keep-going pdr [sc-220]. --- backends/aiger/aiger.cc | 5 +++ .../more_scripting/model_checking.rst | 36 +++++++++++++++++-- passes/cmds/rename.cc | 11 ++++-- 3 files changed, 46 insertions(+), 6 deletions(-) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 95f4c19e2..62c79f60b 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -931,6 +931,11 @@ struct AigerBackend : public Backend { log("\n"); log(" -ywmap \n"); log(" write a map file for conversion to and from yosys witness traces.\n"); + log(" The generated JSON map includes \"asserts\" and \"assumes\" arrays\n"); + log(" containing the hierarchical witness paths of the corresponding\n"); + log(" $assert and $assume cells. This enables downstream tools to map\n"); + log(" AIGER bad-state properties and invariant constraints back to\n"); + log(" individual formal properties by name.\n"); log("\n"); log(" -I, -O, -B, -L\n"); log(" If the design contains no input/output/assert/flip-flop then create one\n"); diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst index 799c99b6f..da9193a6f 100644 --- a/docs/source/using_yosys/more_scripting/model_checking.rst +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -3,9 +3,9 @@ Symbolic model checking .. todo:: check text context -.. note:: - - While it is possible to perform model checking directly in Yosys, it +.. note:: + + While it is possible to perform model checking directly in Yosys, it is highly recommended to use SBY or EQY for formal hardware verification. Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or @@ -117,3 +117,33 @@ Result with fixed :file:`axis_master.v`: Solving problem with 159144 variables and 441626 clauses.. SAT proof finished - no model found: SUCCESS! + +Witness framework and per-property tracking +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ + +When using AIGER-based formal verification flows (such as the ``abc`` engine in +SymbiYosys), Yosys provides infrastructure for tracking individual formal +properties through the verification pipeline. + +The ``rename -witness`` pass (run automatically by ``prep``) assigns public +names to all cells that participate in the witness framework: + +- Witness signal cells: ``$anyconst``, ``$anyseq``, ``$anyinit``, + ``$allconst``, ``$allseq`` +- Formal property cells: ``$assert``, ``$assume``, ``$cover``, ``$live``, + ``$fair``, ``$check`` + +These public names allow downstream tools to refer to individual properties by +their hierarchical path rather than by anonymous internal identifiers. + +The ``write_aiger -ywmap`` option generates a JSON map file that includes, among +other things, ``"asserts"`` and ``"assumes"`` arrays. Each entry contains the +hierarchical witness path of the corresponding ``$assert`` or ``$assume`` cell. +This lets tools such as SymbiYosys map AIGER bad-state properties and invariant +constraints back to individual formal properties, enabling features like +per-property pass/fail reporting (e.g. ``abc pdr`` with ``--keep-going`` mode). + +The ``write_smt2`` backend similarly uses the public witness names when emitting +``yosys-smt2-assert`` and ``yosys-smt2-assume`` comments. Cells whose +``hdlname`` attribute contains the ``_witness_`` marker are treated as having +private names for comment purposes, keeping solver output clean. diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index 078ffb769..f87396743 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -263,9 +263,14 @@ struct RenamePass : public Pass { log(" rename -witness\n"); log("\n"); log("Assigns auto-generated names to all $any*/$all* output wires and containing\n"); - log("cells that do not have a public name. This ensures that, during formal\n"); - log("verification, a solver-found trace can be fully specified using a public\n"); - log("hierarchical names.\n"); + log("cells that do not have a public name. Also renames formal property cells\n"); + log("($assert, $assume, $cover, $live, $fair, $check) that have private names,\n"); + log("giving them public witness-trackable names.\n"); + log("\n"); + log("This ensures that, during formal verification, a solver-found trace can be\n"); + log("fully specified using public hierarchical names, and that individual property\n"); + log("results can be tracked by name in flows that support per-property reporting\n"); + log("(e.g. SBY with abc pdr in --keep-going mode).\n"); log("\n"); log("\n"); log(" rename -hide [selection]\n"); From 63068f9b8f1084d859ab35d454eaa3e74fb3e227 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 16 Feb 2026 16:44:33 +0100 Subject: [PATCH 65/87] count relative to version tag, and ignore non existing --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 78066b2e0..9451e1a6c 100644 --- a/Makefile +++ b/Makefile @@ -165,7 +165,7 @@ YOSYS_VER := 0.62 ifneq (, $(shell command -v git 2>/dev/null)) ifneq (, $(shell git rev-parse --git-dir 2>/dev/null)) - GIT_COMMIT_COUNT := $(shell git rev-list --count $(shell git describe --tags --abbrev=0)..HEAD 2>/dev/null) + GIT_COMMIT_COUNT := $(or $(shell git rev-list --count v$(YOSYS_VER)..HEAD 2>/dev/null),0) ifneq ($(GIT_COMMIT_COUNT),0) YOSYS_VER := $(YOSYS_VER)+$(GIT_COMMIT_COUNT) endif From 81ea922512a5ce7e6fdba1f4ff0c23ce4c3b743a Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Mon, 16 Feb 2026 16:54:26 +0100 Subject: [PATCH 66/87] sat: use the same cell import warnings as equiv --- passes/sat/sat.cc | 7 ++----- 1 file changed, 2 insertions(+), 5 deletions(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index ffebdd01c..c143e938e 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -27,6 +27,7 @@ #include "kernel/satgen.h" #include "kernel/yosys.h" #include "kernel/log_help.h" +#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -227,16 +228,12 @@ struct SatHelper int import_cell_counter = 0; for (auto cell : module->cells()) if (design->selected(module, cell)) { - // log("Import cell: %s\n", RTLIL::id2cstr(cell->name)); if (satgen.importCell(cell, timestep)) { for (auto &p : cell->connections()) if (ct.cell_output(cell->type, p.first)) show_drivers.insert(sigmap(p.second), cell); import_cell_counter++; - } else if (ignore_unknown_cells) - log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type)); - else - log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type)); + } else report_missing_model(ignore_unknown_cells, cell); } log("Imported %d cells to SAT database.\n", import_cell_counter); From 77f64de9979e957452be2a4f2f428f0607791b63 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Mon, 16 Feb 2026 17:01:09 +0100 Subject: [PATCH 67/87] satgen: move report_missing_model here from equiv.h --- kernel/satgen.cc | 20 ++++++++++++++++++++ kernel/satgen.h | 2 ++ passes/equiv/equiv.h | 15 --------------- passes/sat/sat.cc | 1 - 4 files changed, 22 insertions(+), 16 deletions(-) diff --git a/kernel/satgen.cc b/kernel/satgen.cc index b8b850bb3..7fbcba1b2 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -19,6 +19,7 @@ #include "kernel/satgen.h" #include "kernel/ff.h" +#include "kernel/yosys_common.h" USING_YOSYS_NAMESPACE @@ -1387,3 +1388,22 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) // .. and all sequential cells with asynchronous inputs return false; } + +namespace Yosys { + +void report_missing_model(bool warn_only, RTLIL::Cell* cell) +{ + std::string s; + if (cell->is_builtin_ff()) + s = stringf("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); + else + s = stringf("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); + + if (warn_only) { + log_formatted_warning_noprefix(s); + } else { + log_formatted_error(s); + } +} + +} diff --git a/kernel/satgen.h b/kernel/satgen.h index 7815847b3..9ad940585 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -292,6 +292,8 @@ struct SatGen bool importCell(RTLIL::Cell *cell, int timestep = -1); }; +void report_missing_model(bool warn_only, RTLIL::Cell* cell); + YOSYS_NAMESPACE_END #endif diff --git a/passes/equiv/equiv.h b/passes/equiv/equiv.h index 9641e65a7..95d4b25e9 100644 --- a/passes/equiv/equiv.h +++ b/passes/equiv/equiv.h @@ -8,21 +8,6 @@ YOSYS_NAMESPACE_BEGIN -static void report_missing_model(bool warn_only, RTLIL::Cell* cell) -{ - std::string s; - if (cell->is_builtin_ff()) - s = stringf("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type)); - else - s = stringf("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type)); - - if (warn_only) { - log_formatted_warning_noprefix(s); - } else { - log_formatted_error(s); - } -} - struct EquivBasicConfig { bool model_undef = false; int max_seq = 1; diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index c143e938e..203147172 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -27,7 +27,6 @@ #include "kernel/satgen.h" #include "kernel/yosys.h" #include "kernel/log_help.h" -#include "passes/equiv/equiv.h" USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN From 2b4f481850d7ddc160e34d68e201917e508e25c7 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 18 Feb 2026 09:24:41 +0100 Subject: [PATCH 68/87] Cleanup docs. --- backends/aiger/aiger.cc | 9 +++---- .../more_scripting/model_checking.rst | 24 +++++++++---------- passes/cmds/rename.cc | 13 ++++------ 3 files changed, 19 insertions(+), 27 deletions(-) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 62c79f60b..0c49e84b8 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -930,12 +930,9 @@ struct AigerBackend : public Backend { log(" make indexes zero based, enable using map files with smt solvers.\n"); log("\n"); log(" -ywmap \n"); - log(" write a map file for conversion to and from yosys witness traces.\n"); - log(" The generated JSON map includes \"asserts\" and \"assumes\" arrays\n"); - log(" containing the hierarchical witness paths of the corresponding\n"); - log(" $assert and $assume cells. This enables downstream tools to map\n"); - log(" AIGER bad-state properties and invariant constraints back to\n"); - log(" individual formal properties by name.\n"); + log(" write a map file for conversion to and from yosys witness traces,\n"); + log(" also allows for mapping AIGER bad-state properties and invariant\n"); + log(" constraints back to individual formal properties by name.\n"); log("\n"); log(" -I, -O, -B, -L\n"); log(" If the design contains no input/output/assert/flip-flop then create one\n"); diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst index da9193a6f..b418f6aff 100644 --- a/docs/source/using_yosys/more_scripting/model_checking.rst +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -121,29 +121,29 @@ Result with fixed :file:`axis_master.v`: Witness framework and per-property tracking ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When using AIGER-based formal verification flows (such as the ``abc`` engine in -SymbiYosys), Yosys provides infrastructure for tracking individual formal +When using AIGER-based formal verification flows (such as the `abc` engine in +SBY), Yosys provides infrastructure for tracking individual formal properties through the verification pipeline. -The ``rename -witness`` pass (run automatically by ``prep``) assigns public +The `rename -witness` pass (run automatically by `prep`) assigns public names to all cells that participate in the witness framework: -- Witness signal cells: ``$anyconst``, ``$anyseq``, ``$anyinit``, - ``$allconst``, ``$allseq`` -- Formal property cells: ``$assert``, ``$assume``, ``$cover``, ``$live``, - ``$fair``, ``$check`` +- Witness signal cells: `$anyconst`, `$anyseq`, `$anyinit`, + `$allconst`, `$allseq` +- Formal property cells: `$assert`, `$assume`, `$cover`, `$live`, + `$fair`, `$check` These public names allow downstream tools to refer to individual properties by their hierarchical path rather than by anonymous internal identifiers. -The ``write_aiger -ywmap`` option generates a JSON map file that includes, among +The `write_aiger -ywmap` option generates a JSON map file that includes, among other things, ``"asserts"`` and ``"assumes"`` arrays. Each entry contains the -hierarchical witness path of the corresponding ``$assert`` or ``$assume`` cell. -This lets tools such as SymbiYosys map AIGER bad-state properties and invariant +hierarchical witness path of the corresponding `$assert` or `$assume` cell. +This lets tools such as SBY map AIGER bad-state properties and invariant constraints back to individual formal properties, enabling features like -per-property pass/fail reporting (e.g. ``abc pdr`` with ``--keep-going`` mode). +per-property pass/fail reporting (e.g. `abc pdr` with ``--keep-going`` mode). -The ``write_smt2`` backend similarly uses the public witness names when emitting +The `write_smt2` backend similarly uses the public witness names when emitting ``yosys-smt2-assert`` and ``yosys-smt2-assume`` comments. Cells whose ``hdlname`` attribute contains the ``_witness_`` marker are treated as having private names for comment purposes, keeping solver output clean. diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index f87396743..836dfe5b1 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -262,15 +262,10 @@ struct RenamePass : public Pass { log("\n"); log(" rename -witness\n"); log("\n"); - log("Assigns auto-generated names to all $any*/$all* output wires and containing\n"); - log("cells that do not have a public name. Also renames formal property cells\n"); - log("($assert, $assume, $cover, $live, $fair, $check) that have private names,\n"); - log("giving them public witness-trackable names.\n"); - log("\n"); - log("This ensures that, during formal verification, a solver-found trace can be\n"); - log("fully specified using public hierarchical names, and that individual property\n"); - log("results can be tracked by name in flows that support per-property reporting\n"); - log("(e.g. SBY with abc pdr in --keep-going mode).\n"); + log("Assigns auto-generated names to objects used in formal verification\n"); + log("that do not have a public name. This applies to all formal property\n"); + log("cells ($assert, $assume, $cover, $live, $fair, $check), $any*/$all*\n"); + log("output wires, and their containing cells.\n"); log("\n"); log("\n"); log(" rename -hide [selection]\n"); From 01e89a8f9e8ea16d2bab74f725c19d6348fc5f46 Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 18 Feb 2026 09:29:35 +0100 Subject: [PATCH 69/87] Remove cell mentions. --- .../more_scripting/model_checking.rst | 17 ++++++++--------- passes/cmds/rename.cc | 7 +++---- 2 files changed, 11 insertions(+), 13 deletions(-) diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst index b418f6aff..02400d5d8 100644 --- a/docs/source/using_yosys/more_scripting/model_checking.rst +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -136,14 +136,13 @@ names to all cells that participate in the witness framework: These public names allow downstream tools to refer to individual properties by their hierarchical path rather than by anonymous internal identifiers. -The `write_aiger -ywmap` option generates a JSON map file that includes, among -other things, ``"asserts"`` and ``"assumes"`` arrays. Each entry contains the -hierarchical witness path of the corresponding `$assert` or `$assume` cell. -This lets tools such as SBY map AIGER bad-state properties and invariant -constraints back to individual formal properties, enabling features like -per-property pass/fail reporting (e.g. `abc pdr` with ``--keep-going`` mode). +The `write_aiger -ywmap` option generates a map file for conversion to and from +Yosys witness traces, and also allows for mapping AIGER bad-state properties and +invariant constraints back to individual formal properties by name. This enables +features like per-property pass/fail reporting (e.g. `abc pdr` with +``--keep-going`` mode). The `write_smt2` backend similarly uses the public witness names when emitting -``yosys-smt2-assert`` and ``yosys-smt2-assume`` comments. Cells whose -``hdlname`` attribute contains the ``_witness_`` marker are treated as having -private names for comment purposes, keeping solver output clean. +SMT2 comments. Cells whose ``hdlname`` attribute contains the ``_witness_`` +marker are treated as having private names for comment purposes, keeping solver +output clean. diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc index 836dfe5b1..a07d588c4 100644 --- a/passes/cmds/rename.cc +++ b/passes/cmds/rename.cc @@ -254,10 +254,9 @@ struct RenamePass : public Pass { log("\n"); log(" rename -enumerate [-pattern ] [selection]\n"); log("\n"); - log("Assign short auto-generated names to all selected wires and cells with private\n"); - log("names. The -pattern option can be used to set the pattern for the new names.\n"); - log("The character %% in the pattern is replaced with a integer number. The default\n"); - log("pattern is '_%%_'.\n"); + log("Assigns auto-generated names to objects used in formal verification\n"); + log("that do not have a public name. This applies to all formal property\n"); + log("cells, $any*/$all* output wires, and their containing cells.\n"); log("\n"); log("\n"); log(" rename -witness\n"); From 62f19cb3a96a3884e83184b994ff3be51eff7221 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 18 Feb 2026 12:20:36 +0100 Subject: [PATCH 70/87] modtools: fix port_del db erase --- kernel/modtools.h | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/kernel/modtools.h b/kernel/modtools.h index a081c7556..6dd7600e9 100644 --- a/kernel/modtools.h +++ b/kernel/modtools.h @@ -94,8 +94,11 @@ struct ModIndex : public RTLIL::Monitor { for (int i = 0; i < GetSize(sig); i++) { RTLIL::SigBit bit = sigmap(sig[i]); - if (bit.wire) + if (bit.wire) { database[bit].ports.erase(PortInfo(cell, port, i)); + if (!database[bit].is_input && !database[bit].is_output && database[bit].ports.empty()) + database.erase(bit); + } } } From 5bb31485b75587dd6b751f910a899775391cf144 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 18 Feb 2026 13:34:36 +0100 Subject: [PATCH 71/87] Display repo and branch when applicable --- Makefile | 21 +++++++++++++++++++++ 1 file changed, 21 insertions(+) diff --git a/Makefile b/Makefile index 9451e1a6c..588606e2f 100644 --- a/Makefile +++ b/Makefile @@ -802,9 +802,30 @@ endif $(Q) mkdir -p $(dir $@) $(P) $(CXX) -o $@ -c $(CPPFLAGS) $(CXXFLAGS) $< +YOSYS_REPO := +ifneq (, $(shell command -v git 2>/dev/null)) +ifneq (, $(shell git rev-parse --git-dir 2>/dev/null)) + GIT_REMOTE := $(strip $(shell git config --get remote.origin.url 2>/dev/null | $(AWK) '{print tolower($$0)}')) + ifneq ($(strip $(GIT_REMOTE)),) + YOSYS_REPO := $(strip $(shell echo $(GIT_REMOTE) | $(AWK) -F '[:/]' '{gsub(/\.git$$/, "", $$NF); printf "%s/%s", $$(NF-1), $$NF}')) + endif + ifeq ($(strip $(YOSYS_REPO)),yosyshq/yosys) + YOSYS_REPO := + endif + GIT_BRANCH := $(shell git rev-parse --abbrev-ref HEAD 2>/dev/null) + ifeq ($(filter main HEAD release/v%,$(GIT_BRANCH)),) + YOSYS_REPO := $(YOSYS_REPO) at $(GIT_BRANCH) + endif + YOSYS_REPO := $(strip $(YOSYS_REPO)) +endif +endif + YOSYS_GIT_STR := $(GIT_REV)$(GIT_DIRTY) YOSYS_COMPILER := $(notdir $(CXX)) $(shell $(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1) $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS)) YOSYS_VER_STR := Yosys $(YOSYS_VER) (git sha1 $(YOSYS_GIT_STR), $(YOSYS_COMPILER)) +ifneq ($(strip $(YOSYS_REPO)),) + YOSYS_VER_STR := $(YOSYS_VER_STR) [$(YOSYS_REPO)] +endif kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile $(P) rm -f kernel/version_*.o kernel/version_*.d kernel/version_*.cc From c75d80905a8e8e358e9604cf9823299d103d5dca Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 18 Feb 2026 21:20:13 +0100 Subject: [PATCH 72/87] modtools: fix database sanity on wire name swap --- kernel/modtools.h | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/kernel/modtools.h b/kernel/modtools.h index 6dd7600e9..cf68693bc 100644 --- a/kernel/modtools.h +++ b/kernel/modtools.h @@ -28,6 +28,22 @@ YOSYS_NAMESPACE_BEGIN struct ModIndex : public RTLIL::Monitor { + struct PointerOrderedSigBit : public RTLIL::SigBit { + PointerOrderedSigBit(SigBit s) { + wire = s.wire; + if (wire) + offset = s.offset; + else + data = s.data; + } + inline bool operator<(const RTLIL::SigBit &other) const { + if (wire == other.wire) + return wire ? (offset < other.offset) : (data < other.data); + if (wire != nullptr && other.wire != nullptr) + return wire < other.wire; // look here + return (wire != nullptr) < (other.wire != nullptr); + } + }; struct PortInfo { RTLIL::Cell* cell; RTLIL::IdString port; @@ -77,7 +93,7 @@ struct ModIndex : public RTLIL::Monitor SigMap sigmap; RTLIL::Module *module; - std::map database; + std::map database; int auto_reload_counter; bool auto_reload_module; From abc7563a35cf4f9927d19cd0f430ff6f6c606f94 Mon Sep 17 00:00:00 2001 From: "Emil J. Tywoniak" Date: Wed, 18 Feb 2026 22:15:44 +0100 Subject: [PATCH 73/87] modtools: add ModIndex unit test --- kernel/modtools.h | 12 ++++++-- tests/unit/kernel/modindexTest.cc | 47 +++++++++++++++++++++++++++++++ 2 files changed, 56 insertions(+), 3 deletions(-) create mode 100644 tests/unit/kernel/modindexTest.cc diff --git a/kernel/modtools.h b/kernel/modtools.h index cf68693bc..5cd8e3cb2 100644 --- a/kernel/modtools.h +++ b/kernel/modtools.h @@ -151,11 +151,11 @@ struct ModIndex : public RTLIL::Monitor } } - void check() + bool ok() { #ifndef NDEBUG if (auto_reload_module) - return; + return true; for (auto it : database) log_assert(it.first == sigmap(it.first)); @@ -175,11 +175,17 @@ struct ModIndex : public RTLIL::Monitor else if (!(it.second == database_bak.at(it.first))) log("ModuleIndex::check(): Different content for database[%s].\n", log_signal(it.first)); - log_assert(database == database_bak); + return false; } + return true; #endif } + void check() + { + log_assert(ok()); + } + void notify_connect(RTLIL::Cell *cell, RTLIL::IdString port, const RTLIL::SigSpec &old_sig, const RTLIL::SigSpec &sig) override { log_assert(module == cell->module); diff --git a/tests/unit/kernel/modindexTest.cc b/tests/unit/kernel/modindexTest.cc new file mode 100644 index 000000000..1921c9a93 --- /dev/null +++ b/tests/unit/kernel/modindexTest.cc @@ -0,0 +1,47 @@ +#include + +#include "kernel/modtools.h" +#include "kernel/rtlil.h" + +YOSYS_NAMESPACE_BEGIN + +TEST(ModIndexSwapTest, has) +{ + Design* d = new Design; + Module* m = d->addModule("$m"); + Wire* o = m->addWire("$o", 2); + o->port_input = true; + Wire* i = m->addWire("$i", 2); + i->port_input = true; + m->fixup_ports(); + m->addNot("$not", i, o); + auto mi = ModIndex(m); + mi.reload_module(); + for (auto [sb, info] : mi.database) { + EXPECT_TRUE(mi.database.find(sb) != mi.database.end()); + } + m->swap_names(i, o); + for (auto [sb, info] : mi.database) { + EXPECT_TRUE(mi.database.find(sb) != mi.database.end()); + } +} + +TEST(ModIndexDeleteTest, has) +{ + if (log_files.empty()) log_files.emplace_back(stdout); + Design* d = new Design; + Module* m = d->addModule("$m"); + Wire* w = m->addWire("$w"); + Wire* o = m->addWire("$o"); + o->port_output = true; + m->fixup_ports(); + Cell* not_ = m->addNotGate("$not", w, o); + auto mi = ModIndex(m); + mi.reload_module(); + mi.dump_db(); + Wire* a = m->addWire("\\a"); + not_->setPort(ID::A, a); + EXPECT_TRUE(mi.ok()); +} + +YOSYS_NAMESPACE_END From 094481739fa862669f1bb36e1c7bdbd255e4523c Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 18 Oct 2025 12:58:25 +1300 Subject: [PATCH 74/87] memory_libmap: Add -force-params Reduce complexity for adi brams by unconditionally providing the WIDTH and ABITS parameters. --- passes/memory/memory_libmap.cc | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/passes/memory/memory_libmap.cc b/passes/memory/memory_libmap.cc index c3c10363b..87adaa26d 100644 --- a/passes/memory/memory_libmap.cc +++ b/passes/memory/memory_libmap.cc @@ -39,6 +39,7 @@ struct PassOptions { bool no_auto_distributed; bool no_auto_block; bool no_auto_huge; + bool force_params; double logic_cost_rom; double logic_cost_ram; }; @@ -1859,7 +1860,7 @@ void MemMapping::emit_port(const MemConfig &cfg, std::vector &cells, cons cell->setParam(stringf("\\PORT_%s_WR_BE_WIDTH", name), GetSize(hw_wren)); } else { cell->setPort(stringf("\\PORT_%s_WR_EN", name), hw_wren); - if (cfg.def->byte != 0 && cfg.def->width_mode != WidthMode::Single) + if (cfg.def->byte != 0 && (cfg.def->width_mode != WidthMode::Single || opts.force_params)) cell->setParam(stringf("\\PORT_%s_WR_EN_WIDTH", name), GetSize(hw_wren)); } } @@ -2068,8 +2069,10 @@ void MemMapping::emit(const MemConfig &cfg) { std::vector cells; for (int rd = 0; rd < cfg.repl_d; rd++) { Cell *cell = mem.module->addCell(stringf("%s.%d.%d", mem.memid, rp, rd), cfg.def->id); - if (cfg.def->width_mode == WidthMode::Global) + if (cfg.def->width_mode == WidthMode::Global || opts.force_params) cell->setParam(ID::WIDTH, cfg.def->dbits[cfg.base_width_log2]); + if (opts.force_params) + cell->setParam(ID::ABITS, cfg.def->abits); if (cfg.def->widthscale) { std::vector val; for (auto &bit: init_swz.bits[rd]) @@ -2179,6 +2182,9 @@ struct MemoryLibMapPass : public Pass { log(" Disables automatic mapping of given kind of RAMs. Manual mapping\n"); log(" (using ram_style or other attributes) is still supported.\n"); log("\n"); + log(" -force-params\n"); + log(" Always generate memories with WIDTH and ABITS parameters.\n"); + log("\n"); } void execute(std::vector args, RTLIL::Design *design) override { @@ -2188,6 +2194,7 @@ struct MemoryLibMapPass : public Pass { opts.no_auto_distributed = false; opts.no_auto_block = false; opts.no_auto_huge = false; + opts.force_params = false; opts.logic_cost_ram = 1.0; opts.logic_cost_rom = 1.0/16.0; log_header(design, "Executing MEMORY_LIBMAP pass (mapping memories to cells).\n"); @@ -2214,6 +2221,10 @@ struct MemoryLibMapPass : public Pass { opts.no_auto_huge = true; continue; } + if (args[argidx] == "-force-params") { + opts.force_params = true; + continue; + } if (args[argidx] == "-logic-cost-rom" && argidx+1 < args.size()) { opts.logic_cost_rom = strtod(args[++argidx].c_str(), nullptr); continue; From 68e47ebcfeff498bba742c6eb3c9bbd6ed41589a Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 20 Feb 2026 15:23:45 +0100 Subject: [PATCH 75/87] CI: WASI - Applying YoWASP changes to script --- .github/workflows/extra-builds.yml | 1 + 1 file changed, 1 insertion(+) diff --git a/.github/workflows/extra-builds.yml b/.github/workflows/extra-builds.yml index 5d0ac72d4..8af99def8 100644 --- a/.github/workflows/extra-builds.yml +++ b/.github/workflows/extra-builds.yml @@ -103,6 +103,7 @@ jobs: ENABLE_ZLIB := 0 CXXFLAGS += -I$(pwd)/flex-prefix/include + LINKFLAGS += -Wl,-z,stack-size=8388608 -Wl,--stack-first -Wl,--strip-all END make -C build -f ../Makefile CXX=clang -j$(nproc) From 2386923b8fe9563f318c2c4d47ef6caaca5e9dc0 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 20 Feb 2026 12:34:41 +1300 Subject: [PATCH 76/87] gowin: Fix bram ADA byte enables --- techlibs/gowin/brams_map.v | 2 +- techlibs/gowin/brams_map_gw5a.v | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/techlibs/gowin/brams_map.v b/techlibs/gowin/brams_map.v index 774896e79..6187eadac 100644 --- a/techlibs/gowin/brams_map.v +++ b/techlibs/gowin/brams_map.v @@ -205,7 +205,7 @@ output [PORT_A_WIDTH-1:0] PORT_B_RD_DATA; wire RSTA = OPTION_RESET_MODE == "SYNC" ? PORT_A_RD_SRST : PORT_A_RD_ARST; wire RSTB = OPTION_RESET_MODE == "SYNC" ? PORT_B_RD_SRST : PORT_B_RD_ARST; -wire [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_B_WR_BE); +wire [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_A_WR_BE); wire [13:0] ADB = `addrbe(PORT_B_WIDTH, PORT_B_ADDR, PORT_B_WR_BE); generate diff --git a/techlibs/gowin/brams_map_gw5a.v b/techlibs/gowin/brams_map_gw5a.v index 547b0d1d1..8bc77bf4f 100644 --- a/techlibs/gowin/brams_map_gw5a.v +++ b/techlibs/gowin/brams_map_gw5a.v @@ -205,7 +205,7 @@ output [PORT_A_WIDTH-1:0] PORT_B_RD_DATA; wire RSTA = OPTION_RESET_MODE == "SYNC" ? PORT_A_RD_SRST : PORT_A_RD_ARST; wire RSTB = OPTION_RESET_MODE == "SYNC" ? PORT_B_RD_SRST : PORT_B_RD_ARST; -wire [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_B_WR_BE); +wire [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_A_WR_BE); wire [13:0] ADB = `addrbe(PORT_B_WIDTH, PORT_B_ADDR, PORT_B_WR_BE); generate From fd311c55019b5f96b54b8c72aa0294863b7e9eb4 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Fri, 20 Feb 2026 12:42:55 +1300 Subject: [PATCH 77/87] tests/arch/gowin: Add wr_en test --- tests/arch/gowin/bug5688.ys | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 tests/arch/gowin/bug5688.ys diff --git a/tests/arch/gowin/bug5688.ys b/tests/arch/gowin/bug5688.ys new file mode 100644 index 000000000..39019c4d6 --- /dev/null +++ b/tests/arch/gowin/bug5688.ys @@ -0,0 +1,31 @@ +read_verilog << EOT +`default_nettype none + +module top ( + input wire clk, + input wire [9:0] rd_addr, + output reg [15:0] rd_data, + input wire [9:0] wr_addr, + input wire [15:0] wr_data, + input wire wr_en +); + + (* ram_style = "block" *) reg [15:0] mem [0:1023]; + + // Read port — separate always block + always @(posedge clk) begin + rd_data <= mem[rd_addr]; + end + + // Write port — separate always block + always @(posedge clk) begin + if (wr_en) + mem[wr_addr] <= wr_data; + end + +endmodule + +EOT +synth_gowin -top top +splitnets +select -assert-any top/mem.0.0 %ci*:+DPX9B[ADA]:+DFF:+IBUF i:wr_en %i From b51110a50b484212fc04f46f95bd8678ac0364dc Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 23 Feb 2026 09:01:55 +0100 Subject: [PATCH 78/87] Build various Verific configurations --- .github/workflows/test-verific-cfg.yml | 109 +++++++++++++++++++++++++ 1 file changed, 109 insertions(+) create mode 100644 .github/workflows/test-verific-cfg.yml diff --git a/.github/workflows/test-verific-cfg.yml b/.github/workflows/test-verific-cfg.yml new file mode 100644 index 000000000..232ca6bd7 --- /dev/null +++ b/.github/workflows/test-verific-cfg.yml @@ -0,0 +1,109 @@ +name: Build various Verific configurations + +on: + workflow_dispatch: + +jobs: + test-verific-cfg: + if: github.repository_owner == 'YosysHQ' + runs-on: [self-hosted, linux, x64, fast] + steps: + - name: Checkout Yosys + uses: actions/checkout@v4 + with: + persist-credentials: false + submodules: true + - name: Runtime environment + run: | + echo "procs=$(nproc)" >> $GITHUB_ENV + + - name: verific [SV] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [VHDL] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [SV + VHDL] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [SV + HIER] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [VHDL + HIER] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [SV + VHDL + HIER] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs + + - name: verific [SV + VHDL + HIER + EDIF + LIBERTY] + run: | + make config-clang + echo "ENABLE_VERIFIC := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_EDIF := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf + echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf + echo "ENABLE_CCACHE := 1" >> Makefile.conf + make -j$procs From 31f7d0d92d6463748672c3b43c55153ee2c14984 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 25 Feb 2026 10:36:46 +0100 Subject: [PATCH 79/87] Remove already disabled CI job --- .github/workflows/update-flake-lock.yml | 25 ------------------------- 1 file changed, 25 deletions(-) delete mode 100644 .github/workflows/update-flake-lock.yml diff --git a/.github/workflows/update-flake-lock.yml b/.github/workflows/update-flake-lock.yml deleted file mode 100644 index b32498baf..000000000 --- a/.github/workflows/update-flake-lock.yml +++ /dev/null @@ -1,25 +0,0 @@ -name: update-flake-lock -on: - workflow_dispatch: # allows manual triggering - schedule: - - cron: '0 0 * * 0' # runs weekly on Sunday at 00:00 - -jobs: - lockfile: - if: github.repository == 'YosysHQ/Yosys' - runs-on: ubuntu-latest - steps: - - name: Checkout repository - uses: actions/checkout@v4 - with: - persist-credentials: false - - name: Install Nix - uses: DeterminateSystems/nix-installer-action@main - - name: Update flake.lock - uses: DeterminateSystems/update-flake-lock@main - with: - token: ${{CI_CREATE_PR_TOKEN}} - pr-title: "Update flake.lock" # Title of PR to be created - pr-labels: | # Labels to be set on the PR - dependencies - automated From 2c52546e2a9b1ac94c1ddfdd88ef80238c412c7e Mon Sep 17 00:00:00 2001 From: nella Date: Wed, 25 Feb 2026 16:42:05 +0100 Subject: [PATCH 80/87] Fix docs. --- docs/source/using_yosys/more_scripting/model_checking.rst | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/docs/source/using_yosys/more_scripting/model_checking.rst b/docs/source/using_yosys/more_scripting/model_checking.rst index 02400d5d8..cbf5dc7b0 100644 --- a/docs/source/using_yosys/more_scripting/model_checking.rst +++ b/docs/source/using_yosys/more_scripting/model_checking.rst @@ -121,12 +121,12 @@ Result with fixed :file:`axis_master.v`: Witness framework and per-property tracking ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -When using AIGER-based formal verification flows (such as the `abc` engine in +When using AIGER-based formal verification flows (such as the ``abc`` engine in SBY), Yosys provides infrastructure for tracking individual formal properties through the verification pipeline. -The `rename -witness` pass (run automatically by `prep`) assigns public -names to all cells that participate in the witness framework: +The `rename -witness` pass assigns public names to all cells that participate in +the witness framework: - Witness signal cells: `$anyconst`, `$anyseq`, `$anyinit`, `$allconst`, `$allseq` @@ -139,7 +139,7 @@ their hierarchical path rather than by anonymous internal identifiers. The `write_aiger -ywmap` option generates a map file for conversion to and from Yosys witness traces, and also allows for mapping AIGER bad-state properties and invariant constraints back to individual formal properties by name. This enables -features like per-property pass/fail reporting (e.g. `abc pdr` with +features like per-property pass/fail reporting (e.g. ``abc pdr`` with ``--keep-going`` mode). The `write_smt2` backend similarly uses the public witness names when emitting From 5970be33fb0dc99e9ca98ca5a6bc65b22c6ee3ce Mon Sep 17 00:00:00 2001 From: Andrew Pullin Date: Tue, 24 Feb 2026 09:55:11 -0800 Subject: [PATCH 81/87] abc9: preserve topological-loop asserts with targeted SCC fallback A real-world ABC9 flow hit residual combinational loops after SCC breaking, tripping the prep_xaiger loop assertion. Keep the existing topological assertions in place (prep_xaiger and reintegrate still assert no_loops). To handle residual non-box loops, add a targeted fallback in prep_xaiger: when loops remain after normal SCC breaking, insert additional $__ABC9_SCC_BREAKER cuts on non-box loop cells, rebuild toposort, and then re-check the existing assertion. Also keep pre-ABC9 SCC tagging on all cell types (scc -all_cell_types) and add a regression test (tests/techmap/abc9-nonbox-loop-with-box.ys). --- passes/techmap/abc9_ops.cc | 113 ++++++++++++++++----- tests/arch/ice40/fsm.ys | 2 +- tests/techmap/abc9-nonbox-loop-with-box.ys | 19 ++++ 3 files changed, 107 insertions(+), 27 deletions(-) create mode 100644 tests/techmap/abc9-nonbox-loop-with-box.ys diff --git a/passes/techmap/abc9_ops.cc b/passes/techmap/abc9_ops.cc index 8d3869ece..7471ec700 100644 --- a/passes/techmap/abc9_ops.cc +++ b/passes/techmap/abc9_ops.cc @@ -23,6 +23,7 @@ #include "kernel/utils.h" #include "kernel/celltypes.h" #include "kernel/timinginfo.h" +#include USING_YOSYS_NAMESPACE PRIVATE_NAMESPACE_BEGIN @@ -587,6 +588,7 @@ void break_scc(RTLIL::Module *module) auto id = it->second; auto r = ids_seen.insert(id); cell->attributes.erase(it); + // Cut exactly one representative cell per SCC id. if (!r.second) continue; for (auto &c : cell->connections_) { @@ -710,8 +712,6 @@ void prep_xaiger(RTLIL::Module *module, bool dff) SigMap sigmap(module); - dict> bit_drivers, bit_users; - TopoSort toposort; dict> box_ports; for (auto cell : module->cells()) { @@ -750,39 +750,100 @@ void prep_xaiger(RTLIL::Module *module, bool dff) } } } - else if (!yosys_celltypes.cell_known(cell->type)) - continue; - - // TODO: Speed up toposort -- we care about box ordering only - for (auto conn : cell->connections()) { - if (cell->input(conn.first)) - for (auto bit : sigmap(conn.second)) - bit_users[bit].insert(cell->name); - - if (cell->output(conn.first) && !abc9_flop) - for (auto bit : sigmap(conn.second)) - bit_drivers[bit].insert(cell->name); - } - toposort.node(cell->name); } if (box_ports.empty()) return; - for (auto &it : bit_users) - if (bit_drivers.count(it.first)) - for (auto driver_cell : bit_drivers.at(it.first)) - for (auto user_cell : it.second) - toposort.edge(driver_cell, user_cell); + // Build the same topo graph for the initial pass and the optional retry. + auto build_toposort = [&](TopoSort &toposort) { + dict> bit_drivers, bit_users; - if (ys_debug(1)) - toposort.analyze_loops = true; + for (auto cell : module->cells()) { + if (cell->type.in(ID($_DFF_N_), ID($_DFF_P_))) + continue; + if (cell->has_keep_attr()) + continue; - bool no_loops = toposort.sort(); + auto inst_module = design->module(cell->type); + bool abc9_flop = inst_module && inst_module->get_bool_attribute(ID::abc9_flop); + if (abc9_flop && !dff) + continue; + if (!(inst_module && inst_module->get_bool_attribute(ID::abc9_box)) && !yosys_celltypes.cell_known(cell->type)) + continue; + + // TODO: Speed up toposort -- we care about box ordering only + for (auto conn : cell->connections()) { + if (cell->input(conn.first)) + for (auto bit : sigmap(conn.second)) + bit_users[bit].insert(cell->name); + + if (cell->output(conn.first) && !abc9_flop) + for (auto bit : sigmap(conn.second)) + bit_drivers[bit].insert(cell->name); + } + toposort.node(cell->name); + } + + // Build producer -> consumer edges on sigmapped nets. + for (auto &it : bit_users) + if (bit_drivers.count(it.first)) + for (auto driver_cell : bit_drivers.at(it.first)) + for (auto user_cell : it.second) + toposort.edge(driver_cell, user_cell); + if (ys_debug(1)) + toposort.analyze_loops = true; + return toposort.sort(); + }; + + // Build TopoSort in a container, as we may need to conditionally rebuild it on retry. + std::optional> toposort; + toposort.emplace(); + bool no_loops = build_toposort(toposort.value()); + + // Fallback for residual loops after SCC cutting: insert additional + // breakers on non-box loop cells, then re-run toposort checks. + if (!no_loops) { + SigSpec I, O; + pool broken_cells; + + for (auto &loop : toposort.value().loops) + for (auto cell_name : loop) { + // Loop reports can overlap; cut each cell at most once. + if (!broken_cells.insert(cell_name).second) + continue; + auto cell = module->cell(cell_name); + log_assert(cell); + auto inst_module = design->module(cell->type); + if (inst_module && inst_module->get_bool_attribute(ID::abc9_box)) + continue; + for (auto &c : cell->connections_) { + if (c.second.is_fully_const()) continue; + if (cell->output(c.first)) { + Wire *w = module->addWire(NEW_ID, GetSize(c.second)); + I.append(w); + O.append(c.second); + c.second = w; + } + } + } + + if (!I.empty()) { + auto cell = module->addCell(NEW_ID, ID($__ABC9_SCC_BREAKER)); + log_assert(GetSize(I) == GetSize(O)); + cell->setParam(ID::WIDTH, GetSize(I)); + cell->setPort(ID::I, std::move(I)); + cell->setPort(ID::O, std::move(O)); + + // Rebuild topo ordering after inserting the additional breakers. + toposort.emplace(); + no_loops = build_toposort(toposort.value()); + } + } if (ys_debug(1)) { unsigned i = 0; - for (auto &it : toposort.loops) { + for (auto &it : toposort.value().loops) { log(" loop %d\n", i++); for (auto cell_name : it) { auto cell = module->cell(cell_name); @@ -806,7 +867,7 @@ void prep_xaiger(RTLIL::Module *module, bool dff) TimingInfo timing; int port_id = 1, box_count = 0; - for (auto cell_name : toposort.sorted) { + for (auto cell_name : toposort.value().sorted) { RTLIL::Cell *cell = module->cell(cell_name); log_assert(cell); diff --git a/tests/arch/ice40/fsm.ys b/tests/arch/ice40/fsm.ys index e3b746202..b01d34bba 100644 --- a/tests/arch/ice40/fsm.ys +++ b/tests/arch/ice40/fsm.ys @@ -12,5 +12,5 @@ cd fsm # Constrain all select calls below inside the top module select -assert-count 4 t:SB_DFF select -assert-count 2 t:SB_DFFESR -select -assert-max 15 t:SB_LUT4 +select -assert-max 16 t:SB_LUT4 select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D diff --git a/tests/techmap/abc9-nonbox-loop-with-box.ys b/tests/techmap/abc9-nonbox-loop-with-box.ys new file mode 100644 index 000000000..2b7a551bc --- /dev/null +++ b/tests/techmap/abc9-nonbox-loop-with-box.ys @@ -0,0 +1,19 @@ +read_verilog -icells -specify < o) = 1; +endspecify +endmodule + +module top(input i, output o); + wire a, b, c, z; + $_AND_ a0(.A(b), .B(i), .Y(a)); + $_AND_ b0(.A(a), .B(c), .Y(b)); + $_AND_ c0(.A(b), .B(i), .Y(c)); + box1 u_box(.i(i), .o(z)); + assign o = c ^ z; +endmodule +EOT + +abc9 -lut 4 From b3caec1a93baf847559422bb30df8b1168296292 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 27 Feb 2026 07:55:34 +0100 Subject: [PATCH 82/87] Update ABC as per 2026-02-27 --- abc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/abc b/abc index c18b835ef..8e401543d 160000 --- a/abc +++ b/abc @@ -1 +1 @@ -Subproject commit c18b835ef140217c84a26ba510f98f69d54dd48e +Subproject commit 8e401543d3ecf65e3a3631c7a271793a4d356cb0 From 7f1f247c5629863902e36bb2d7b51f9aec2feb59 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Fri, 27 Feb 2026 13:12:32 +0100 Subject: [PATCH 83/87] gowin: remove spurious warning --- techlibs/gowin/synth_gowin.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/techlibs/gowin/synth_gowin.cc b/techlibs/gowin/synth_gowin.cc index 3d1414e9e..9fd4dca86 100644 --- a/techlibs/gowin/synth_gowin.cc +++ b/techlibs/gowin/synth_gowin.cc @@ -309,7 +309,7 @@ struct SynthGowinPass : public ScriptPass if (nolutram) args += " -no-auto-distributed"; } - run(stringf("memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt -D %s", family) + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)"); + run(stringf("memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt%s", family == "gw5a" ? " -D gw5a" : "") + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)"); run(stringf("techmap -map +/gowin/lutrams_map.v -map +/gowin/brams_map%s.v", family == "gw5a" ? "_gw5a" : "")); } From e9442194f27140e3e80cb3bf407c3259d562c449 Mon Sep 17 00:00:00 2001 From: likeamahoney Date: Fri, 27 Feb 2026 20:42:40 +0300 Subject: [PATCH 84/87] support automatic lifetime qualifier on procedural variables --- frontends/ast/genrtlil.cc | 12 ++++ frontends/verilog/verilog_parser.y | 18 +++-- tests/verilog/automatic_lifetime.ys | 104 ++++++++++++++++++++++++++++ 3 files changed, 129 insertions(+), 5 deletions(-) create mode 100644 tests/verilog/automatic_lifetime.ys diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index d9eb51a9c..65af26132 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -403,6 +403,18 @@ struct AST_INTERNAL::ProcessGenerator if (GetSize(syncrule->signal) != 1) always->input_error("Found posedge/negedge event on a signal that is not 1 bit wide!\n"); addChunkActions(syncrule->actions, subst_lvalue_from, subst_lvalue_to, true); + // Automatic (nosync) variables must not become flip-flops: remove + // them from clocked sync rules so that proc_dff does not infer + // an unnecessary register for a purely combinational temporary. + syncrule->actions.erase( + std::remove_if(syncrule->actions.begin(), syncrule->actions.end(), + [](const RTLIL::SigSig &ss) { + for (auto &chunk : ss.first.chunks()) + if (chunk.wire && chunk.wire->get_bool_attribute(ID::nosync)) + return true; + return false; + }), + syncrule->actions.end()); proc->syncs.push_back(syncrule); } if (proc->syncs.empty()) { diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 684727d5b..148a6cc63 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -84,7 +84,7 @@ int current_function_or_task_port_id; std::vector case_type_stack; bool do_not_require_port_stubs; - bool current_wire_rand, current_wire_const; + bool current_wire_rand, current_wire_const, current_wire_automatic; bool current_modport_input, current_modport_output; bool default_nettype_wire = true; std::istream* lexin; @@ -958,14 +958,18 @@ delay: non_opt_delay | %empty; io_wire_type: - { extra->astbuf3 = std::make_unique(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; } + { extra->astbuf3 = std::make_unique(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; extra->current_wire_automatic = false; } wire_type_token_io wire_type_const_rand opt_wire_type_token wire_type_signedness { $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); }; non_io_wire_type: - { extra->astbuf3 = std::make_unique(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; } - wire_type_const_rand wire_type_token wire_type_signedness - { $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); }; + { extra->astbuf3 = std::make_unique(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; extra->current_wire_automatic = false; } + opt_lifetime wire_type_const_rand wire_type_token wire_type_signedness + { + if (extra->current_wire_automatic) + extra->astbuf3->set_attribute(ID::nosync, AstNode::mkconst_int(extra->astbuf3->location, 1, false)); + $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); + }; wire_type: io_wire_type { $$ = std::move($1); } | @@ -1253,6 +1257,10 @@ opt_automatic: TOK_AUTOMATIC | %empty; +opt_lifetime: + TOK_AUTOMATIC { extra->current_wire_automatic = true; } | + %empty; + task_func_args_opt: TOK_LPAREN TOK_RPAREN | %empty | TOK_LPAREN { extra->albuf = nullptr; diff --git a/tests/verilog/automatic_lifetime.ys b/tests/verilog/automatic_lifetime.ys new file mode 100644 index 000000000..84e21e088 --- /dev/null +++ b/tests/verilog/automatic_lifetime.ys @@ -0,0 +1,104 @@ +# Automatic reg as intermediate value in always @(*) +# The result must be provably equivalent to the direct expression. +# No latch or DFF must be created for tmp. +design -reset +read_verilog -sv <> 4) & 1'b1)); +endmodule +EOF +proc +async2sync +select -assert-none t:$dff t:$dlatch %% +sat -verify -prove-asserts -show-all + +# automatic in a clocked block — only the explicitly registered +# output (result) must get a DFF; the automatic temp must not. +design -reset +read_verilog -sv < Date: Wed, 4 Mar 2026 07:46:40 +0100 Subject: [PATCH 85/87] Fix help message for equiv passes --- passes/equiv/equiv_induct.cc | 2 +- passes/equiv/equiv_simple.cc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index d843fef67..e4480c893 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -174,7 +174,7 @@ struct EquivInductPass : public Pass { log("Only selected $equiv cells are proven and only selected cells are used to\n"); log("perform the proof.\n"); log("\n"); - EquivBasicConfig::help("4"); + log("%s", EquivBasicConfig::help("4")); log("\n"); log("This command is very effective in proving complex sequential circuits, when\n"); log("the internal state of the circuit quickly propagates to $equiv cells.\n"); diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index ff6df295c..e498928c3 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -428,7 +428,7 @@ struct EquivSimplePass : public Pass { log("\n"); log("This command tries to prove $equiv cells using a simple direct SAT approach.\n"); log("\n"); - EquivSimpleConfig::help("1"); + log("%s", EquivSimpleConfig::help("1")); log("\n"); } void execute(std::vector args, Design *design) override From 70a11c6bf0e8dd669f56c7da3587f78b405138e2 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 4 Mar 2026 07:46:57 +0100 Subject: [PATCH 86/87] Release version 0.63 --- CHANGELOG | 14 +++++++++++++- Makefile | 4 ++-- docs/source/conf.py | 2 +- 3 files changed, 16 insertions(+), 4 deletions(-) diff --git a/CHANGELOG b/CHANGELOG index e345a8514..4904d9639 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,8 +2,20 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.62 .. Yosys 0.63-dev +Yosys 0.62 .. Yosys 0.63 -------------------------- + * Various + - Added DSP inference for Gowin GW1N and GW2A. + - Added support for subtract in preadder for Xilinx arch. + - Added infrastructure to run a sat solver as a command. + + * New commands and options + - Added "-ignore-unknown-cells" option to "equiv_induct" + and "equiv_simple" pass. + - Added "-force-params" option to "memory_libmap" pass. + - Added "-select-solver" option to "sat" pass. + - Added "-default_params" option to "write_verilog" pass. + - Added "-nodsp" option to "synth_gowin" pass. Yosys 0.61 .. Yosys 0.62 -------------------------- diff --git a/Makefile b/Makefile index 0a15c2b23..5a2cb66f5 100644 --- a/Makefile +++ b/Makefile @@ -161,7 +161,7 @@ ifeq ($(OS), Haiku) CXXFLAGS += -D_DEFAULT_SOURCE endif -YOSYS_VER := 0.62 +YOSYS_VER := 0.63 ifneq (, $(shell command -v git 2>/dev/null)) ifneq (, $(shell git rev-parse --git-dir 2>/dev/null)) @@ -170,7 +170,7 @@ ifneq (, $(shell git rev-parse --git-dir 2>/dev/null)) YOSYS_VER := $(YOSYS_VER)+$(GIT_COMMIT_COUNT) endif else - YOSYS_VER := $(YOSYS_VER)+post +# YOSYS_VER := $(YOSYS_VER)+post endif endif diff --git a/docs/source/conf.py b/docs/source/conf.py index a7da22d97..458040db0 100644 --- a/docs/source/conf.py +++ b/docs/source/conf.py @@ -6,7 +6,7 @@ import os project = 'YosysHQ Yosys' author = 'YosysHQ GmbH' copyright ='2026 YosysHQ GmbH' -yosys_ver = "0.62" +yosys_ver = "0.63" # select HTML theme html_theme = 'furo-ys' From 228052bfb3e4a733e4bdb3fe57cdc7692a47e220 Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Wed, 4 Mar 2026 08:45:13 +0100 Subject: [PATCH 87/87] Next dev cycle --- CHANGELOG | 3 +++ Makefile | 2 +- 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/CHANGELOG b/CHANGELOG index 4904d9639..372a59d58 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -2,6 +2,9 @@ List of major changes and improvements between releases ======================================================= +Yosys 0.63 .. Yosys 0.64-dev +-------------------------- + Yosys 0.62 .. Yosys 0.63 -------------------------- * Various diff --git a/Makefile b/Makefile index 5a2cb66f5..507c74a63 100644 --- a/Makefile +++ b/Makefile @@ -170,7 +170,7 @@ ifneq (, $(shell git rev-parse --git-dir 2>/dev/null)) YOSYS_VER := $(YOSYS_VER)+$(GIT_COMMIT_COUNT) endif else -# YOSYS_VER := $(YOSYS_VER)+post + YOSYS_VER := $(YOSYS_VER)+post endif endif