aboutsummaryrefslogtreecommitdiffstats
path: root/passes/equiv
diff options
context:
space:
mode:
Diffstat (limited to 'passes/equiv')
-rw-r--r--passes/equiv/equiv_add.cc2
-rw-r--r--passes/equiv/equiv_induct.cc11
-rw-r--r--passes/equiv/equiv_make.cc10
-rw-r--r--passes/equiv/equiv_mark.cc2
-rw-r--r--passes/equiv/equiv_miter.cc2
-rw-r--r--passes/equiv/equiv_purge.cc6
-rw-r--r--passes/equiv/equiv_remove.cc2
-rw-r--r--passes/equiv/equiv_simple.cc10
-rw-r--r--passes/equiv/equiv_status.cc2
-rw-r--r--passes/equiv/equiv_struct.cc2
10 files changed, 29 insertions, 20 deletions
diff --git a/passes/equiv/equiv_add.cc b/passes/equiv/equiv_add.cc
index 2abbb59bb..1bcd4a887 100644
--- a/passes/equiv/equiv_add.cc
+++ b/passes/equiv/equiv_add.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index 596c938fc..8d882ae83 100644
--- a/passes/equiv/equiv_induct.cc
+++ b/passes/equiv/equiv_induct.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
@@ -55,7 +55,10 @@ struct EquivInductWorker
for (auto cell : cells) {
if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) {
- log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
+ if (RTLIL::builtin_ff_cell_types().count(cell->type))
+ 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 (cell->type == ID($equiv)) {
@@ -65,8 +68,10 @@ struct EquivInductWorker
int ez_a = satgen.importSigBit(bit_a, step);
int ez_b = satgen.importSigBit(bit_b, step);
int cond = ez->IFF(ez_a, ez_b);
- if (satgen.model_undef)
+ if (satgen.model_undef) {
+ cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_b, step)));
cond = ez->OR(cond, satgen.importUndefSigBit(bit_a, step));
+ }
ez_equal_terms.push_back(cond);
}
}
diff --git a/passes/equiv/equiv_make.cc b/passes/equiv/equiv_make.cc
index 51b4ad0f1..7ef2827bf 100644
--- a/passes/equiv/equiv_make.cc
+++ b/passes/equiv/equiv_make.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
@@ -114,25 +114,25 @@ struct EquivMakeWorker
Module *gate_clone = gate_mod->clone();
for (auto it : gold_clone->wires().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
wire_names.insert(it->name);
gold_clone->rename(it, it->name.str() + "_gold");
}
for (auto it : gold_clone->cells().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
cell_names.insert(it->name);
gold_clone->rename(it, it->name.str() + "_gold");
}
for (auto it : gate_clone->wires().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
wire_names.insert(it->name);
gate_clone->rename(it, it->name.str() + "_gate");
}
for (auto it : gate_clone->cells().to_vector()) {
- if ((it->name[0] == '\\' || inames) && blacklist_names.count(it->name) == 0)
+ if ((it->name.isPublic() || inames) && blacklist_names.count(it->name) == 0)
cell_names.insert(it->name);
gate_clone->rename(it, it->name.str() + "_gate");
}
diff --git a/passes/equiv/equiv_mark.cc b/passes/equiv/equiv_mark.cc
index a722b5ed6..97a2a38dd 100644
--- a/passes/equiv/equiv_mark.cc
+++ b/passes/equiv/equiv_mark.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
diff --git a/passes/equiv/equiv_miter.cc b/passes/equiv/equiv_miter.cc
index e028f806a..6acfe85a9 100644
--- a/passes/equiv/equiv_miter.cc
+++ b/passes/equiv/equiv_miter.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
diff --git a/passes/equiv/equiv_purge.cc b/passes/equiv/equiv_purge.cc
index d15c8d183..5b0696d9b 100644
--- a/passes/equiv/equiv_purge.cc
+++ b/passes/equiv/equiv_purge.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
@@ -35,7 +35,7 @@ struct EquivPurgeWorker
{
if (sig.is_wire()) {
Wire *wire = sig.as_wire();
- if (wire->name[0] == '\\') {
+ if (wire->name.isPublic()) {
if (!wire->port_output) {
log(" Module output: %s (%s)\n", log_signal(wire), log_id(cellname));
wire->port_output = true;
@@ -62,7 +62,7 @@ struct EquivPurgeWorker
{
if (sig.is_wire()) {
Wire *wire = sig.as_wire();
- if (wire->name[0] == '\\') {
+ if (wire->name.isPublic()) {
if (!wire->port_output) {
log(" Module input: %s\n", log_signal(wire));
wire->port_input = true;
diff --git a/passes/equiv/equiv_remove.cc b/passes/equiv/equiv_remove.cc
index 89442308b..5d1823e12 100644
--- a/passes/equiv/equiv_remove.cc
+++ b/passes/equiv/equiv_remove.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index 408c5a793..7621341a7 100644
--- a/passes/equiv/equiv_simple.cc
+++ b/passes/equiv/equiv_simple.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
@@ -184,8 +184,12 @@ struct EquivSimpleWorker
for (auto cell : problem_cells) {
auto key = pair<Cell*, int>(cell, step+1);
- if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1))
- log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
+ if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) {
+ if (RTLIL::builtin_ff_cell_types().count(cell->type))
+ 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));
+ }
imported_cells_cache.insert(key);
}
diff --git a/passes/equiv/equiv_status.cc b/passes/equiv/equiv_status.cc
index 2db44ea90..b221be27c 100644
--- a/passes/equiv/equiv_status.cc
+++ b/passes/equiv/equiv_status.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
diff --git a/passes/equiv/equiv_struct.cc b/passes/equiv/equiv_struct.cc
index 9784225db..39604994a 100644
--- a/passes/equiv/equiv_struct.cc
+++ b/passes/equiv/equiv_struct.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 02:33:24 +0000