aboutsummaryrefslogtreecommitdiffstats
path: root/passes/sat
diff options
context:
space:
mode:
Diffstat (limited to 'passes/sat')
-rw-r--r--passes/sat/assertpmux.cc6
-rw-r--r--passes/sat/clk2fflogic.cc7
-rw-r--r--passes/sat/cutpoint.cc2
-rw-r--r--passes/sat/eval.cc4
-rw-r--r--passes/sat/expose.cc4
-rw-r--r--passes/sat/miter.cc6
-rw-r--r--passes/sat/sat.cc10
7 files changed, 25 insertions, 14 deletions
diff --git a/passes/sat/assertpmux.cc b/passes/sat/assertpmux.cc
index 509cb0ba9..3b432c461 100644
--- a/passes/sat/assertpmux.cc
+++ b/passes/sat/assertpmux.cc
@@ -180,7 +180,7 @@ struct AssertpmuxWorker
};
struct AssertpmuxPass : public Pass {
- AssertpmuxPass() : Pass("assertpmux", "convert internal signals to module ports") { }
+ AssertpmuxPass() : Pass("assertpmux", "adds asserts for parallel muxes") { }
void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
@@ -195,8 +195,8 @@ struct AssertpmuxPass : public Pass {
log("\n");
log(" -always\n");
log(" usually the $pmux condition is only checked when the $pmux output\n");
- log(" is used be the mux tree it drives. this option will deactivate this\n");
- log(" additional constrained and check the $pmux condition always.\n");
+ log(" is used by the mux tree it drives. this option will deactivate this\n");
+ log(" additional constraint and check the $pmux condition always.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc
index 49ec795d3..4bb4aa047 100644
--- a/passes/sat/clk2fflogic.cc
+++ b/passes/sat/clk2fflogic.cc
@@ -253,6 +253,13 @@ struct Clk2fflogicPass : public Pass {
SigSpec qval = module->Mux(NEW_ID, past_q, past_d, clock_edge);
Const rstval = cell->parameters["\\ARST_VALUE"];
+ Wire *past_arst = module->addWire(NEW_ID);
+ module->addFf(NEW_ID, arst, past_arst);
+ if (cell->parameters["\\ARST_POLARITY"].as_bool())
+ arst = module->LogicOr(NEW_ID, arst, past_arst);
+ else
+ arst = module->LogicAnd(NEW_ID, arst, past_arst);
+
if (cell->parameters["\\ARST_POLARITY"].as_bool())
module->addMux(NEW_ID, qval, rstval, arst, sig_q);
else
diff --git a/passes/sat/cutpoint.cc b/passes/sat/cutpoint.cc
index 048aec7f3..b4549bc39 100644
--- a/passes/sat/cutpoint.cc
+++ b/passes/sat/cutpoint.cc
@@ -24,7 +24,7 @@ USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct CutpointPass : public Pass {
- CutpointPass() : Pass("cutpoint", "add hi/lo cover cells for each wire bit") { }
+ CutpointPass() : Pass("cutpoint", "adds formal cut points to the design") { }
void help() YS_OVERRIDE
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
diff --git a/passes/sat/eval.cc b/passes/sat/eval.cc
index 008cd2dfa..e0bb439f4 100644
--- a/passes/sat/eval.cc
+++ b/passes/sat/eval.cc
@@ -47,8 +47,8 @@ struct BruteForceEquivChecker
{
if (inputs.size() < mod1_inputs.size()) {
RTLIL::SigSpec inputs0 = inputs, inputs1 = inputs;
- inputs0.append(RTLIL::Const(0, 1));
- inputs1.append(RTLIL::Const(1, 1));
+ inputs0.append(State::S0);
+ inputs1.append(State::S1);
run_checker(inputs0);
run_checker(inputs1);
return;
diff --git a/passes/sat/expose.cc b/passes/sat/expose.cc
index 71ce1683d..29dfc7b19 100644
--- a/passes/sat/expose.cc
+++ b/passes/sat/expose.cc
@@ -143,7 +143,7 @@ void create_dff_dq_map(std::map<RTLIL::IdString, dff_map_info_t> &map, RTLIL::De
continue;
}
- if (info.cell->type == "$_DFF_N_" || info.cell->type == "$_DFF_P_") {
+ if (info.cell->type.in("$_DFF_N_", "$_DFF_P_")) {
info.bit_clk = sigmap(info.cell->getPort("\\C")).as_bit();
info.clk_polarity = info.cell->type == "$_DFF_P_";
info.bit_d = sigmap(info.cell->getPort("\\D")).as_bit();
@@ -151,7 +151,7 @@ void create_dff_dq_map(std::map<RTLIL::IdString, dff_map_info_t> &map, RTLIL::De
continue;
}
- if (info.cell->type.size() == 10 && info.cell->type.substr(0, 6) == "$_DFF_") {
+ if (info.cell->type.size() == 10 && info.cell->type.begins_with("$_DFF_")) {
info.bit_clk = sigmap(info.cell->getPort("\\C")).as_bit();
info.bit_arst = sigmap(info.cell->getPort("\\R")).as_bit();
info.clk_polarity = info.cell->type[6] == 'P';
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc
index 1a886af70..49ef40061 100644
--- a/passes/sat/miter.cc
+++ b/passes/sat/miter.cc
@@ -59,7 +59,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
}
break;
}
- if (argidx+3 != args.size() || args[argidx].substr(0, 1) == "-")
+ if (argidx+3 != args.size() || args[argidx].compare(0, 1, "-") == 0)
that->cmd_error(args, argidx, "command argument error");
RTLIL::IdString gold_name = RTLIL::escape_id(args[argidx++]);
@@ -236,7 +236,7 @@ void create_miter_equiv(struct Pass *that, std::vector<std::string> args, RTLIL:
if (flag_make_assert) {
RTLIL::Cell *assert_cell = miter_module->addCell(NEW_ID, "$assert");
assert_cell->setPort("\\A", all_conditions);
- assert_cell->setPort("\\EN", RTLIL::SigSpec(1, 1));
+ assert_cell->setPort("\\EN", State::S1);
}
RTLIL::Wire *w_trigger = miter_module->addWire("\\trigger");
@@ -279,7 +279,7 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL
}
break;
}
- if ((argidx+1 != args.size() && argidx+2 != args.size()) || args[argidx].substr(0, 1) == "-")
+ if ((argidx+1 != args.size() && argidx+2 != args.size()) || args[argidx].compare(0, 1, "-") == 0)
that->cmd_error(args, argidx, "command argument error");
IdString module_name = RTLIL::escape_id(args[argidx++]);
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index cbba738f0..dd56d8c71 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -519,7 +519,7 @@ struct SatHelper
for (auto &p : d->connections()) {
if (d->type == "$dff" && p.first == "\\CLK")
continue;
- if (d->type.substr(0, 6) == "$_DFF_" && p.first == "\\C")
+ if (d->type.begins_with("$_DFF_") && p.first == "\\C")
continue;
queued_signals.add(handled_signals.remove(sigmap(p.second)));
}
@@ -659,6 +659,7 @@ struct SatHelper
void dump_model_to_vcd(std::string vcd_file_name)
{
+ rewrite_filename(vcd_file_name);
FILE *f = fopen(vcd_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", vcd_file_name.c_str(), strerror(errno));
@@ -761,6 +762,7 @@ struct SatHelper
void dump_model_to_json(std::string json_file_name)
{
+ rewrite_filename(json_file_name);
FILE *f = fopen(json_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", json_file_name.c_str(), strerror(errno));
@@ -795,7 +797,7 @@ struct SatHelper
vector<string> data;
string name = wd.first.c_str();
- while (name.substr(0, 1) == "\\")
+ while (name.compare(0, 1, "\\") == 0)
name = name.substr(1);
fprintf(f, " { \"name\": \"%s\", \"wave\": \"", name.c_str());
@@ -1351,7 +1353,7 @@ struct SatPass : public Pass {
if (show_regs) {
pool<Wire*> reg_wires;
for (auto cell : module->cells()) {
- if (cell->type == "$dff" || cell->type.substr(0, 6) == "$_DFF_")
+ if (cell->type == "$dff" || cell->type.begins_with("$_DFF_"))
for (auto bit : cell->getPort("\\Q"))
if (bit.wire)
reg_wires.insert(bit.wire);
@@ -1505,6 +1507,7 @@ struct SatPass : public Pass {
{
if (!cnf_file_name.empty())
{
+ rewrite_filename(cnf_file_name);
FILE *f = fopen(cnf_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
@@ -1608,6 +1611,7 @@ struct SatPass : public Pass {
if (!cnf_file_name.empty())
{
+ rewrite_filename(cnf_file_name);
FILE *f = fopen(cnf_file_name.c_str(), "w");
if (!f)
log_cmd_error("Can't open output file `%s' for writing: %s\n", cnf_file_name.c_str(), strerror(errno));
generated by cgit v1.2.3 (git 2.25.1) at 2025-06-04 18:32:08 +0000