aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/btor/btor.cc34
-rw-r--r--backends/smt2/smt2.cc2
-rw-r--r--kernel/yw.h4
-rw-r--r--passes/sat/formalff.cc216
-rw-r--r--passes/sat/sim.cc51
5 files changed, 274 insertions, 33 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 4eb675c3c..4c43e91e7 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -95,7 +95,9 @@ struct BtorWorker
vector<ywmap_btor_sig> ywmap_inputs;
vector<ywmap_btor_sig> ywmap_states;
- dict<SigBit, int> ywmap_clocks;
+ dict<SigBit, int> ywmap_clock_bits;
+ dict<SigBit, int> ywmap_clock_inputs;
+
PrettyJson ywmap_json;
@@ -693,7 +695,7 @@ struct BtorWorker
info_clocks[nid] |= negedge ? 2 : 1;
if (ywmap_json.active())
- ywmap_clocks[sig_c] |= negedge ? 2 : 1;
+ ywmap_clock_bits[sig_c] |= negedge ? 2 : 1;
}
IdString symbol;
@@ -1175,6 +1177,20 @@ struct BtorWorker
btorf_push("inputs");
+ if (ywmap_json.active()) {
+ for (auto wire : module->wires())
+ {
+ auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+ if (gclk_attr == wire->attributes.end())
+ continue;
+ SigSpec sig = sigmap(wire);
+ if (gclk_attr->second == State::S1)
+ ywmap_clock_bits[sig] |= 1;
+ else if (gclk_attr->second == State::S0)
+ ywmap_clock_bits[sig] |= 2;
+ }
+ }
+
for (auto wire : module->wires())
{
if (wire->attributes.count(ID::init)) {
@@ -1206,12 +1222,12 @@ struct BtorWorker
}
if (ywmap_json.active()) {
- auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
- if (gclk_attr != wire->attributes.end()) {
- if (gclk_attr->second == State::S1)
- ywmap_clocks[sig] |= 1;
- else if (gclk_attr->second == State::S0)
- ywmap_clocks[sig] |= 2;
+ for (int i = 0; i < GetSize(sig); i++) {
+ auto input_bit = SigBit(wire, i);
+ auto bit = sigmap(input_bit);
+ if (!ywmap_clock_bits.count(bit))
+ continue;
+ ywmap_clock_inputs[input_bit] = ywmap_clock_bits[bit];
}
}
}
@@ -1479,7 +1495,7 @@ struct BtorWorker
ywmap_json.name("clocks");
ywmap_json.begin_array();
- for (auto &entry : ywmap_clocks) {
+ for (auto &entry : ywmap_clock_inputs) {
if (entry.second != 1 && entry.second != 2)
continue;
log_assert(entry.first.is_wire());
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 3b3585b59..1ab39a405 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -998,7 +998,7 @@ struct Smt2Worker
if (contains_clock && GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
- if (contains_clock) {
+ if (wire->port_input && contains_clock) {
for (int i = 0; i < GetSize(sig); i++) {
bool is_posedge = clock_posedge.count(sig[i]);
bool is_negedge = clock_negedge.count(sig[i]);
diff --git a/kernel/yw.h b/kernel/yw.h
index 503319b1d..c2f5921b1 100644
--- a/kernel/yw.h
+++ b/kernel/yw.h
@@ -69,8 +69,8 @@ struct ReadWitness
struct Clock {
IdPath path;
int offset;
- bool is_posedge;
- bool is_negedge;
+ bool is_posedge = false;
+ bool is_negedge = false;
};
struct Signal {
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index e36379096..099df4be9 100644
--- a/passes/sat/formalff.cc
+++ b/passes/sat/formalff.cc
@@ -317,6 +317,172 @@ struct InitValWorker
}
};
+struct ReplacedPort {
+ IdString name;
+ int offset;
+ bool clk_pol;
+};
+
+struct HierarchyWorker
+{
+ Design *design;
+ pool<Module *> pending;
+
+ dict<Module *, std::vector<ReplacedPort>> replaced_clk_inputs;
+
+ HierarchyWorker(Design *design) :
+ design(design)
+ {
+ for (auto module : design->modules())
+ pending.insert(module);
+ }
+
+ void propagate();
+
+ const std::vector<ReplacedPort> &find_replaced_clk_inputs(IdString cell_type);
+};
+
+// Propagates replaced clock signals
+struct PropagateWorker
+{
+ HierarchyWorker &hierarchy;
+
+ Module *module;
+ SigMap sigmap;
+
+ dict<SigBit, bool> replaced_clk_bits;
+ dict<SigBit, SigBit> not_drivers;
+
+ std::vector<ReplacedPort> replaced_clk_inputs;
+ std::vector<std::pair<SigBit, bool>> pending;
+
+ PropagateWorker(Module *module, HierarchyWorker &hierarchy) :
+ hierarchy(hierarchy), module(module), sigmap(module)
+ {
+ hierarchy.pending.erase(module);
+
+ for (auto wire : module->wires())
+ if (wire->has_attribute(ID::replaced_by_gclk))
+ replace_clk_bit(SigBit(wire), wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1, false);
+
+ for (auto cell : module->cells()) {
+ if (cell->type.in(ID($not), ID($_NOT_))) {
+ auto sig_a = cell->getPort(ID::A);
+ auto &sig_y = cell->getPort(ID::Y);
+ sig_a.extend_u0(GetSize(sig_y), cell->parameters.at(ID::A_SIGNED).as_bool());
+
+ for (int i = 0; i < GetSize(sig_a); i++)
+ if (sig_a[i].is_wire())
+ not_drivers.emplace(sigmap(sig_y[i]), sigmap(sig_a[i]));
+ } else {
+ for (auto &port_bit : hierarchy.find_replaced_clk_inputs(cell->type))
+ replace_clk_bit(cell->getPort(port_bit.name)[port_bit.offset], port_bit.clk_pol, true);
+ }
+ }
+
+ while (!pending.empty()) {
+ auto current = pending.back();
+ pending.pop_back();
+ auto it = not_drivers.find(current.first);
+ if (it == not_drivers.end())
+ continue;
+
+ replace_clk_bit(it->second, !current.second, true);
+ }
+
+ for (auto cell : module->cells()) {
+ if (cell->type.in(ID($not), ID($_NOT_)))
+ continue;
+ for (auto &conn : cell->connections()) {
+ if (!cell->output(conn.first))
+ continue;
+ for (SigBit bit : conn.second) {
+ sigmap.apply(bit);
+ if (replaced_clk_bits.count(bit))
+ log_error("derived signal %s driven by %s (%s) from module %s is used as clock, derived clocks are only supported with clk2fflogic.\n",
+ log_signal(bit), log_id(cell->name), log_id(cell->type), log_id(module));
+ }
+ }
+ }
+
+ for (auto port : module->ports) {
+ auto wire = module->wire(port);
+ if (!wire->port_input)
+ continue;
+ for (int i = 0; i < GetSize(wire); i++) {
+ SigBit bit(wire, i);
+ sigmap.apply(bit);
+ auto it = replaced_clk_bits.find(bit);
+ if (it == replaced_clk_bits.end())
+ continue;
+ replaced_clk_inputs.emplace_back(ReplacedPort {port, i, it->second});
+
+ if (it->second) {
+ bit = module->Not(NEW_ID, bit);
+ }
+ }
+ }
+ }
+
+ void replace_clk_bit(SigBit bit, bool polarity, bool add_attribute)
+ {
+ sigmap.apply(bit);
+ if (!bit.is_wire())
+ log_error("XXX todo\n");
+
+ auto it = replaced_clk_bits.find(bit);
+ if (it != replaced_clk_bits.end()) {
+ if (it->second != polarity)
+ log_error("signal %s from module %s is used as clock with different polarities, run clk2fflogic instead.\n",
+ log_signal(bit), log_id(module));
+ return;
+ }
+
+ replaced_clk_bits.emplace(bit, polarity);
+
+ if (add_attribute) {
+ Wire *clk_wire = bit.wire;
+ if (bit.offset != 0 || GetSize(bit.wire) != 1) {
+ clk_wire = module->addWire(NEW_ID);
+ module->connect(RTLIL::SigBit(clk_wire), bit);
+ }
+ clk_wire->attributes[ID::replaced_by_gclk] = polarity ? State::S1 : State::S0;
+ clk_wire->set_bool_attribute(ID::keep);
+ }
+
+ pending.emplace_back(bit, polarity);
+ }
+};
+
+const std::vector<ReplacedPort> &HierarchyWorker::find_replaced_clk_inputs(IdString cell_type)
+{
+ static const std::vector<ReplacedPort> empty;
+ if (!cell_type.isPublic())
+ return empty;
+
+ Module *module = design->module(cell_type);
+ if (module == nullptr)
+ return empty;
+
+ auto it = replaced_clk_inputs.find(module);
+ if (it != replaced_clk_inputs.end())
+ return it->second;
+
+ if (pending.count(module)) {
+ PropagateWorker worker(module, *this);
+ return replaced_clk_inputs.emplace(module, std::move(worker.replaced_clk_inputs)).first->second;
+ }
+
+ return empty;
+}
+
+
+void HierarchyWorker::propagate()
+{
+ while (!pending.empty())
+ PropagateWorker worker(pending.pop(), *this);
+}
+
struct FormalFfPass : public Pass {
FormalFfPass() : Pass("formalff", "prepare FFs for formal") { }
void help() override
@@ -362,6 +528,15 @@ struct FormalFfPass : public Pass {
log(" them. For -ff2anyinit, this reduces the number of generated $anyinit\n");
log(" cells that drive wires with private names.\n");
log("\n");
+ log(" -hierarchy\n");
+ log(" Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards\n");
+ log(" through the design hierarchy towards the toplevel inputs. This option\n");
+ log(" works on the whole design and ignores the selection.\n");
+ log("\n");
+ log(" -assume\n");
+ log(" Add assumptions that constrain wires with the 'replaced_by_gclk'\n");
+ log(" attribute to the value they would have before an active clock edge.\n");
+ log("\n");
// TODO: An option to check whether all FFs use the same clock before changing it to the global clock
}
@@ -372,6 +547,8 @@ struct FormalFfPass : public Pass {
bool flag_anyinit2ff = false;
bool flag_fine = false;
bool flag_setundef = false;
+ bool flag_hierarchy = false;
+ bool flag_assume = false;
log_header(design, "Executing FORMALFF pass.\n");
@@ -398,12 +575,20 @@ struct FormalFfPass : public Pass {
flag_setundef = true;
continue;
}
+ if (args[argidx] == "-hierarchy") {
+ flag_hierarchy = true;
+ continue;
+ }
+ if (args[argidx] == "-assume") {
+ flag_assume = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
- if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff))
- log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n");
+ if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume))
+ log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume must be specified.\n");
if (flag_ff2anyinit && flag_anyinit2ff)
log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
@@ -548,6 +733,33 @@ struct FormalFfPass : public Pass {
ff.emit();
}
}
+
+ if (flag_hierarchy) {
+ HierarchyWorker worker(design);
+ worker.propagate();
+ }
+
+ if (flag_assume) {
+ for (auto module : design->selected_modules()) {
+ std::vector<pair<SigBit, bool>> found;
+ for (auto wire : module->wires()) {
+ if (!wire->has_attribute(ID::replaced_by_gclk))
+ continue;
+ bool clk_pol = wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1;
+
+ found.emplace_back(SigSpec(wire), clk_pol);
+ }
+ for (auto pair : found) {
+ SigBit clk = pair.first;
+
+ if (pair.second)
+ clk = module->Not(NEW_ID, clk);
+
+ module->addAssume(NEW_ID, clk, State::S1);
+
+ }
+ }
+ }
}
} FormalFfPass;
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 1dd406f22..cfe31968d 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -1655,28 +1655,25 @@ struct SimWorker : SimShared
};
struct YwHierarchy {
- dict<IdPath, FoundYWPath> signal_paths;
- dict<IdPath, FoundYWPath> clock_paths;
+ dict<IdPath, FoundYWPath> paths;
};
YwHierarchy prepare_yw_hierarchy(const ReadWitness &yw)
{
+ YwHierarchy hierarchy;
pool<IdPath> paths;
dict<IdPath, pool<IdString>> mem_paths;
for (auto &signal : yw.signals)
paths.insert(signal.path);
- for (auto &clock : yw.clocks) {
- if (paths.count(clock.path))
- log_warning("Witness path `%s` is present as witness signal and as clock, treating as clock and ignoring signal data.\n", clock.path.str().c_str());
+ for (auto &clock : yw.clocks)
paths.insert(clock.path);
- }
+
for (auto &path : paths)
if (path.has_address())
mem_paths[path.prefix()].insert(path.back());
- YwHierarchy hierarchy;
witness_hierarchy(top->module, top, [&](IdPath const &path, WitnessHierarchyItem item, SimInstance *instance) {
if (item.cell != nullptr)
return instance->children.at(item.cell);
@@ -1684,7 +1681,7 @@ struct SimWorker : SimShared
if (paths.count(path)) {
if (debug)
log("witness hierarchy: found wire %s\n", path.str().c_str());
- bool inserted = hierarchy.signal_paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second;
+ bool inserted = hierarchy.paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second;
if (!inserted)
log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
}
@@ -1701,7 +1698,7 @@ struct SimWorker : SimShared
word_path.get_address(addr);
if (addr < item.mem->start_offset || (addr - item.mem->start_offset) >= item.mem->size)
continue;
- bool inserted = hierarchy.signal_paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second;
+ bool inserted = hierarchy.paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second;
if (!inserted)
log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
}
@@ -1711,19 +1708,35 @@ struct SimWorker : SimShared
});
for (auto &path : paths)
- if (!hierarchy.signal_paths.count(path))
+ if (!hierarchy.paths.count(path))
log_warning("Yosys witness path `%s` was not found in this design, ignoring\n", path.str().c_str());
+ dict<IdPath, dict<int, bool>> clock_inputs;
+
for (auto &clock : yw.clocks) {
- auto found_path_it = hierarchy.signal_paths.find(clock.path);
- if (found_path_it == hierarchy.signal_paths.end())
+ if (clock.is_negedge == clock.is_posedge)
continue;
- hierarchy.clock_paths.insert(*found_path_it);
- hierarchy.signal_paths.erase(found_path_it);
- paths.insert(clock.path);
+ clock_inputs[clock.path].emplace(clock.offset, clock.is_posedge);
}
+ for (auto &signal : yw.signals) {
+ auto it = clock_inputs.find(signal.path);
+ if (it == clock_inputs.end())
+ continue;
+ for (auto &clock_input : it->second) {
+ int offset = clock_input.first;
+ if (offset >= signal.offset && (offset - signal.offset) < signal.width) {
+ int clock_bits_offset = signal.bits_offset + (offset - signal.offset);
+ State expected = clock_input.second ? State::S0 : State::S1;
+
+ for (int t = 0; t < GetSize(yw.steps); t++) {
+ if (yw.get_bits(t, clock_bits_offset, 1) != expected)
+ log_warning("Yosys witness trace has an unexpected value for the clock input `%s` in step %d.\n", signal.path.str().c_str(), t);
+ }
+ }
+ }
+ }
// TODO add checks and warnings for witness signals (toplevel inputs, $any*) not present in the witness file
return hierarchy;
@@ -1736,8 +1749,8 @@ struct SimWorker : SimShared
for (auto &signal : yw.signals) {
if (signal.init_only && t >= 1)
continue;
- auto found_path_it = hierarchy.signal_paths.find(signal.path);
- if (found_path_it == hierarchy.signal_paths.end())
+ auto found_path_it = hierarchy.paths.find(signal.path);
+ if (found_path_it == hierarchy.paths.end())
continue;
auto &found_path = found_path_it->second;
@@ -1767,8 +1780,8 @@ struct SimWorker : SimShared
for (auto &clock : yw.clocks) {
if (clock.is_negedge == clock.is_posedge)
continue;
- auto found_path_it = hierarchy.clock_paths.find(clock.path);
- if (found_path_it == hierarchy.clock_paths.end())
+ auto found_path_it = hierarchy.paths.find(clock.path);
+ if (found_path_it == hierarchy.paths.end())
continue;
auto &found_path = found_path_it->second;
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-29 13:46:27 +0000