mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-06 01:24:10 +00:00
Code Activity

Add new $check cell to represent assertions with a message.

Browse source
This commit is contained in:
Catherine 2024-01-11 09:39:28 +00:00 committed by Jannis Harder
parent e1a59ba80b
commit c7bf0e3b8f
12 changed files with 516 additions and 306 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

363
backends/cxxrtl/cxxrtl_backend.cc
View file

@ -218,7 +218,7 @@ bool is_internal_cell(RTLIL::IdString type)
bool is_effectful_cell(RTLIL::IdString type) bool is_effectful_cell(RTLIL::IdString type)
{ {
return type.isPublic() || type == ID($print); return type.in(ID($print), ID($check));
} }
bool is_cxxrtl_blackbox_cell(const RTLIL::Cell *cell) bool is_cxxrtl_blackbox_cell(const RTLIL::Cell *cell)
@ -282,7 +282,7 @@ struct FlowGraph {
CONNECT, CONNECT,
CELL_SYNC, CELL_SYNC,
CELL_EVAL, CELL_EVAL,
PRINT_SYNC, EFFECT_SYNC,
PROCESS_SYNC, PROCESS_SYNC,
PROCESS_CASE, PROCESS_CASE,
MEM_RDPORT, MEM_RDPORT,
@ -292,7 +292,7 @@ struct FlowGraph {
Type type; Type type;
RTLIL::SigSig connect = {}; RTLIL::SigSig connect = {};
const RTLIL::Cell *cell = nullptr; const RTLIL::Cell *cell = nullptr;
std::vector<const RTLIL::Cell*> print_sync_cells; std::vector<const RTLIL::Cell*> cells;
const RTLIL::Process *process = nullptr; const RTLIL::Process *process = nullptr;
const Mem *mem = nullptr; const Mem *mem = nullptr;
int portidx; int portidx;
@ -480,11 +480,11 @@ struct FlowGraph {
return node; return node;
} }
Node *add_print_sync_node(std::vector<const RTLIL::Cell*> cells) Node *add_effect_sync_node(std::vector<const RTLIL::Cell*> cells)
{ {
Node *node = new Node; Node *node = new Node;
node->type = Node::Type::PRINT_SYNC; node->type = Node::Type::EFFECT_SYNC;
node->print_sync_cells = cells; node->cells = cells;
nodes.push_back(node); nodes.push_back(node);
return node; return node;
} }
@ -1063,99 +1063,6 @@ struct CxxrtlWorker {
f << ".val()"; f << ".val()";
} }
void dump_print(const RTLIL::Cell *cell)
{
Fmt fmt = {};
fmt.parse_rtlil(cell);
f << indent << "if (";
dump_sigspec_rhs(cell->getPort(ID::EN));
f << " == value<1>{1u}) {\n";
inc_indent();
dict<std::string, RTLIL::SigSpec> fmt_args;
f << indent << "struct : public lazy_fmt {\n";
inc_indent();
f << indent << "std::string operator() () const override {\n";
inc_indent();
fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) {
if (sig.size() == 0)
f << "value<0>()";
else {
std::string arg_name = "arg" + std::to_string(fmt_args.size());
fmt_args[arg_name] = sig;
f << arg_name;
}
}, "performer");
dec_indent();
f << indent << "}\n";
f << indent << "struct performer *performer;\n";
for (auto arg : fmt_args)
f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n";
dec_indent();
f << indent << "} formatter;\n";
f << indent << "formatter.performer = performer;\n";
for (auto arg : fmt_args) {
f << indent << "formatter." << arg.first << " = ";
dump_sigspec_rhs(arg.second);
f << ";\n";
}
f << indent << "if (performer) {\n";
inc_indent();
f << indent << "static const metadata_map attributes = ";
dump_metadata_map(cell->attributes);
f << ";\n";
f << indent << "performer->on_print(formatter, attributes);\n";
dec_indent();
f << indent << "} else {\n";
inc_indent();
f << indent << print_output << " << formatter();\n";
dec_indent();
f << indent << "}\n";
dec_indent();
f << indent << "}\n";
}
void dump_sync_print(std::vector<const RTLIL::Cell*> &cells)
{
log_assert(!cells.empty());
const auto &trg = cells[0]->getPort(ID::TRG);
const auto &trg_polarity = cells[0]->getParam(ID::TRG_POLARITY);
f << indent << "if (";
for (int i = 0; i < trg.size(); i++) {
RTLIL::SigBit trg_bit = trg[i];
trg_bit = sigmaps[trg_bit.wire->module](trg_bit);
log_assert(trg_bit.wire);
if (i != 0)
f << " || ";
if (trg_polarity[i] == State::S1)
f << "posedge_";
else
f << "negedge_";
f << mangle(trg_bit);
}
f << ") {\n";
inc_indent();
std::sort(cells.begin(), cells.end(), [](const RTLIL::Cell *a, const RTLIL::Cell *b) {
return a->getParam(ID::PRIORITY).as_int() > b->getParam(ID::PRIORITY).as_int();
});
for (auto cell : cells) {
log_assert(cell->getParam(ID::TRG_ENABLE).as_bool());
log_assert(cell->getPort(ID::TRG) == trg);
log_assert(cell->getParam(ID::TRG_POLARITY) == trg_polarity);
std::vector<const RTLIL::Cell*> inlined_cells;
collect_cell_eval(cell, /*for_debug=*/false, inlined_cells);
dump_inlined_cells(inlined_cells);
dump_print(cell);
}
dec_indent();
f << indent << "}\n";
}
void dump_inlined_cells(const std::vector<const RTLIL::Cell*> &cells) void dump_inlined_cells(const std::vector<const RTLIL::Cell*> &cells)
{ {
if (cells.empty()) { if (cells.empty()) {
@ -1309,6 +1216,144 @@ struct CxxrtlWorker {
} }
} }
void dump_print(const RTLIL::Cell *cell)
{
Fmt fmt;
fmt.parse_rtlil(cell);
f << indent << "if (";
dump_sigspec_rhs(cell->getPort(ID::EN));
f << " == value<1>{1u}) {\n";
inc_indent();
dict<std::string, RTLIL::SigSpec> fmt_args;
f << indent << "struct : public lazy_fmt {\n";
inc_indent();
f << indent << "std::string operator() () const override {\n";
inc_indent();
fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) {
if (sig.size() == 0)
f << "value<0>()";
else {
std::string arg_name = "arg" + std::to_string(fmt_args.size());
fmt_args[arg_name] = sig;
f << arg_name;
}
}, "performer");
dec_indent();
f << indent << "}\n";
f << indent << "struct performer *performer;\n";
for (auto arg : fmt_args)
f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n";
dec_indent();
f << indent << "} formatter;\n";
f << indent << "formatter.performer = performer;\n";
for (auto arg : fmt_args) {
f << indent << "formatter." << arg.first << " = ";
dump_sigspec_rhs(arg.second);
f << ";\n";
}
f << indent << "if (performer) {\n";
inc_indent();
f << indent << "static const metadata_map attributes = ";
dump_metadata_map(cell->attributes);
f << ";\n";
f << indent << "performer->on_print(formatter, attributes);\n";
dec_indent();
f << indent << "} else {\n";
inc_indent();
f << indent << print_output << " << formatter();\n";
dec_indent();
f << indent << "}\n";
dec_indent();
f << indent << "}\n";
}
void dump_effect(const RTLIL::Cell *cell)
{
Fmt fmt;
fmt.parse_rtlil(cell);
f << indent << "if (";
dump_sigspec_rhs(cell->getPort(ID::EN));
f << ") {\n";
inc_indent();
dict<std::string, RTLIL::SigSpec> fmt_args;
f << indent << "struct : public lazy_fmt {\n";
inc_indent();
f << indent << "std::string operator() () const override {\n";
inc_indent();
fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) {
if (sig.size() == 0)
f << "value<0>()";
else {
std::string arg_name = "arg" + std::to_string(fmt_args.size());
fmt_args[arg_name] = sig;
f << arg_name;
}
}, "performer");
dec_indent();
f << indent << "}\n";
f << indent << "struct performer *performer;\n";
for (auto arg : fmt_args)
f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n";
dec_indent();
f << indent << "} formatter;\n";
f << indent << "formatter.performer = performer;\n";
for (auto arg : fmt_args) {
f << indent << "formatter." << arg.first << " = ";
dump_sigspec_rhs(arg.second);
f << ";\n";
}
if (cell->hasPort(ID::A)) {
f << indent << "bool condition = (bool)";
dump_sigspec_rhs(cell->getPort(ID::A));
f << ";\n";
}
f << indent << "if (performer) {\n";
inc_indent();
f << indent << "static const metadata_map attributes = ";
dump_metadata_map(cell->attributes);
f << ";\n";
if (cell->type == ID($print)) {
f << indent << "performer->on_print(formatter, attributes);\n";
} else if (cell->type == ID($check)) {
std::string flavor = cell->getParam(ID::FLAVOR).decode_string();
f << indent << "performer->on_check(";
if (flavor == "assert")
f << "flavor::ASSERT";
else if (flavor == "assume")
f << "flavor::ASSUME";
else if (flavor == "live")
f << "flavor::ASSERT_EVENTUALLY";
else if (flavor == "fair")
f << "flavor::ASSUME_EVENTUALLY";
else if (flavor == "cover")
f << "flavor::COVER";
else log_assert(false);
f << ", condition, formatter, attributes);\n";
} else log_assert(false);
dec_indent();
f << indent << "} else {\n";
inc_indent();
if (cell->type == ID($print)) {
f << indent << print_output << " << formatter();\n";
} else if (cell->type == ID($check)) {
std::string flavor = cell->getParam(ID::FLAVOR).decode_string();
if (flavor == "assert" || flavor == "assume") {
f << indent << "if (!condition) {\n";
inc_indent();
f << indent << "std::cerr << formatter();\n";
dec_indent();
f << indent << "}\n";
f << indent << "CXXRTL_ASSERT(condition && \"Check failed\");\n";
}
} else log_assert(false);
dec_indent();
f << indent << "}\n";
dec_indent();
f << indent << "}\n";
}
void dump_cell_eval(const RTLIL::Cell *cell, bool for_debug = false) void dump_cell_eval(const RTLIL::Cell *cell, bool for_debug = false)
{ {
std::vector<const RTLIL::Cell*> inlined_cells; std::vector<const RTLIL::Cell*> inlined_cells;
@ -1322,30 +1367,34 @@ struct CxxrtlWorker {
f << " = "; f << " = ";
dump_cell_expr(cell, for_debug); dump_cell_expr(cell, for_debug);
f << ";\n"; f << ";\n";
// $print cell // Effectful cells
} else if (cell->type == ID($print)) { } else if (is_effectful_cell(cell->type)) {
log_assert(!for_debug); log_assert(!for_debug);
// Sync $print cells are grouped into PRINT_SYNC nodes in the FlowGraph. // Sync effectful cells are grouped into EFFECT_SYNC nodes in the FlowGraph.
log_assert(!cell->getParam(ID::TRG_ENABLE).as_bool() || (cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0)); log_assert(!cell->getParam(ID::TRG_ENABLE).as_bool() || (cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0));
if (!cell->getParam(ID::TRG_ENABLE).as_bool()) { // async $print cell if (!cell->getParam(ID::TRG_ENABLE).as_bool()) { // async effectful cell
f << indent << "auto " << mangle(cell) << "_curr = "; f << indent << "auto " << mangle(cell) << "_next = ";
dump_sigspec_rhs(cell->getPort(ID::EN)); dump_sigspec_rhs(cell->getPort(ID::EN));
f << ".concat("; f << ".concat(";
dump_sigspec_rhs(cell->getPort(ID::ARGS)); if (cell->type == ID($print))
dump_sigspec_rhs(cell->getPort(ID::ARGS));
else if (cell->type == ID($check))
dump_sigspec_rhs(cell->getPort(ID::A));
else log_assert(false);
f << ").val();\n"; f << ").val();\n";
f << indent << "if (" << mangle(cell) << " != " << mangle(cell) << "_curr) {\n"; f << indent << "if (" << mangle(cell) << " != " << mangle(cell) << "_next) {\n";
inc_indent(); inc_indent();
dump_print(cell); dump_effect(cell);
f << indent << mangle(cell) << " = " << mangle(cell) << "_curr;\n"; f << indent << mangle(cell) << " = " << mangle(cell) << "_next;\n";
dec_indent(); dec_indent();
f << indent << "}\n"; f << indent << "}\n";
} else { // initial $print cell } else { // initial effectful cell
f << indent << "if (!" << mangle(cell) << ") {\n"; f << indent << "if (!" << mangle(cell) << ") {\n";
inc_indent(); inc_indent();
dump_print(cell); dump_effect(cell);
f << indent << mangle(cell) << " = value<1>{1u};\n"; f << indent << mangle(cell) << " = value<1>{1u};\n";
dec_indent(); dec_indent();
f << indent << "}\n"; f << indent << "}\n";
@ -1728,6 +1777,47 @@ struct CxxrtlWorker {
} }
} }
void dump_cell_effect_sync(std::vector<const RTLIL::Cell*> &cells)
{
log_assert(!cells.empty());
const auto &trg = cells[0]->getPort(ID::TRG);
const auto &trg_polarity = cells[0]->getParam(ID::TRG_POLARITY);
f << indent << "if (";
for (int i = 0; i < trg.size(); i++) {
RTLIL::SigBit trg_bit = trg[i];
trg_bit = sigmaps[trg_bit.wire->module](trg_bit);
log_assert(trg_bit.wire);
if (i != 0)
f << " || ";
if (trg_polarity[i] == State::S1)
f << "posedge_";
else
f << "negedge_";
f << mangle(trg_bit);
}
f << ") {\n";
inc_indent();
std::sort(cells.begin(), cells.end(), [](const RTLIL::Cell *a, const RTLIL::Cell *b) {
return a->getParam(ID::PRIORITY).as_int() > b->getParam(ID::PRIORITY).as_int();
});
for (auto cell : cells) {
log_assert(cell->getParam(ID::TRG_ENABLE).as_bool());
log_assert(cell->getPort(ID::TRG) == trg);
log_assert(cell->getParam(ID::TRG_POLARITY) == trg_polarity);
std::vector<const RTLIL::Cell*> inlined_cells;
collect_cell_eval(cell, /*for_debug=*/false, inlined_cells);
dump_inlined_cells(inlined_cells);
dump_effect(cell);
}
dec_indent();
f << indent << "}\n";
}
void dump_mem_rdport(const Mem *mem, int portidx, bool for_debug = false) void dump_mem_rdport(const Mem *mem, int portidx, bool for_debug = false)
{ {
auto &port = mem->rd_ports[portidx]; auto &port = mem->rd_ports[portidx];
@ -2047,11 +2137,10 @@ struct CxxrtlWorker {
} }
} }
for (auto cell : module->cells()) { for (auto cell : module->cells()) {
// Certain $print cells have additional state, which must be reset as well. // Async and initial effectful cells have additional state, which must be reset as well.
if (cell->type == ID($print) && !cell->getParam(ID::TRG_ENABLE).as_bool()) if (is_effectful_cell(cell->type))
f << indent << mangle(cell) << " = value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << ">();\n"; if (!cell->getParam(ID::TRG_ENABLE).as_bool() || cell->getParam(ID::TRG_WIDTH).as_int() == 0)
if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0) f << indent << mangle(cell) << " = {};\n";
f << indent << mangle(cell) << " = value<1>();\n";
if (is_internal_cell(cell->type)) if (is_internal_cell(cell->type))
continue; continue;
f << indent << mangle(cell); f << indent << mangle(cell);
@ -2099,8 +2188,8 @@ struct CxxrtlWorker {
case FlowGraph::Node::Type::CELL_EVAL: case FlowGraph::Node::Type::CELL_EVAL:
dump_cell_eval(node.cell); dump_cell_eval(node.cell);
break; break;
case FlowGraph::Node::Type::PRINT_SYNC: case FlowGraph::Node::Type::EFFECT_SYNC:
dump_sync_print(node.print_sync_cells); dump_cell_effect_sync(node.cells);
break; break;
case FlowGraph::Node::Type::PROCESS_CASE: case FlowGraph::Node::Type::PROCESS_CASE:
dump_process_case(node.process); dump_process_case(node.process);
@ -2481,11 +2570,15 @@ struct CxxrtlWorker {
f << "\n"; f << "\n";
bool has_cells = false; bool has_cells = false;
for (auto cell : module->cells()) { for (auto cell : module->cells()) {
// Certain $print cells have additional state, which requires storage. // Async and initial effectful cells have additional state, which requires storage.
if (cell->type == ID($print) && !cell->getParam(ID::TRG_ENABLE).as_bool()) if (is_effectful_cell(cell->type)) {
f << indent << "value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << "> " << mangle(cell) << ";\n"; if (cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0)
if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0) f << indent << "value<1> " << mangle(cell) << ";\n"; // async initial cell
f << indent << "value<1> " << mangle(cell) << ";\n"; if (!cell->getParam(ID::TRG_ENABLE).as_bool() && cell->type == ID($print))
f << indent << "value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << "> " << mangle(cell) << ";\n"; // {EN, ARGS}
if (!cell->getParam(ID::TRG_ENABLE).as_bool() && cell->type == ID($check))
f << indent << "value<2> " << mangle(cell) << ";\n"; // {EN, A}
}
if (is_internal_cell(cell->type)) if (is_internal_cell(cell->type))
continue; continue;
dump_attrs(cell); dump_attrs(cell);
@ -2803,8 +2896,8 @@ struct CxxrtlWorker {
cell->parameters[ID::CLK_POLARITY].as_bool() ? RTLIL::STp : RTLIL::STn); cell->parameters[ID::CLK_POLARITY].as_bool() ? RTLIL::STp : RTLIL::STn);
} }
// $print cells may be triggered on posedge/negedge events. // Effectful cells may be triggered on posedge/negedge events.
if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool()) { if (is_effectful_cell(cell->type) && cell->getParam(ID::TRG_ENABLE).as_bool()) {
for (size_t i = 0; i < (size_t)cell->getParam(ID::TRG_WIDTH).as_int(); i++) { for (size_t i = 0; i < (size_t)cell->getParam(ID::TRG_WIDTH).as_int(); i++) {
RTLIL::SigBit trg = cell->getPort(ID::TRG).extract(i, 1); RTLIL::SigBit trg = cell->getPort(ID::TRG).extract(i, 1);
if (is_valid_clock(trg)) if (is_valid_clock(trg))
@ -2945,10 +3038,12 @@ struct CxxrtlWorker {
// Discover nodes reachable from primary outputs (i.e. members) and collect reachable wire users. // Discover nodes reachable from primary outputs (i.e. members) and collect reachable wire users.
pool<FlowGraph::Node*, hash_ptr_ops> worklist; pool<FlowGraph::Node*, hash_ptr_ops> worklist;
for (auto node : flow.nodes) { for (auto node : flow.nodes) {
if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type)) if (node->type == FlowGraph::Node::Type::CELL_EVAL && !is_internal_cell(node->cell->type))
worklist.insert(node); // node has effects worklist.insert(node); // node evaluates a submodule
else if (node->type == FlowGraph::Node::Type::PRINT_SYNC) else if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type))
worklist.insert(node); // node is sync $print worklist.insert(node); // node has async effects
else if (node->type == FlowGraph::Node::Type::EFFECT_SYNC)
worklist.insert(node); // node has sync effects
else if (node->type == FlowGraph::Node::Type::MEM_WRPORTS) else if (node->type == FlowGraph::Node::Type::MEM_WRPORTS)
worklist.insert(node); // node is memory write worklist.insert(node); // node is memory write
else if (node->type == FlowGraph::Node::Type::PROCESS_SYNC && is_memwr_process(node->process)) else if (node->type == FlowGraph::Node::Type::PROCESS_SYNC && is_memwr_process(node->process))
@ -3005,21 +3100,21 @@ struct CxxrtlWorker {
} }
// Emit reachable nodes in eval(). // Emit reachable nodes in eval().
// Accumulate sync $print cells per trigger condition. // Accumulate sync effectful cells per trigger condition.
dict<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> sync_print_cells; dict<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> effect_sync_cells;
for (auto node : node_order) for (auto node : node_order)
if (live_nodes[node]) { if (live_nodes[node]) {
if (node->type == FlowGraph::Node::Type::CELL_EVAL && if (node->type == FlowGraph::Node::Type::CELL_EVAL &&
node->cell->type == ID($print) && is_effectful_cell(node->cell->type) &&
node->cell->getParam(ID::TRG_ENABLE).as_bool() && node->cell->getParam(ID::TRG_ENABLE).as_bool() &&
node->cell->getParam(ID::TRG_WIDTH).as_int() != 0) node->cell->getParam(ID::TRG_WIDTH).as_int() != 0)
sync_print_cells[make_pair(node->cell->getPort(ID::TRG), node->cell->getParam(ID::TRG_POLARITY))].push_back(node->cell); effect_sync_cells[make_pair(node->cell->getPort(ID::TRG), node->cell->getParam(ID::TRG_POLARITY))].push_back(node->cell);
else else
schedule[module].push_back(*node); schedule[module].push_back(*node);
} }
for (auto &it : sync_print_cells) { for (auto &it : effect_sync_cells) {
auto node = flow.add_print_sync_node(it.second); auto node = flow.add_effect_sync_node(it.second);
schedule[module].push_back(*node); schedule[module].push_back(*node);
} }

27
backends/cxxrtl/runtime/cxxrtl/cxxrtl.h
View file

@ -952,7 +952,23 @@ struct lazy_fmt {
virtual std::string operator() () const = 0; virtual std::string operator() () const = 0;
}; };
// An object that can be passed to a `eval()` method in order to act on side effects. // 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. The default behavior implemented
// below is the same as the behavior of `eval(nullptr)`, except that `-print-output` option of `write_cxxrtl` is not
// taken into account.
struct performer { struct performer {
// Called by generated formatting code to evaluate a Verilog `$time` expression. // Called by generated formatting code to evaluate a Verilog `$time` expression.
virtual int64_t vlog_time() const { return 0; } virtual int64_t vlog_time() const { return 0; }
@ -964,6 +980,15 @@ struct performer {
virtual void on_print(const lazy_fmt &formatter, const metadata_map &attributes) { virtual void on_print(const lazy_fmt &formatter, const metadata_map &attributes) {
std::cout << formatter(); 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();
CXXRTL_ASSERT(condition && "Check failed");
}
}
}; };
// An object that can be passed to a `commit()` method in order to produce a replay log of every state change in // An object that can be passed to a `commit()` method in order to produce a replay log of every state change in

88
backends/verilog/verilog_backend.cc
View file

@ -1008,7 +1008,7 @@ void dump_cell_expr_binop(std::ostream &f, std::string indent, RTLIL::Cell *cell
void dump_cell_expr_print(std::ostream &f, std::string indent, const RTLIL::Cell *cell) void dump_cell_expr_print(std::ostream &f, std::string indent, const RTLIL::Cell *cell)
{ {
Fmt fmt = {}; Fmt fmt;
fmt.parse_rtlil(cell); fmt.parse_rtlil(cell);
std::vector<VerilogFmtArg> args = fmt.emit_verilog(); std::vector<VerilogFmtArg> args = fmt.emit_verilog();
@ -1041,6 +1041,23 @@ void dump_cell_expr_print(std::ostream &f, std::string indent, const RTLIL::Cell
f << stringf(");\n"); 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) bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
{ {
if (cell->type == ID($_NOT_)) { if (cell->type == ID($_NOT_)) {
@ -1814,6 +1831,39 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
return true; 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") {
Fmt fmt;
fmt.parse_rtlil(cell);
if (!fmt.parts.empty()) {
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 // FIXME: $fsm
return false; return false;
@ -1903,7 +1953,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) { if (trg.size() == 0) {
f << stringf("%s" "initial begin\n", indent.c_str()); f << stringf("%s" "initial begin\n", indent.c_str());
@ -1927,9 +1977,29 @@ void dump_sync_print(std::ostream &f, std::string indent, const RTLIL::SigSpec &
for (auto cell : cells) { for (auto cell : cells) {
f << stringf("%s" " if (", indent.c_str()); f << stringf("%s" " if (", indent.c_str());
dump_sigspec(f, cell->getPort(ID::EN)); dump_sigspec(f, cell->getPort(ID::EN));
f << stringf(")\n"); f << stringf(") begin\n");
dump_cell_expr_print(f, indent + " ", cell); 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") {
Fmt fmt;
fmt.parse_rtlil(cell);
if (!fmt.parts.empty()) {
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());
} }
f << stringf("%s" "end\n", indent.c_str()); f << stringf("%s" "end\n", indent.c_str());
@ -2182,7 +2252,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) 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(); reg_wires.clear();
reset_auto_counter(module); reset_auto_counter(module);
@ -2214,8 +2284,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
std::set<std::pair<RTLIL::Wire*,int>> reg_bits; std::set<std::pair<RTLIL::Wire*,int>> reg_bits;
for (auto cell : module->cells()) for (auto cell : module->cells())
{ {
if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool()) { if (cell->type.in(ID($print), ID($check)) && cell->getParam(ID::TRG_ENABLE).as_bool()) {
sync_print_cells[make_pair(cell->getPort(ID::TRG), cell->getParam(ID::TRG_POLARITY))].push_back(cell); sync_effect_cells[make_pair(cell->getPort(ID::TRG), cell->getParam(ID::TRG_POLARITY))].push_back(cell);
continue; continue;
} }
@ -2274,8 +2344,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
for (auto cell : module->cells()) for (auto cell : module->cells())
dump_cell(f, indent + " ", cell); dump_cell(f, indent + " ", cell);
for (auto &it : sync_print_cells) for (auto &it : sync_effect_cells)
dump_sync_print(f, indent + " ", it.first.first, it.first.second, it.second); dump_sync_effect(f, indent + " ", it.first.first, it.first.second, it.second);
for (auto it = module->processes.begin(); it != module->processes.end(); ++it) for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
dump_process(f, indent + " ", it->second); dump_process(f, indent + " ", it->second);

6
docs/source/CHAPTER_CellLib.rst
View file

@ -621,7 +621,7 @@ Add information about ``$specify2``, ``$specify3``, and ``$specrule`` cells.
Formal verification cells Formal verification cells
~~~~~~~~~~~~~~~~~~~~~~~~~ ~~~~~~~~~~~~~~~~~~~~~~~~~
Add information about ``$assert``, ``$assume``, ``$live``, ``$fair``, Add information about ``$check``, ``$assert``, ``$assume``, ``$live``, ``$fair``,
``$cover``, ``$equiv``, ``$initstate``, ``$anyconst``, ``$anyseq``, ``$cover``, ``$equiv``, ``$initstate``, ``$anyconst``, ``$anyseq``,
``$anyinit``, ``$allconst``, ``$allseq`` cells. ``$anyinit``, ``$allconst``, ``$allseq`` cells.
@ -654,8 +654,8 @@ If ``\TRG_ENABLE`` is true, the following parameters also apply:
negative-edge triggered. negative-edge triggered.
``\PRIORITY`` ``\PRIORITY``
When multiple ``$print`` cells fire on the same trigger, they execute in When multiple ``$print`` or ``$$check`` cells fire on the same trigger, they\
descending priority order. execute in descending priority order.
Ports: Ports:

189
frontends/ast/genrtlil.cc
View file

@ -163,6 +163,28 @@ static RTLIL::SigSpec mux2rtlil(AstNode *that, const RTLIL::SigSpec &cond, const
return wire; return wire;
} }
static void check_unique_id(RTLIL::Module *module, RTLIL::IdString id,
const AstNode *node, const char *to_add_kind)
{
auto already_exists = [&](const RTLIL::AttrObject *existing, const char *existing_kind) {
std::string src = existing->get_string_attribute(ID::src);
std::string location_str = "earlier";
if (!src.empty())
location_str = "at " + src;
node->input_error("Cannot add %s `%s' because a %s with the same name was already created %s!\n",
to_add_kind, id.c_str(), existing_kind, location_str.c_str());
};
if (const RTLIL::Wire *wire = module->wire(id))
already_exists(wire, "signal");
if (const RTLIL::Cell *cell = module->cell(id))
already_exists(cell, "cell");
if (module->processes.count(id))
already_exists(module->processes.at(id), "process");
if (module->memories.count(id))
already_exists(module->memories.at(id), "memory");
}
// helper class for rewriting simple lookahead references in AST always blocks // helper class for rewriting simple lookahead references in AST always blocks
struct AST_INTERNAL::LookaheadRewriter struct AST_INTERNAL::LookaheadRewriter
{ {
@ -316,10 +338,10 @@ struct AST_INTERNAL::ProcessGenerator
// Buffer for generating the init action // Buffer for generating the init action
RTLIL::SigSpec init_lvalue, init_rvalue; RTLIL::SigSpec init_lvalue, init_rvalue;
// The most recently assigned $print cell \PRIORITY. // The most recently assigned $print or $check cell \PRIORITY.
int last_print_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 // rewrite lookahead references
LookaheadRewriter la_rewriter(always); LookaheadRewriter la_rewriter(always);
@ -703,8 +725,10 @@ struct AST_INTERNAL::ProcessGenerator
std::stringstream sstr; std::stringstream sstr;
sstr << ast->str << "$" << ast->filename << ":" << ast->location.first_line << "$" << (autoidx++); sstr << ast->str << "$" << ast->filename << ":" << ast->location.first_line << "$" << (autoidx++);
RTLIL::Cell *cell = current_module->addCell(sstr.str(), ID($print)); Wire *en = current_module->addWire(sstr.str() + "_EN", 1);
set_src_attr(cell, ast); 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::SigSpec triggers;
RTLIL::Const polarity; RTLIL::Const polarity;
@ -717,18 +741,15 @@ struct AST_INTERNAL::ProcessGenerator
polarity.bits.push_back(RTLIL::S0); polarity.bits.push_back(RTLIL::S0);
} }
} }
cell->parameters[ID::TRG_WIDTH] = triggers.size();
cell->parameters[ID::TRG_ENABLE] = (always->type == AST_INITIAL) || !triggers.empty(); RTLIL::Cell *cell = current_module->addCell(sstr.str(), ID($print));
cell->parameters[ID::TRG_POLARITY] = polarity; set_src_attr(cell, ast);
cell->parameters[ID::PRIORITY] = --last_print_priority; 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::TRG, triggers);
cell->setPort(ID::EN, en);
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));
int default_base = 10; int default_base = 10;
if (ast->str.back() == 'b') if (ast->str.back() == 'b')
@ -766,7 +787,7 @@ struct AST_INTERNAL::ProcessGenerator
args.push_back(arg); args.push_back(arg);
} }
Fmt fmt = {}; Fmt fmt;
fmt.parse_verilog(args, /*sformat_like=*/false, default_base, /*task_name=*/ast->str, current_module->name); fmt.parse_verilog(args, /*sformat_like=*/false, default_base, /*task_name=*/ast->str, current_module->name);
if (ast->str.substr(0, 8) == "$display") if (ast->str.substr(0, 8) == "$display")
fmt.append_string("\n"); fmt.append_string("\n");
@ -776,6 +797,70 @@ struct AST_INTERNAL::ProcessGenerator
} }
break; 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 ()"; }
IdString cellname;
if (ast->str.empty())
cellname = stringf("$%s$%s:%d$%d", flavor.c_str(), RTLIL::encode_filename(ast->filename).c_str(), ast->location.first_line, autoidx++);
else
cellname = ast->str;
check_unique_id(current_module, cellname, ast, "procedural assertion");
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(cellname.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::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);
// No message is emitted to ensure Verilog code roundtrips correctly.
Fmt fmt;
fmt.emit_rtlil(cell);
break;
}
case AST_NONE: case AST_NONE:
case AST_FOR: case AST_FOR:
break; break;
@ -1242,28 +1327,6 @@ void AstNode::detectSignWidth(int &width_hint, bool &sign_hint, bool *found_real
width_hint, kWidthLimit); width_hint, kWidthLimit);
} }
static void check_unique_id(RTLIL::Module *module, RTLIL::IdString id,
const AstNode *node, const char *to_add_kind)
{
auto already_exists = [&](const RTLIL::AttrObject *existing, const char *existing_kind) {
std::string src = existing->get_string_attribute(ID::src);
std::string location_str = "earlier";
if (!src.empty())
location_str = "at " + src;
node->input_error("Cannot add %s `%s' because a %s with the same name was already created %s!\n",
to_add_kind, id.c_str(), existing_kind, location_str.c_str());
};
if (const RTLIL::Wire *wire = module->wire(id))
already_exists(wire, "signal");
if (const RTLIL::Cell *cell = module->cell(id))
already_exists(cell, "cell");
if (module->processes.count(id))
already_exists(module->processes.at(id), "process");
if (module->memories.count(id))
already_exists(module->memories.at(id), "memory");
}
// create RTLIL from an AST node // create RTLIL from an AST node
// all generated cells, wires and processes are added to the module pointed to by 'current_module' // all generated cells, wires and processes are added to the module pointed to by 'current_module'
// when the AST node is an expression (AST_ADD, AST_BIT_XOR, etc.), the result signal is returned. // when the AST node is an expression (AST_ADD, AST_BIT_XOR, etc.), the result signal is returned.
@ -1945,48 +2008,50 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
} }
break; break;
// generate $assert cells // generate $check cells
case AST_ASSERT: case AST_ASSERT:
case AST_ASSUME: case AST_ASSUME:
case AST_LIVE: case AST_LIVE:
case AST_FAIR: case AST_FAIR:
case AST_COVER: case AST_COVER:
{ {
IdString celltype; std::string flavor, desc;
if (type == AST_ASSERT) celltype = ID($assert); if (type == AST_ASSERT) { flavor = "assert"; desc = "assert property ()"; }
if (type == AST_ASSUME) celltype = ID($assume); if (type == AST_ASSUME) { flavor = "assume"; desc = "assume property ()"; }
if (type == AST_LIVE) celltype = ID($live); if (type == AST_LIVE) { flavor = "live"; desc = "assert property (eventually)"; }
if (type == AST_FAIR) celltype = ID($fair); if (type == AST_FAIR) { flavor = "fair"; desc = "assume property (eventually)"; }
if (type == AST_COVER) celltype = ID($cover); if (type == AST_COVER) { flavor = "cover"; desc = "cover property ()"; }
log_assert(children.size() == 2); IdString cellname;
if (str.empty())
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::SigSpec check = children[0]->genRTLIL(); RTLIL::SigSpec check = children[0]->genRTLIL();
if (GetSize(check) != 1) if (GetSize(check) != 1)
check = current_module->ReduceBool(NEW_ID, check); check = current_module->ReduceBool(NEW_ID, check);
RTLIL::SigSpec en = children[1]->genRTLIL(); RTLIL::Cell *cell = current_module->addCell(cellname, ID($check));
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++);
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); set_src_attr(cell, this);
for (auto &attr : attributes) { for (auto &attr : attributes) {
if (attr.second->type != AST_CONSTANT) if (attr.second->type != AST_CONSTANT)
input_error("Attribute `%s' with non-constant value!\n", attr.first.c_str()); input_error("Attribute `%s' with non-constant value!\n", attr.first.c_str());
cell->attributes[attr.first] = attr.second->asAttrConst(); 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::A, check);
cell->setPort(ID::EN, en);
// No message is emitted to ensure Verilog code roundtrips correctly.
Fmt fmt;
fmt.emit_rtlil(cell);
} }
break; break;

