aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--frontends/verific/verific.cc20
-rw-r--r--kernel/rtlil.cc5
-rw-r--r--passes/pmgen/xilinx_dsp_cascade.pmg2
-rw-r--r--passes/sat/qbfsat.cc28
-rw-r--r--techlibs/ecp5/ecp5_gsr.cc2
-rw-r--r--techlibs/intel_alm/synth_intel_alm.cc10
-rw-r--r--techlibs/xilinx/xilinx_dffopt.cc9
-rw-r--r--tests/arch/ice40/ice40_dsp.ys1
-rw-r--r--tests/arch/intel_alm/quartus_ice.ys12
-rw-r--r--tests/arch/xilinx/xilinx_dffopt.ys35
-rw-r--r--tests/arch/xilinx/xilinx_dsp.ys1
11 files changed, 98 insertions, 27 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 519151310..ae7fcefa7 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1153,6 +1153,26 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
for (auto net : anyseq_nets)
module->connect(net_map_at(net), module->Anyseq(new_verific_id(net)));
+ char *id_name;
+ TypeRange *type_range;
+ FOREACH_MAP_ITEM(nl->GetTypeRangeTable(), mi, &id_name, &type_range)
+ {
+ if (!type_range)
+ continue;
+ if (!type_range->IsTypeEnum())
+ continue;
+ auto wire = module->wire(RTLIL::escape_id(id_name));
+ log_assert(wire);
+ wire->set_string_attribute(ID(wiretype), type_range->GetTypeName());
+
+ MapIter mj;
+ char *k, *v;
+ FOREACH_MAP_ITEM(type_range->GetEnumIdMap(), mj, &k, &v) {
+ IdString key = stringf("\\enum_value_%s", v);
+ wire->set_string_attribute(key, k);
+ }
+ }
+
pool<Instance*, hash_ptr_ops> sva_asserts;
pool<Instance*, hash_ptr_ops> sva_assumes;
pool<Instance*, hash_ptr_ops> sva_covers;
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 2aefe30b1..196e301b6 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -2619,16 +2619,15 @@ void RTLIL::Cell::setParam(RTLIL::IdString paramname, RTLIL::Const value)
const RTLIL::Const &RTLIL::Cell::getParam(RTLIL::IdString paramname) const
{
- static const RTLIL::Const empty;
const auto &it = parameters.find(paramname);
if (it != parameters.end())
return it->second;
if (module && module->design) {
RTLIL::Module *m = module->design->module(type);
if (m)
- return m->parameter_default_values.at(paramname, empty);
+ return m->parameter_default_values.at(paramname);
}
- return empty;
+ throw std::out_of_range("Cell::getParam()");
}
void RTLIL::Cell::sort()
diff --git a/passes/pmgen/xilinx_dsp_cascade.pmg b/passes/pmgen/xilinx_dsp_cascade.pmg
index a36edd9e5..8babb88e6 100644
--- a/passes/pmgen/xilinx_dsp_cascade.pmg
+++ b/passes/pmgen/xilinx_dsp_cascade.pmg
@@ -188,7 +188,7 @@ arg next
// driven by the 'P' output of the previous DSP cell, and (c) has its
// 'PCIN' port unused
match nextP
- select !param(nextP, \CREG).as_bool()
+ select !nextP->type.in(\DSP48E1) || !param(nextP, \CREG).as_bool()
select (nextP->type.in(\DSP48A, \DSP48A1) && port(nextP, \OPMODE, Const(0, 8)).extract(2,2) == Const::from_string("11")) || (nextP->type.in(\DSP48E1) && port(nextP, \OPMODE, Const(0, 7)).extract(4,3) == Const::from_string("011"))
select nusers(port(nextP, \C, SigSpec())) > 1
select nusers(port(nextP, \PCIN, SigSpec())) == 0
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc
index e9b4913cd..d99ca1b53 100644
--- a/passes/sat/qbfsat.cc
+++ b/passes/sat/qbfsat.cc
@@ -49,15 +49,15 @@ struct QbfSolutionType {
};
struct QbfSolveOptions {
- bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs;
+ bool specialize, specialize_from_file, write_solution, nocleanup, dump_final_smt2, assume_outputs, assume_neg;
bool sat, unsat, show_smtbmc;
std::string specialize_soln_file;
std::string write_soln_soln_file;
std::string dump_final_smt2_file;
size_t argidx;
QbfSolveOptions() : specialize(false), specialize_from_file(false), write_solution(false),
- nocleanup(false), dump_final_smt2(false), assume_outputs(false), sat(false), unsat(false),
- show_smtbmc(false), argidx(0) {};
+ nocleanup(false), dump_final_smt2(false), assume_outputs(false), assume_neg(false),
+ sat(false), unsat(false), show_smtbmc(false), argidx(0) {};
};
void recover_solution(QbfSolutionType &sol) {
@@ -239,7 +239,7 @@ void allconstify_inputs(RTLIL::Module *module, const pool<std::string> &input_wi
module->fixup_ports();
}
-void assume_miter_outputs(RTLIL::Module *module) {
+void assume_miter_outputs(RTLIL::Module *module, const QbfSolveOptions &opt) {
std::vector<RTLIL::Wire *> wires_to_assume;
for (auto w : module->wires())
if (w->port_output && w->width == 1)
@@ -254,7 +254,14 @@ void assume_miter_outputs(RTLIL::Module *module) {
log("\n");
}
- for(auto i = 0; wires_to_assume.size() > 1; ++i) {
+ if (opt.assume_neg) {
+ for (unsigned int i = 0; i < wires_to_assume.size(); ++i) {
+ RTLIL::SigSpec n_wire = module->LogicNot(wires_to_assume[i]->name.str() + "__n__qbfsat", wires_to_assume[i], false, wires_to_assume[i]->get_src_attribute());
+ wires_to_assume[i] = n_wire.as_wire();
+ }
+ }
+
+ for (auto i = 0; wires_to_assume.size() > 1; ++i) {
std::vector<RTLIL::Wire *> buf;
for (auto j = 0; j + 1 < GetSize(wires_to_assume); j += 2) {
std::stringstream strstr; strstr << i << "_" << j;
@@ -368,6 +375,10 @@ QbfSolveOptions parse_args(const std::vector<std::string> &args) {
opt.assume_outputs = true;
continue;
}
+ else if (args[opt.argidx] == "-assume-negative-polarity") {
+ opt.assume_neg = true;
+ continue;
+ }
else if (args[opt.argidx] == "-sat") {
opt.sat = true;
continue;
@@ -461,6 +472,11 @@ struct QbfSatPass : public Pass {
log(" -assume-outputs\n");
log(" Add an $assume cell for the conjunction of all one-bit module output wires.\n");
log("\n");
+ log(" -assume-negative-polarity\n");
+ log(" When adding $assume cells for one-bit module output wires, assume they are\n");
+ log(" negative polarity signals and should always be low, for example like the\n");
+ log(" miters created with the `miter` command.\n");
+ log("\n");
log(" -sat\n");
log(" Generate an error if the solver does not return \"sat\".\n");
log("\n");
@@ -509,7 +525,7 @@ struct QbfSatPass : public Pass {
pool<std::string> input_wires = validate_design_and_get_inputs(module, opt);
allconstify_inputs(module, input_wires);
if (opt.assume_outputs)
- assume_miter_outputs(module);
+ assume_miter_outputs(module, opt);
QbfSolutionType ret = qbf_solve(module, opt);
Pass::call(design, "design -pop");
diff --git a/techlibs/ecp5/ecp5_gsr.cc b/techlibs/ecp5/ecp5_gsr.cc
index 1c69e1d79..3d3f8e1c1 100644
--- a/techlibs/ecp5/ecp5_gsr.cc
+++ b/techlibs/ecp5/ecp5_gsr.cc
@@ -81,7 +81,7 @@ struct Ecp5GsrPass : public Pass {
for (auto cell : module->selected_cells())
{
- if (cell->getParam(ID(GSR)).decode_string() != "AUTO")
+ if (!cell->hasParam(ID(GSR)) || cell->getParam(ID(GSR)).decode_string() != "AUTO")
continue;
bool gsren = found_gsr;
diff --git a/techlibs/intel_alm/synth_intel_alm.cc b/techlibs/intel_alm/synth_intel_alm.cc
index 47aa11500..5d4c78d74 100644
--- a/techlibs/intel_alm/synth_intel_alm.cc
+++ b/techlibs/intel_alm/synth_intel_alm.cc
@@ -200,6 +200,8 @@ struct SynthIntelALMPass : public ScriptPass {
if (check_label("map_ffs")) {
run("dff2dffe -direct-match $_DFF_*");
+ // As mentioned in common/dff_sim.v, Intel flops power up to zero,
+ // so use `zinit` to add inverters where needed.
run("zinit");
run("techmap -map +/techmap.v -map +/intel_alm/common/dff_map.v");
run("opt -full -undriven -mux_undef");
@@ -223,8 +225,16 @@ struct SynthIntelALMPass : public ScriptPass {
if (check_label("quartus")) {
if (quartus || help_mode) {
+ // Quartus ICEs if you have a wire which has `[]` in its name,
+ // which Yosys produces when building memories out of flops.
+ run("rename -hide w:*[* w:*]*");
+ // VQM mode does not support 'x, so replace those with zero.
run("setundef -zero");
+ // VQM mode does not support multi-bit constant assignments
+ // (e.g. 2'b00 is an error), so as a workaround use references
+ // to constant driver cells, which Quartus accepts.
run("hilomap -singleton -hicell __MISTRAL_VCC Q -locell __MISTRAL_GND Q");
+ // Rename from Yosys-internal MISTRAL_* cells to Quartus cells.
run("techmap -map +/intel_alm/common/quartus_rename.v");
run(stringf("techmap -map +/intel_alm/%s/quartus_rename.v", family_opt.c_str()));
}
diff --git a/techlibs/xilinx/xilinx_dffopt.cc b/techlibs/xilinx/xilinx_dffopt.cc
index c608db883..c9d63c9f7 100644
--- a/techlibs/xilinx/xilinx_dffopt.cc
+++ b/techlibs/xilinx/xilinx_dffopt.cc
@@ -292,18 +292,21 @@ unmap:
LutData final_lut;
if (worthy_post_r) {
final_lut = lut_d_post_r;
- log(" Merging R LUT for %s/%s (%d -> %d)\n", log_id(cell), log_id(sig_Q.wire), GetSize(lut_d.second), GetSize(final_lut.second));
} else if (worthy_post_s) {
final_lut = lut_d_post_s;
- log(" Merging S LUT for %s/%s (%d -> %d)\n", log_id(cell), log_id(sig_Q.wire), GetSize(lut_d.second), GetSize(final_lut.second));
} else if (worthy_post_ce) {
final_lut = lut_d_post_ce;
- log(" Merging CE LUT for %s/%s (%d -> %d)\n", log_id(cell), log_id(sig_Q.wire), GetSize(lut_d.second), GetSize(final_lut.second));
} else {
// Nothing to do here.
continue;
}
+ std::string ports;
+ if (worthy_post_r) ports += " + R";
+ if (worthy_post_s) ports += " + S";
+ if (worthy_post_ce) ports += " + CE";
+ log(" Merging D%s LUTs for %s/%s (%d -> %d)\n", ports.c_str(), log_id(cell), log_id(sig_Q.wire), GetSize(lut_d.second), GetSize(final_lut.second));
+
// Okay, we're doing it. Unmap ports.
if (worthy_post_r) {
cell->unsetParam(ID(IS_R_INVERTED));
diff --git a/tests/arch/ice40/ice40_dsp.ys b/tests/arch/ice40/ice40_dsp.ys
index 250273859..b13e525fd 100644
--- a/tests/arch/ice40/ice40_dsp.ys
+++ b/tests/arch/ice40/ice40_dsp.ys
@@ -8,4 +8,5 @@ assign o4 = a * b;
SB_MAC16 m3 (.A(a), .B(b), .O(o5));
endmodule
EOT
+read_verilog -lib +/ice40/cells_sim.v
ice40_dsp
diff --git a/tests/arch/intel_alm/quartus_ice.ys b/tests/arch/intel_alm/quartus_ice.ys
new file mode 100644
index 000000000..4b9b54d10
--- /dev/null
+++ b/tests/arch/intel_alm/quartus_ice.ys
@@ -0,0 +1,12 @@
+read_verilog <<EOT
+// Verilog has syntax for raw identifiers, where you start it with \ and end it with a space.
+// This test crashes Quartus due to it parsing \a[10] as a wire slice and not a raw identifier.
+module top();
+ (* keep *) wire [31:0] \a[10] ;
+ (* keep *) wire b;
+ assign b = \a[10] [31];
+endmodule
+EOT
+
+synth_intel_alm -family cyclonev -quartus
+select -assert-none w:*[* w:*]*
diff --git a/tests/arch/xilinx/xilinx_dffopt.ys b/tests/arch/xilinx/xilinx_dffopt.ys
index dc036acfd..2c729832e 100644
--- a/tests/arch/xilinx/xilinx_dffopt.ys
+++ b/tests/arch/xilinx/xilinx_dffopt.ys
@@ -18,17 +18,17 @@ FDRE ff (.D(tmp[0]), .CE(tmp[1]), .R(tmp[2]), .Q(o[0]));
endmodule
EOT
-
+read_verilog -lib +/xilinx/cells_sim.v
design -save t0
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
design -load postopt
clean
+cd t0
select -assert-count 1 t:FDRE
select -assert-count 1 t:LUT6
-select -assert-count 3 t:LUT2
-select -assert-none t:FDRE t:LUT6 t:LUT2 %% t:* %D
+select -assert-none t:FDRE t:LUT6 %% t:* %D
design -load t0
@@ -36,9 +36,10 @@ equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim
design -load postopt
clean
+cd t0
select -assert-count 1 t:FDRE
select -assert-count 1 t:LUT4
-select -assert-count 3 t:LUT2
+select -assert-count 1 t:LUT2
select -assert-none t:FDRE t:LUT4 t:LUT2 %% t:* %D
design -reset
@@ -65,16 +66,17 @@ endmodule
EOT
+read_verilog -lib +/xilinx/cells_sim.v
design -save t0
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
design -load postopt
clean
+cd t0
select -assert-count 1 t:FDSE
select -assert-count 1 t:LUT6
-select -assert-count 3 t:LUT2
-select -assert-none t:FDSE t:LUT6 t:LUT2 %% t:* %D
+select -assert-none t:FDSE t:LUT6 %% t:* %D
design -load t0
@@ -82,9 +84,10 @@ equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim
design -load postopt
clean
+cd t0
select -assert-count 1 t:FDSE
select -assert-count 1 t:LUT4
-select -assert-count 3 t:LUT2
+select -assert-count 1 t:LUT2
select -assert-none t:FDSE t:LUT4 t:LUT2 %% t:* %D
design -reset
@@ -111,15 +114,17 @@ endmodule
EOT
+read_verilog -lib +/xilinx/cells_sim.v
design -save t0
equiv_opt -async2sync -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
design -load postopt
clean
+cd t0
select -assert-count 1 t:FDCE
select -assert-count 1 t:LUT4
-select -assert-count 3 t:LUT2
+select -assert-count 1 t:LUT2
select -assert-none t:FDCE t:LUT4 t:LUT2 %% t:* %D
design -reset
@@ -145,16 +150,17 @@ endmodule
EOT
+read_verilog -lib +/xilinx/cells_sim.v
design -save t0
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
design -load postopt
clean
+cd t0
select -assert-count 1 t:FDSE
select -assert-count 1 t:LUT5
-select -assert-count 2 t:LUT2
-select -assert-none t:FDSE t:LUT5 t:LUT2 %% t:* %D
+select -assert-none t:FDSE t:LUT5 %% t:* %D
design -load t0
@@ -162,6 +168,7 @@ equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim
design -load postopt
clean
+cd t0
select -assert-count 1 t:FDSE
select -assert-count 2 t:LUT2
select -assert-none t:FDSE t:LUT2 %% t:* %D
@@ -191,16 +198,17 @@ endmodule
EOT
+read_verilog -lib +/xilinx/cells_sim.v
design -save t0
equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim.v xilinx_dffopt
design -load postopt
clean
+cd t0
select -assert-count 1 t:FDRSE
select -assert-count 1 t:LUT6
-select -assert-count 4 t:LUT2
-select -assert-none t:FDRSE t:LUT6 t:LUT2 %% t:* %D
+select -assert-none t:FDRSE t:LUT6 %% t:* %D
design -load t0
@@ -208,9 +216,10 @@ equiv_opt -blacklist xilinx_dffopt_blacklist.txt -assert -map +/xilinx/cells_sim
design -load postopt
clean
+cd t0
select -assert-count 1 t:FDRSE
select -assert-count 1 t:LUT4
-select -assert-count 4 t:LUT2
+select -assert-count 1 t:LUT2
select -assert-none t:FDRSE t:LUT4 t:LUT2 %% t:* %D
design -reset
diff --git a/tests/arch/xilinx/xilinx_dsp.ys b/tests/arch/xilinx/xilinx_dsp.ys
index 3b9f52930..59d8296ab 100644
--- a/tests/arch/xilinx/xilinx_dsp.ys
+++ b/tests/arch/xilinx/xilinx_dsp.ys
@@ -8,4 +8,5 @@ assign o4 = a * b;
DSP48E1 m3 (.A(a), .B(b), .P(o5));
endmodule
EOT
+read_verilog -lib +/xilinx/cells_sim.v
xilinx_dsp
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-14 12:58:50 +0000