Skip to content

Commit

Permalink
WIP: Add new $check cell to represent assertions with a message.
Browse files Browse the repository at this point in the history
  • Loading branch information
@whitequark
whitequark committed Jan 19, 2024
1 parent fc5ff7a commit 6860b15
Show file tree
Hide file tree
Showing 12 changed files with 468 additions and 274 deletions.
363 changes: 229 additions & 134 deletions backends/cxxrtl/cxxrtl_backend.cc
View file

Large diffs are not rendered by default.

21 changes: 21 additions & 0 deletions backends/cxxrtl/runtime/cxxrtl/cxxrtl.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -952,6 +952,20 @@ struct lazy_fmt {
virtual std::string operator() () const = 0;
};

// Flavor of a `$check` cell.
enum class flavor {
// Corresponds to a `$assert` cell in other flows, and a Verilog `assert ()` statement.
ASSERT,
// Corresponds to a `$assume` cell in other flows, and a Verilog `assume ()` statement.
ASSUME,
// Corresponds to a `$live` cell in other flows, and a Verilog `assert (eventually)` statement.
ASSERT_EVENTUALLY,
// Corresponds to a `$fair` cell in other flows, and a Verilog `assume (eventually)` statement.
ASSUME_EVENTUALLY,
// Corresponds to a `$cover` cell in other flows, and a Verilog `cover ()` statement.
COVER
};

// An object that can be passed to a `eval()` method in order to act on side effects.
struct performer {
// Called by generated formatting code to evaluate a Verilog `$time` expression.
Expand All @@ -964,6 +978,13 @@ struct performer {
virtual void on_print(const lazy_fmt &formatter, const metadata_map &attributes) {
std::cout << formatter();
}

// Called when a `$check` cell is triggered.
virtual void on_check(flavor type, bool condition, const lazy_fmt &formatter, const metadata_map &attributes) {
if (type == flavor::ASSERT || type == flavor::ASSUME)
if (!condition)
std::cerr << formatter();
}
};

// An object that can be passed to a `commit()` method in order to produce a replay log of every state change in
Expand Down
78 changes: 70 additions & 8 deletions backends/verilog/verilog_backend.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1041,6 +1041,23 @@ void dump_cell_expr_print(std::ostream &f, std::string indent, const RTLIL::Cell
f << stringf(");\n");
}

void dump_cell_expr_check(std::ostream &f, std::string indent, const RTLIL::Cell *cell)
{
std::string flavor = cell->getParam(ID(FLAVOR)).decode_string();
if (flavor == "assert")
f << stringf("%s" "assert (", indent.c_str());
else if (flavor == "assume")
f << stringf("%s" "assume (", indent.c_str());
else if (flavor == "live")
f << stringf("%s" "assert (eventually ", indent.c_str());
else if (flavor == "fair")
f << stringf("%s" "assume (eventually ", indent.c_str());
else if (flavor == "cover")
f << stringf("%s" "cover (", indent.c_str());
dump_sigspec(f, cell->getPort(ID::A));
f << stringf(");\n");
}

bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
{
if (cell->type == ID($_NOT_)) {
Expand Down Expand Up @@ -1805,6 +1822,35 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true;
}

if (cell->type == ID($check))
{
// Sync $check cells are accumulated and handled in dump_module.
if (cell->getParam(ID::TRG_ENABLE).as_bool())
return true;

f << stringf("%s" "always @*\n", indent.c_str());

f << stringf("%s" " if (", indent.c_str());
dump_sigspec(f, cell->getPort(ID::EN));
f << stringf(") begin\n");

std::string flavor = cell->getParam(ID::FLAVOR).decode_string();
if (flavor == "assert" || flavor == "assume") {
f << stringf("%s" " if (!", indent.c_str());
dump_sigspec(f, cell->getPort(ID::A));
f << stringf(")\n");
dump_cell_expr_print(f, indent + " ", cell);
} else {
f << stringf("%s" " /* message omitted */\n", indent.c_str());
}

dump_cell_expr_check(f, indent + " ", cell);

f << stringf("%s" " end\n", indent.c_str());

return true;
}

// FIXME: $fsm

return false;
Expand Down Expand Up @@ -1894,7 +1940,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
}
}