95
frontends/ast/simplify.cc
View file

@ -178,7 +178,7 @@ Fmt AstNode::processFormat(int stage, bool sformat_like, int default_base, size_
args.push_back(arg); args.push_back(arg);
} }
Fmt fmt = {}; Fmt fmt;
fmt.parse_verilog(args, sformat_like, default_base, /*task_name=*/str, current_module->name); fmt.parse_verilog(args, sformat_like, default_base, /*task_name=*/str, current_module->name);
return fmt; return fmt;
} }
@ -784,7 +784,7 @@ AstNode *AstNode::clone_at_zero()
pointee->type != AST_MEMORY) pointee->type != AST_MEMORY)
break; break;
YS_FALLTHROUGH; YS_FALLTHROUGH
case AST_MEMRD: case AST_MEMRD:
detectSignWidth(width_hint, sign_hint); detectSignWidth(width_hint, sign_hint);
return mkconst_int(0, sign_hint, width_hint); return mkconst_int(0, sign_hint, width_hint);
@ -3039,97 +3039,6 @@ bool AstNode::simplify(bool const_fold, int stage, int width_hint, bool sign_hin
} }
skip_dynamic_range_lvalue_expansion:; skip_dynamic_range_lvalue_expansion:;
if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_LIVE || type == AST_FAIR || type == AST_COVER) && current_block != NULL)
{
std::stringstream sstr;
sstr << "$formal$" << RTLIL::encode_filename(filename) << ":" << location.first_line << "$" << (autoidx++);
std::string id_check = sstr.str() + "_CHECK", id_en = sstr.str() + "_EN";
AstNode *wire_check = new AstNode(AST_WIRE);
wire_check->str = id_check;
wire_check->was_checked = true;
current_ast_mod->children.push_back(wire_check);
current_scope[wire_check->str] = wire_check;
while (wire_check->simplify(true, 1, -1, false)) { }
AstNode *wire_en = new AstNode(AST_WIRE);
wire_en->str = id_en;
wire_en->was_checked = true;
current_ast_mod->children.push_back(wire_en);
if (current_always_clocked) {
current_ast_mod->children.push_back(new AstNode(AST_INITIAL, new AstNode(AST_BLOCK, new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), AstNode::mkconst_int(0, false, 1)))));
current_ast_mod->children.back()->children[0]->children[0]->children[0]->str = id_en;
current_ast_mod->children.back()->children[0]->children[0]->children[0]->was_checked = true;
}
current_scope[wire_en->str] = wire_en;
while (wire_en->simplify(true, 1, -1, false)) { }
AstNode *check_defval;
if (type == AST_LIVE || type == AST_FAIR) {
check_defval = new AstNode(AST_REDUCE_BOOL, children[0]->clone());
} else {
std::vector<RTLIL::State> x_bit;
x_bit.push_back(RTLIL::State::Sx);
check_defval = mkconst_bits(x_bit, false);
}
AstNode *assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), check_defval);
assign_check->children[0]->str = id_check;
assign_check->children[0]->was_checked = true;
AstNode *assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(0, false, 1));
assign_en->children[0]->str = id_en;
assign_en->children[0]->was_checked = true;
AstNode *default_signals = new AstNode(AST_BLOCK);
default_signals->children.push_back(assign_check);
default_signals->children.push_back(assign_en);
current_top_block->children.insert(current_top_block->children.begin(), default_signals);
if (type == AST_LIVE || type == AST_FAIR) {
assign_check = nullptr;
} else {
assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_REDUCE_BOOL, children[0]->clone()));
assign_check->children[0]->str = id_check;
assign_check->children[0]->was_checked = true;
assign_check->fixup_hierarchy_flags();
}
if (current_always == nullptr || current_always->type != AST_INITIAL) {
assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(1, false, 1));
} else {
assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_FCALL));
assign_en->children[1]->str = "\\$initstate";
}
assign_en->children[0]->str = id_en;
assign_en->children[0]->was_checked = true;
assign_en->fixup_hierarchy_flags();
newNode = new AstNode(AST_BLOCK);
if (assign_check != nullptr)
newNode->children.push_back(assign_check);
newNode->children.push_back(assign_en);
AstNode *assertnode = new AstNode(type);
assertnode->location = location;
assertnode->str = str;
assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
assertnode->children[0]->str = id_check;
assertnode->children[1]->str = id_en;
assertnode->attributes.swap(attributes);
current_ast_mod->children.push_back(assertnode);
goto apply_newNode;
}
if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_LIVE || type == AST_FAIR || type == AST_COVER) && children.size() == 1)
{
children.push_back(mkconst_int(1, false, 1));
fixup_hierarchy_flags();
did_something = true;
}
// found right-hand side identifier for memory -> replace with memory read port // found right-hand side identifier for memory -> replace with memory read port
if (stage > 1 && type == AST_IDENTIFIER && id2ast != NULL && id2ast->type == AST_MEMORY && !in_lvalue && if (stage > 1 && type == AST_IDENTIFIER && id2ast != NULL && id2ast->type == AST_MEMORY && !in_lvalue &&
children.size() == 1 && children[0]->type == AST_RANGE && children[0]->children.size() == 1) { children.size() == 1 && children[0]->type == AST_RANGE && children[0]->children.size() == 1) {

1
kernel/celltypes.h
View file

@ -102,6 +102,7 @@ struct CellTypes
setup_type(ID($specify3), {ID::EN, ID::SRC, ID::DST, ID::DAT}, pool<RTLIL::IdString>(), true); setup_type(ID($specify3), {ID::EN, ID::SRC, ID::DST, ID::DAT}, pool<RTLIL::IdString>(), true);
setup_type(ID($specrule), {ID::EN_SRC, ID::EN_DST, ID::SRC, ID::DST}, pool<RTLIL::IdString>(), true); setup_type(ID($specrule), {ID::EN_SRC, ID::EN_DST, ID::SRC, ID::DST}, pool<RTLIL::IdString>(), true);
setup_type(ID($print), {ID::EN, ID::ARGS, ID::TRG}, pool<RTLIL::IdString>()); setup_type(ID($print), {ID::EN, ID::ARGS, ID::TRG}, pool<RTLIL::IdString>());
setup_type(ID($check), {ID::A, ID::EN, ID::ARGS, ID::TRG}, pool<RTLIL::IdString>());
setup_type(ID($set_tag), {ID::A, ID::SET, ID::CLR}, {ID::Y}); setup_type(ID($set_tag), {ID::A, ID::SET, ID::CLR}, {ID::Y});
setup_type(ID($get_tag), {ID::A}, {ID::Y}); setup_type(ID($get_tag), {ID::A}, {ID::Y});
setup_type(ID($overwrite_tag), {ID::A, ID::SET, ID::CLR}, pool<RTLIL::IdString>()); setup_type(ID($overwrite_tag), {ID::A, ID::SET, ID::CLR}, pool<RTLIL::IdString>());

1
kernel/constids.inc
View file

@ -88,6 +88,7 @@ X(equiv_merged)
X(equiv_region) X(equiv_region)
X(extract_order) X(extract_order)
X(F) X(F)
X(FLAVOR)
X(FORMAT) X(FORMAT)
X(force_downto) X(force_downto)
X(force_upto) X(force_upto)

22
kernel/rtlil.cc
View file

@ -1068,6 +1068,12 @@ namespace {
error(__LINE__); error(__LINE__);
} }
std::string param_string(const RTLIL::IdString &name)
{
param(name);
return cell->parameters.at(name).decode_string();
}
void port(const RTLIL::IdString& name, int width) void port(const RTLIL::IdString& name, int width)
{ {
auto it = cell->connections_.find(name); auto it = cell->connections_.find(name);
@ -1747,6 +1753,22 @@ namespace {
return; return;
} }
if (cell->type == ID($check)) {
std::string flavor = param_string(ID(FLAVOR));
if (!(flavor == "assert" || flavor == "assume" || flavor == "live" || flavor == "fair" || flavor == "cover"))
error(__LINE__);
param(ID(FORMAT));
param_bool(ID::TRG_ENABLE);
param(ID::TRG_POLARITY);
param(ID::PRIORITY);
port(ID::A, 1);
port(ID::EN, 1);
port(ID::TRG, param(ID::TRG_WIDTH));
port(ID::ARGS, param(ID::ARGS_WIDTH));
check_expected();
return;
}
if (cell->type == ID($_BUF_)) { port(ID::A,1); port(ID::Y,1); check_expected(); return; } if (cell->type == ID($_BUF_)) { port(ID::A,1); port(ID::Y,1); check_expected(); return; }
if (cell->type == ID($_NOT_)) { port(ID::A,1); port(ID::Y,1); check_expected(); return; } if (cell->type == ID($_NOT_)) { port(ID::A,1); port(ID::Y,1); check_expected(); return; }
if (cell->type == ID($_AND_)) { port(ID::A,1); port(ID::B,1); port(ID::Y,1); check_expected(); return; } if (cell->type == ID($_AND_)) { port(ID::A,1); port(ID::B,1); port(ID::Y,1); check_expected(); return; }

2
passes/hierarchy/hierarchy.cc
View file

@ -671,7 +671,7 @@ bool set_keep_assert(std::map<RTLIL::Module*, bool> &cache, RTLIL::Module *mod)
if (cache.count(mod) == 0) if (cache.count(mod) == 0)
for (auto c : mod->cells()) { for (auto c : mod->cells()) {
RTLIL::Module *m = mod->design->module(c->type); RTLIL::Module *m = mod->design->module(c->type);
if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover))) if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in(ID($check), ID($assert), ID($assume), ID($live), ID($fair), ID($cover)))
return cache[mod] = true; return cache[mod] = true;
} }
return cache[mod]; return cache[mod];

