mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-24 09:35:32 +00:00
ebd6d5f85b
Linking to optiongroups doesn't add *that* much, and is kind of a pain; meanwhile having the optiongroups adds an extra level of indentation. Instead of options needing to be in an option group, they instead go in either the root node or nested in a usage node. Putting them in a usage node allows for more-or-less the previous behaviour but without making it the default.
435 lines
13 KiB
C++
435 lines
13 KiB
C++
/*
|
|
* yosys -- Yosys Open SYnthesis Suite
|
|
*
|
|
* 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
|
|
* copyright notice and this permission notice appear in all copies.
|
|
*
|
|
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
|
|
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
|
|
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
|
|
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
|
|
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
|
|
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
|
|
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
|
|
*
|
|
*/
|
|
|
|
#include "kernel/yosys.h"
|
|
#include "kernel/sigtools.h"
|
|
#include "kernel/log_help.h"
|
|
|
|
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") {}
|
|
|
|
bool formatted_help() override {
|
|
auto *help = PrettyHelp::get_current();
|
|
help->set_group("formal");
|
|
|
|
auto content_root = help->get_root();
|
|
|
|
content_root->usage("chformal [types] [mode] [options] [selection]");
|
|
content_root->paragraph(
|
|
"Make changes to the formal constraints of the design. The [types] options "
|
|
"the type of constraint to operate on. If none of the following options are "
|
|
"given, the command will operate on all constraint types:"
|
|
);
|
|
|
|
content_root->option("-assert", "`$assert` cells, representing ``assert(...)`` constraints");
|
|
content_root->option("-assume", "`$assume` cells, representing ``assume(...)`` constraints");
|
|
content_root->option("-live", "`$live` cells, representing ``assert(s_eventually ...)``");
|
|
content_root->option("-fair", "`$fair` cells, representing ``assume(s_eventually ...)``");
|
|
content_root->option("-cover", "`$cover` cells, representing ``cover()`` statements");
|
|
content_root->paragraph(
|
|
"Additionally chformal will operate on `$check` cells corresponding to the "
|
|
"selected constraint types."
|
|
);
|
|
|
|
content_root->paragraph("Exactly one of the following modes must be specified:");
|
|
|
|
content_root->option("-remove", "remove the cells and thus constraints from the design");
|
|
content_root->option("-early",
|
|
"bypass FFs that only delay the activation of a constraint. When inputs "
|
|
"of the bypassed FFs do not remain stable between clock edges, this may "
|
|
"result in unexpected behavior."
|
|
);
|
|
content_root->option("-delay <N>", "delay activation of the constraint by <N> clock cycles");
|
|
content_root->option("-skip <N>", "ignore activation of the constraint in the first <N> clock cycles");
|
|
auto cover_option = content_root->open_option("-coverenable");
|
|
cover_option->paragraph(
|
|
"add cover statements for the enable signals of the constraints"
|
|
);
|
|
#ifdef YOSYS_ENABLE_VERIFIC
|
|
cover_option->paragraph(
|
|
"Note: For the Verific frontend it is currently not guaranteed that a "
|
|
"reachable SVA statement corresponds to an active enable signal."
|
|
);
|
|
#endif
|
|
content_root->option("-assert2assume");
|
|
content_root->option("-assume2assert");
|
|
content_root->option("-live2fair");
|
|
content_root->option("-fair2live", "change the roles of cells as indicated. these options can be combined");
|
|
content_root->option("-lower",
|
|
"convert each $check cell into an $assert, $assume, $live, $fair or "
|
|
"$cover cell. If the $check cell contains a message, also produce a "
|
|
"$print cell."
|
|
);
|
|
return true;
|
|
}
|
|
void execute(std::vector<std::string> args, RTLIL::Design *design) override
|
|
{
|
|
bool assert2assume = false;
|
|
bool assume2assert = false;
|
|
bool live2fair = false;
|
|
bool fair2live = false;
|
|
|
|
pool<IdString> constr_types;
|
|
char mode = 0;
|
|
int mode_arg = 0;
|
|
|
|
size_t argidx;
|
|
for (argidx = 1; argidx < args.size(); argidx++)
|
|
{
|
|
if (args[argidx] == "-assert") {
|
|
constr_types.insert(ID($assert));
|
|
continue;
|
|
}
|
|
if (args[argidx] == "-assume") {
|
|
constr_types.insert(ID($assume));
|
|
continue;
|
|
}
|
|
if (args[argidx] == "-live") {
|
|
constr_types.insert(ID($live));
|
|
continue;
|
|
}
|
|
if (args[argidx] == "-fair") {
|
|
constr_types.insert(ID($fair));
|
|
continue;
|
|
}
|
|
if (args[argidx] == "-cover") {
|
|
constr_types.insert(ID($cover));
|
|
continue;
|
|
}
|
|
if (mode == 0 && args[argidx] == "-remove") {
|
|
mode = 'r';
|
|
continue;
|
|
}
|
|
if (mode == 0 && args[argidx] == "-early") {
|
|
mode = 'e';
|
|
continue;
|
|
}
|
|
if (mode == 0 && args[argidx] == "-delay" && argidx+1 < args.size()) {
|
|
mode = 'd';
|
|
mode_arg = atoi(args[++argidx].c_str());
|
|
continue;
|
|
}
|
|
if (mode == 0 && args[argidx] == "-skip" && argidx+1 < args.size()) {
|
|
mode = 's';
|
|
mode_arg = atoi(args[++argidx].c_str());
|
|
continue;
|
|
}
|
|
if (mode == 0 && args[argidx] == "-coverenable") {
|
|
mode = 'p';
|
|
continue;
|
|
}
|
|
if ((mode == 0 || mode == 'c') && args[argidx] == "-assert2assume") {
|
|
assert2assume = true;
|
|
mode = 'c';
|
|
continue;
|
|
}
|
|
if ((mode == 0 || mode == 'c') && args[argidx] == "-assume2assert") {
|
|
assume2assert = true;
|
|
mode = 'c';
|
|
continue;
|
|
}
|
|
if ((mode == 0 || mode == 'c') && args[argidx] == "-live2fair") {
|
|
live2fair = true;
|
|
mode = 'c';
|
|
continue;
|
|
}
|
|
if ((mode == 0 || mode == 'c') && args[argidx] == "-fair2live") {
|
|
fair2live = true;
|
|
mode = 'c';
|
|
continue;
|
|
}
|
|
if (mode == 0 && args[argidx] == "-lower") {
|
|
mode = 'l';
|
|
continue;
|
|
}
|
|
break;
|
|
}
|
|
extra_args(args, argidx, design);
|
|
|
|
if (constr_types.empty()) {
|
|
constr_types.insert(ID($assert));
|
|
constr_types.insert(ID($assume));
|
|
constr_types.insert(ID($live));
|
|
constr_types.insert(ID($fair));
|
|
constr_types.insert(ID($cover));
|
|
}
|
|
|
|
if (mode == 0)
|
|
log_cmd_error("Mode option is missing.\n");
|
|
|
|
for (auto module : design->selected_modules())
|
|
{
|
|
vector<Cell*> constr_cells;
|
|
|
|
for (auto cell : module->selected_cells())
|
|
if (constr_types.count(formal_flavor(cell)))
|
|
constr_cells.push_back(cell);
|
|
|
|
if (mode == 'r')
|
|
{
|
|
for (auto cell : constr_cells)
|
|
module->remove(cell);
|
|
}
|
|
else
|
|
if (mode == 'e')
|
|
{
|
|
SigMap sigmap(module);
|
|
dict<SigBit, pair<SigBit, pair<SigBit, bool>>> ffmap;
|
|
pool<SigBit> init_zero, init_one;
|
|
|
|
for (auto wire : module->wires())
|
|
{
|
|
if (wire->attributes.count(ID::init) == 0)
|
|
continue;
|
|
|
|
SigSpec initsig = sigmap(wire);
|
|
Const initval = wire->attributes.at(ID::init);
|
|
|
|
for (int i = 0; i < GetSize(initsig) && i < GetSize(initval); i++) {
|
|
if (initval[i] == State::S0)
|
|
init_zero.insert(initsig[i]);
|
|
if (initval[i] == State::S1)
|
|
init_one.insert(initsig[i]);
|
|
}
|
|
}
|
|
|
|
for (auto cell : module->selected_cells())
|
|
{
|
|
if (cell->type == ID($ff)) {
|
|
SigSpec D = sigmap(cell->getPort(ID::D));
|
|
SigSpec Q = sigmap(cell->getPort(ID::Q));
|
|
for (int i = 0; i < GetSize(D); i++)
|
|
ffmap[Q[i]] = make_pair(D[i], make_pair(State::Sm, false));
|
|
}
|
|
if (cell->type == ID($dff)) {
|
|
SigSpec D = sigmap(cell->getPort(ID::D));
|
|
SigSpec Q = sigmap(cell->getPort(ID::Q));
|
|
SigSpec C = sigmap(cell->getPort(ID::CLK));
|
|
bool clockpol = cell->getParam(ID::CLK_POLARITY).as_bool();
|
|
for (int i = 0; i < GetSize(D); i++)
|
|
ffmap[Q[i]] = make_pair(D[i], make_pair(C, clockpol));
|
|
}
|
|
}
|
|
|
|
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));
|
|
SigSpec EN = sigmap(cell->getPort(ID::EN));
|
|
|
|
if (ffmap.count(A) == 0 || ffmap.count(EN) == 0)
|
|
break;
|
|
|
|
if (!init_zero.count(EN)) {
|
|
if (flavor == ID($cover)) break;
|
|
if (flavor.in(ID($assert), ID($assume)) && !init_one.count(A)) break;
|
|
}
|
|
|
|
const auto &A_map = ffmap.at(A);
|
|
const auto &EN_map = ffmap.at(EN);
|
|
|
|
if (A_map.second != EN_map.second)
|
|
break;
|
|
|
|
cell->setPort(ID::A, A_map.first);
|
|
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);
|
|
SigSpec orig_en = cell->getPort(ID::EN);
|
|
|
|
Wire *new_a = module->addWire(NEW_ID);
|
|
Wire *new_en = module->addWire(NEW_ID);
|
|
new_en->attributes[ID::init] = State::S0;
|
|
|
|
module->addFf(NEW_ID, orig_a, new_a);
|
|
module->addFf(NEW_ID, orig_en, new_en);
|
|
|
|
cell->setPort(ID::A, new_a);
|
|
cell->setPort(ID::EN, new_en);
|
|
}
|
|
}
|
|
}
|
|
else
|
|
if (mode == 's')
|
|
{
|
|
SigSpec en = State::S1;
|
|
|
|
for (int i = 0; i < mode_arg; i++) {
|
|
Wire *w = module->addWire(NEW_ID);
|
|
w->attributes[ID::init] = State::S0;
|
|
module->addFf(NEW_ID, en, w);
|
|
en = w;
|
|
}
|
|
|
|
for (auto cell : constr_cells)
|
|
cell->setPort(ID::EN, module->LogicAnd(NEW_ID, en, cell->getPort(ID::EN)));
|
|
}
|
|
else
|
|
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) {
|
|
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));
|
|
}
|
|
}
|
|
}
|
|
}
|
|
}
|
|
} ChformalPass;
|
|
|
|
PRIVATE_NAMESPACE_END
|