riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

chformal: Support $check cells and add chformal -lower 

This adds support for `$check` cells in chformal and adds a `-lower`
mode which converts `$check` cells into `$assert` etc. cells with a
`$print` cell to output the `$check` message.
This commit is contained in:
Jannis Harder 2024-01-22 18:30:24 +01:00
parent 331ac5285f
commit 6c4902313b
1 changed files with 158 additions and 25 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

159
passes/cmds/chformal.cc
View File

@ -23,6 +23,52 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
static RTLIL::IdString formal_flavor(RTLIL::Cell *cell)
{
if (cell->type != ID($check))
return cell->type;
std::string flavor_param = cell->getParam(ID(FLAVOR)).decode_string();
if (flavor_param == "assert")
return ID($assert);
else if (flavor_param == "assume")
return ID($assume);
else if (flavor_param == "cover")
return ID($cover);
else if (flavor_param == "live")
return ID($live);
else if (flavor_param == "fair")
return ID($fair);
else
log_abort();
}
static void set_formal_flavor(RTLIL::Cell *cell, RTLIL::IdString flavor)
{
if (cell->type != ID($check)) {
cell->type = flavor;
return;
}
if (flavor == ID($assert))
cell->setParam(ID(FLAVOR), std::string("assert"));
else if (flavor == ID($assume))
cell->setParam(ID(FLAVOR), std::string("assume"));
else if (flavor == ID($cover))
cell->setParam(ID(FLAVOR), std::string("cover"));
else if (flavor == ID($live))
cell->setParam(ID(FLAVOR), std::string("live"));
else if (flavor == ID($fair))
cell->setParam(ID(FLAVOR), std::string("fair"));
else
log_abort();
}
static bool is_triggered_check_cell(RTLIL::Cell * cell)
{
return cell->type == ID($check) && cell->getParam(ID(TRG_ENABLE)).as_bool();
}
struct ChformalPass : public Pass {
ChformalPass() : Pass("chformal", "change formal constraints of the design") { }
void help() override
@ -41,13 +87,18 @@ struct ChformalPass : public Pass {
log(" -fair $fair cells, representing assume(s_eventually ...)\n");
log(" -cover $cover cells, representing cover() statements\n");
log("\n");
log(" Additionally chformal will operate on $check cells corresponding to the\n");
log(" selected constraint types.\n");
log("\n");
log("Exactly one of the following modes must be specified:\n");
log("\n");
log(" -remove\n");
log(" remove the cells and thus constraints from the design\n");
log("\n");
log(" -early\n");
log(" bypass FFs that only delay the activation of a constraint\n");
log(" bypass FFs that only delay the activation of a constraint. When inputs\n");
log(" of the bypassed FFs do not remain stable between clock edges, this may\n");
log(" result in unexpected behavior.\n");
log("\n");
log(" -delay <N>\n");
log(" delay activation of the constraint by <N> clock cycles\n");
@ -69,6 +120,11 @@ struct ChformalPass : public Pass {
log(" -fair2live\n");
log(" change the roles of cells as indicated. these options can be combined\n");
log("\n");
log(" -lower\n");
log(" convert each $check cell into an $assert, $assume, $live, $fair or\n");
log(" $cover cell. If the $check cell contains a message, also produce a\n");
log(" $print cell.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
@ -146,6 +202,10 @@ struct ChformalPass : public Pass {
mode = 'c';
continue;
}
if (mode == 0 && args[argidx] == "-lower") {
mode = 'l';
continue;
}
break;
}
extra_args(args, argidx, design);
@ -166,7 +226,7 @@ struct ChformalPass : public Pass {
vector<Cell*> constr_cells;
for (auto cell : module->selected_cells())
if (constr_types.count(cell->type))
if (constr_types.count(formal_flavor(cell)))
constr_cells.push_back(cell);
if (mode == 'r')
@ -216,6 +276,18 @@ struct ChformalPass : public Pass {
}
for (auto cell : constr_cells)
{
if (is_triggered_check_cell(cell)) {
if (cell->getParam(ID::TRG_WIDTH).as_int() != 1)
continue;
cell->setPort(ID::TRG, SigSpec());
cell->setParam(ID::TRG_ENABLE, false);
cell->setParam(ID::TRG_WIDTH, 0);
cell->setParam(ID::TRG_POLARITY, false);
}
IdString flavor = formal_flavor(cell);
while (true)
{
SigSpec A = sigmap(cell->getPort(ID::A));
@ -225,8 +297,8 @@ struct ChformalPass : public Pass {
break;
if (!init_zero.count(EN)) {
if (cell->type == ID($cover)) break;
if (cell->type.in(ID($assert), ID($assume)) && !init_one.count(A)) break;
if (flavor == ID($cover)) break;
if (flavor.in(ID($assert), ID($assume)) && !init_one.count(A)) break;
}
const auto &A_map = ffmap.at(A);
@ -239,10 +311,15 @@ struct ChformalPass : public Pass {
cell->setPort(ID::EN, EN_map.first);
}
}
}
else
if (mode == 'd')
{
for (auto cell : constr_cells)
{
if (is_triggered_check_cell(cell))
log_error("Cannot delay edge triggered $check cell %s, run async2sync or clk2fflogic first.\n", log_id(cell));
for (int i = 0; i < mode_arg; i++)
{
SigSpec orig_a = cell->getPort(ID::A);
@ -259,6 +336,7 @@ struct ChformalPass : public Pass {
cell->setPort(ID::EN, new_en);
}
}
}
else
if (mode == 's')
{
@ -278,21 +356,76 @@ struct ChformalPass : public Pass {
if (mode =='p')
{
for (auto cell : constr_cells)
{
if (cell->type == ID($check)) {
Cell *cover = module->addCell(NEW_ID_SUFFIX("coverenable"), ID($check));
cover->attributes = cell->attributes;
cover->parameters = cell->parameters;
cover->setParam(ID(FLAVOR), Const("cover"));
for (auto const &conn : cell->connections())
if (!conn.first.in(ID::A, ID::EN))
cover->setPort(conn.first, conn.second);
cover->setPort(ID::A, cell->getPort(ID::EN));
cover->setPort(ID::EN, State::S1);
} else {
module->addCover(NEW_ID_SUFFIX("coverenable"),
cell->getPort(ID::EN), State::S1, cell->get_src_attribute());
}
}
}
else
if (mode == 'c')
{
for (auto cell : constr_cells)
if (assert2assume && cell->type == ID($assert))
cell->type = ID($assume);
else if (assume2assert && cell->type == ID($assume))
cell->type = ID($assert);
else if (live2fair && cell->type == ID($live))
cell->type = ID($fair);
else if (fair2live && cell->type == ID($fair))
cell->type = ID($live);
for (auto cell : constr_cells) {
IdString flavor = formal_flavor(cell);
if (assert2assume && flavor == ID($assert))
set_formal_flavor(cell, ID($assume));
else if (assume2assert && flavor == ID($assume))
set_formal_flavor(cell, ID($assert));
else if (live2fair && flavor == ID($live))
set_formal_flavor(cell, ID($fair));
else if (fair2live && flavor == ID($fair))
set_formal_flavor(cell, ID($live));
}
}
else
if (mode == 'l')
{
for (auto cell : constr_cells) {
if (cell->type != ID($check))
continue;
if (is_triggered_check_cell(cell))
log_error("Cannot lower edge triggered $check cell %s, run async2sync or clk2fflogic first.\n", log_id(cell));
Cell *plain_cell = module->addCell(NEW_ID, formal_flavor(cell));
plain_cell->attributes = cell->attributes;
SigBit sig_a = cell->getPort(ID::A);
SigBit sig_en = cell->getPort(ID::EN);
plain_cell->setPort(ID::A, sig_a);
plain_cell->setPort(ID::EN, sig_en);
if (plain_cell->type.in(ID($assert), ID($assume)))
sig_a = module->Not(NEW_ID, sig_a);
SigBit combined_en = module->And(NEW_ID, sig_a, sig_en);
module->swap_names(cell, plain_cell);
if (cell->getPort(ID::ARGS).empty()) {
module->remove(cell);
} else {
cell->type = ID($print);
cell->setPort(ID::EN, combined_en);
cell->unsetPort(ID::A);
cell->unsetParam(ID(FLAVOR));
}
}
}
}
}