2
passes/opt/opt_clean.cc
View file

@ -82,7 +82,7 @@ struct keep_cache_t
if (!ignore_specify && cell->type.in(ID($specify2), ID($specify3), ID($specrule))) if (!ignore_specify && cell->type.in(ID($specify2), ID($specify3), ID($specrule)))
return true; return true;
if (cell->type == ID($print)) if (cell->type == ID($print) || cell->type == ID($check))
return true; return true;
if (cell->has_keep_attr()) if (cell->has_keep_attr())

26
techlibs/common/simlib.v
View file

@ -1803,11 +1803,12 @@ endmodule
module \$print (EN, TRG, ARGS); module \$print (EN, TRG, ARGS);
parameter PRIORITY = 0;
parameter FORMAT = ""; parameter FORMAT = "";
parameter ARGS_WIDTH = 0; parameter ARGS_WIDTH = 0;
parameter PRIORITY = 0;
parameter TRG_ENABLE = 1;
parameter TRG_ENABLE = 1;
parameter TRG_WIDTH = 0; parameter TRG_WIDTH = 0;
parameter TRG_POLARITY = 0; parameter TRG_POLARITY = 0;
@ -1817,6 +1818,27 @@ input [ARGS_WIDTH-1:0] ARGS;
endmodule endmodule
// --------------------------------------------------------
module \$check (A, EN, TRG, ARGS);
parameter FLAVOR = "";
parameter PRIORITY = 0;
parameter FORMAT = "";
parameter ARGS_WIDTH = 0;
parameter TRG_ENABLE = 1;
parameter TRG_WIDTH = 0;
parameter TRG_POLARITY = 0;
input A;
input EN;
input [TRG_WIDTH-1:0] TRG;
input [ARGS_WIDTH-1:0] ARGS;
endmodule
// -------------------------------------------------------- // --------------------------------------------------------
`ifndef SIMLIB_NOSR `ifndef SIMLIB_NOSR