void dump_sync_print(std::ostream &f, std::string indent, const RTLIL::SigSpec &trg, const RTLIL::Const &polarity, std::vector<const RTLIL::Cell*> &cells)
void dump_sync_effect(std::ostream &f, std::string indent, const RTLIL::SigSpec &trg, const RTLIL::Const &polarity, std::vector<const RTLIL::Cell*> &cells)
{
if (trg.size() == 0) {
f << stringf("%s" "initial begin\n", indent.c_str());
Expand All @@ -1918,9 +1964,25 @@ void dump_sync_print(std::ostream &f, std::string indent, const RTLIL::SigSpec &
for (auto cell : cells) {
f << stringf("%s" " if (", indent.c_str());
dump_sigspec(f, cell->getPort(ID::EN));
f << stringf(")\n");
f << stringf(") begin\n");

if (cell->type == ID($print)) {
dump_cell_expr_print(f, indent + " ", cell);
} else if (cell->type == ID($check)) {
std::string flavor = cell->getParam(ID::FLAVOR).decode_string();
if (flavor == "assert" || flavor == "assume") {
f << stringf("%s" " if (!", indent.c_str());
dump_sigspec(f, cell->getPort(ID::A));
f << stringf(")\n");
dump_cell_expr_print(f, indent + " ", cell);
} else {
f << stringf("%s" " /* message omitted */\n", indent.c_str());
}

dump_cell_expr_print(f, indent + " ", cell);
dump_cell_expr_check(f, indent + " ", cell);
}

f << stringf("%s" " end\n", indent.c_str());
}

f << stringf("%s" "end\n", indent.c_str());
Expand Down Expand Up @@ -2171,7 +2233,7 @@ void dump_process(std::ostream &f, std::string indent, RTLIL::Process *proc, boo

void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
{
std::map<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> sync_print_cells;
std::map<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> sync_effect_cells;

reg_wires.clear();
reset_auto_counter(module);
Expand Down Expand Up @@ -2203,8 +2265,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
std::set<std::pair<RTLIL::Wire*,int>> reg_bits;
for (auto cell : module->cells())
{
if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool()) {
sync_print_cells[make_pair(cell->getPort(ID::TRG), cell->getParam(ID::TRG_POLARITY))].push_back(cell);
if (cell->type.in(ID($print), ID($check)) && cell->getParam(ID::TRG_ENABLE).as_bool()) {
sync_effect_cells[make_pair(cell->getPort(ID::TRG), cell->getParam(ID::TRG_POLARITY))].push_back(cell);
continue;
}

Expand Down Expand Up @@ -2263,8 +2325,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
for (auto cell : module->cells())
dump_cell(f, indent + " ", cell);

for (auto &it : sync_print_cells)
dump_sync_print(f, indent + " ", it.first.first, it.first.second, it.second);
for (auto &it : sync_effect_cells)
dump_sync_effect(f, indent + " ", it.first.first, it.first.second, it.second);

for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
dump_process(f, indent + " ", it->second);
Expand Down
6 changes: 3 additions & 3 deletions docs/source/CHAPTER_CellLib.rst
View file
Original file line number Diff line number Diff line change
Expand Up @@ -621,7 +621,7 @@ Add information about ``$specify2``, ``$specify3``, and ``$specrule`` cells.
Formal verification cells
~~~~~~~~~~~~~~~~~~~~~~~~~

Add information about ``$assert``, ``$assume``, ``$live``, ``$fair``,
Add information about ``$check``, ``$assert``, ``$assume``, ``$live``, ``$fair``,
``$cover``, ``$equiv``, ``$initstate``, ``$anyconst``, ``$anyseq``,
``$anyinit``, ``$allconst``, ``$allseq`` cells.

Expand Down Expand Up @@ -654,8 +654,8 @@ If ``\TRG_ENABLE`` is true, the following parameters also apply:
negative-edge triggered.

``\PRIORITY``
When multiple ``$print`` cells fire on the same trigger, they execute in
descending priority order.
When multiple ``$print`` or ``$$check`` cells fire on the same trigger, they\
execute in descending priority order.

Ports:

Expand Down
132 changes: 97 additions & 35 deletions frontends/ast/genrtlil.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -316,10 +316,10 @@ struct AST_INTERNAL::ProcessGenerator
// Buffer for generating the init action
RTLIL::SigSpec init_lvalue, init_rvalue;

// The most recently assigned $print cell \PRIORITY.
int last_print_priority;
// The most recently assigned $print or $check cell \PRIORITY.
int last_effect_priority;

ProcessGenerator(AstNode *always, RTLIL::SigSpec initSyncSignalsArg = RTLIL::SigSpec()) : always(always), initSyncSignals(initSyncSignalsArg), last_print_priority(0)
ProcessGenerator(AstNode *always, RTLIL::SigSpec initSyncSignalsArg = RTLIL::SigSpec()) : always(always), initSyncSignals(initSyncSignalsArg), last_effect_priority(0)
{
// rewrite lookahead references
LookaheadRewriter la_rewriter(always);
Expand Down Expand Up @@ -703,8 +703,10 @@ struct AST_INTERNAL::ProcessGenerator
std::stringstream sstr;
sstr << ast->str << "$" << ast->filename << ":" << ast->location.first_line << "$" << (autoidx++);

RTLIL::Cell *cell = current_module->addCell(sstr.str(), ID($print));
set_src_attr(cell, ast);
Wire *en = current_module->addWire(sstr.str() + "_EN", 1);
set_src_attr(en, ast);
proc->root_case.actions.push_back(SigSig(en, false));
current_case->actions.push_back(SigSig(en, true));

RTLIL::SigSpec triggers;
RTLIL::Const polarity;
Expand All @@ -717,18 +719,15 @@ struct AST_INTERNAL::ProcessGenerator
polarity.bits.push_back(RTLIL::S0);
}
}
cell->parameters[ID::TRG_WIDTH] = triggers.size();
cell->parameters[ID::TRG_ENABLE] = (always->type == AST_INITIAL) || !triggers.empty();
cell->parameters[ID::TRG_POLARITY] = polarity;
cell->parameters[ID::PRIORITY] = --last_print_priority;
cell->setPort(ID::TRG, triggers);

Wire *wire = current_module->addWire(sstr.str() + "_EN", 1);
set_src_attr(wire, ast);
cell->setPort(ID::EN, wire);

proc->root_case.actions.push_back(SigSig(wire, false));
current_case->actions.push_back(SigSig(wire, true));
RTLIL::Cell *cell = current_module->addCell(sstr.str(), ID($print));
set_src_attr(cell, ast);
cell->setParam(ID::TRG_WIDTH, triggers.size());
cell->setParam(ID::TRG_ENABLE, (always->type == AST_INITIAL) || !triggers.empty());
cell->setParam(ID::TRG_POLARITY, polarity);
cell->setParam(ID::PRIORITY, --last_effect_priority);
cell->setPort(ID::TRG, triggers);
cell->setPort(ID::EN, en);

int default_base = 10;
if (ast->str.back() == 'b')
Expand Down Expand Up @@ -776,6 +775,67 @@ struct AST_INTERNAL::ProcessGenerator
}
break;

// generate $check cells
case AST_ASSERT:
case AST_ASSUME:
case AST_LIVE:
case AST_FAIR:
case AST_COVER:
{
std::string flavor, desc;
if (ast->type == AST_ASSERT) { flavor = "assert"; desc = "assert ()"; }
if (ast->type == AST_ASSUME) { flavor = "assume"; desc = "assume ()"; }
if (ast->type == AST_LIVE) { flavor = "live"; desc = "assert (eventually)"; }
if (ast->type == AST_FAIR) { flavor = "fair"; desc = "assume (eventually)"; }
if (ast->type == AST_COVER) { flavor = "cover"; desc = "cover ()"; }

std::stringstream sstr;
sstr << "$" << flavor << ast->str << "$" << ast->filename << ":" << ast->location.first_line << "$" << (autoidx++);

RTLIL::SigSpec check = ast->children[0]->genWidthRTLIL(-1, false, &subst_rvalue_map.stdmap());
if (GetSize(check) != 1)
check = current_module->ReduceBool(NEW_ID, check);

Wire *en = current_module->addWire(sstr.str() + "_EN", 1);
set_src_attr(en, ast);
proc->root_case.actions.push_back(SigSig(en, false));
current_case->actions.push_back(SigSig(en, true));

RTLIL::SigSpec triggers;
RTLIL::Const polarity;
for (auto sync : proc->syncs) {
if (sync->type == RTLIL::STp) {
triggers.append(sync->signal);
polarity.bits.push_back(RTLIL::S1);
} else if (sync->type == RTLIL::STn) {
triggers.append(sync->signal);
polarity.bits.push_back(RTLIL::S0);
}
}

RTLIL::IdString cellname = ast->str.empty() ? sstr.str() : ast->str;
RTLIL::Cell *cell = current_module->addCell(cellname, ID($check));
set_src_attr(cell, ast);
for (auto &attr : ast->attributes) {
if (attr.second->type != AST_CONSTANT)
log_file_error(ast->filename, ast->location.first_line, "Attribute `%s' with non-constant value!\n", attr.first.c_str());
cell->attributes[attr.first] = attr.second->asAttrConst();
}
cell->setParam(ID::FLAVOR, flavor);
cell->setParam(ID::TRG_WIDTH, triggers.size());
cell->setParam(ID::TRG_ENABLE, (always->type == AST_INITIAL) || !triggers.empty());
cell->setParam(ID::TRG_POLARITY, polarity);
cell->setParam(ID::PRIORITY, --last_effect_priority);
cell->setPort(ID::TRG, triggers);
cell->setPort(ID::EN, en);
cell->setPort(ID::A, check);

Fmt fmt = {};
fmt.append_string(stringf("%s failed at %s:%d\n", desc.c_str(), RTLIL::encode_filename(ast->filename).c_str(), ast->location.first_line));
fmt.emit_rtlil(cell);
break;
}

case AST_NONE:
case AST_FOR:
break;
Expand Down Expand Up @@ -1945,48 +2005,50 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
}
break;

// generate $assert cells
// generate $check cells
case AST_ASSERT:
case AST_ASSUME:
case AST_LIVE:
case AST_FAIR:
case AST_COVER:
{
IdString celltype;
if (type == AST_ASSERT) celltype = ID($assert);
if (type == AST_ASSUME) celltype = ID($assume);
if (type == AST_LIVE) celltype = ID($live);
if (type == AST_FAIR) celltype = ID($fair);
if (type == AST_COVER) celltype = ID($cover);

log_assert(children.size() == 2);
std::string flavor, desc;
if (type == AST_ASSERT) { flavor = "assert"; desc = "assert property ()"; }
if (type == AST_ASSUME) { flavor = "assume"; desc = "assume property ()"; }
if (type == AST_LIVE) { flavor = "live"; desc = "assert property (eventually)"; }
if (type == AST_FAIR) { flavor = "fair"; desc = "assume property (eventually)"; }
if (type == AST_COVER) { flavor = "cover"; desc = "cover property ()"; }

RTLIL::SigSpec check = children[0]->genRTLIL();
if (GetSize(check) != 1)
check = current_module->ReduceBool(NEW_ID, check);

RTLIL::SigSpec en = children[1]->genRTLIL();
if (GetSize(en) != 1)
en = current_module->ReduceBool(NEW_ID, en);

IdString cellname;
if (str.empty())
cellname = stringf("%s$%s:%d$%d", celltype.c_str(), RTLIL::encode_filename(filename).c_str(), location.first_line, autoidx++);
cellname = stringf("$%s$%s:%d$%d", flavor.c_str(), RTLIL::encode_filename(filename).c_str(), location.first_line, autoidx++);
else
cellname = str;

check_unique_id(current_module, cellname, this, "procedural assertion");
RTLIL::Cell *cell = current_module->addCell(cellname, celltype);
set_src_attr(cell, this);

RTLIL::Cell *cell = current_module->addCell(cellname, ID($check));
set_src_attr(cell, this);
for (auto &attr : attributes) {
if (attr.second->type != AST_CONSTANT)
input_error("Attribute `%s' with non-constant value!\n", attr.first.c_str());
cell->attributes[attr.first] = attr.second->asAttrConst();
}

cell->setParam(ID(FLAVOR), flavor);
cell->parameters[ID::TRG_WIDTH] = 0;
cell->parameters[ID::TRG_ENABLE] = 0;
cell->parameters[ID::TRG_POLARITY] = 0;
cell->parameters[ID::PRIORITY] = 0;
cell->setPort(ID::TRG, RTLIL::SigSpec());
cell->setPort(ID::EN, RTLIL::S1);
cell->setPort(ID::A, check);
cell->setPort(ID::EN, en);

Fmt fmt = {};
fmt.append_string(stringf("%s failed at %s:%d\n", desc.c_str(), RTLIL::encode_filename(filename).c_str(), location.first_line));
fmt.emit_rtlil(cell);
}
break;

Expand Down
Loading

0 comments on commit 6860b15

Please sign in to comment.