mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 19:52:31 +00:00
Code Activity

Merge pull request #4128 from whitequark/check-cell

Browse source 
Add `$check` cell to represent assertions with messages
This commit is contained in:
Catherine 2024-02-03 18:39:00 +00:00 • committed by GitHub
commit 3caac53827
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
62 changed files with 1144 additions and 557 deletions
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)
{
return type.isPublic() || type == ID($print);
return type.in(ID($print), ID($check));
}
bool is_cxxrtl_blackbox_cell(const RTLIL::Cell *cell)
@ -282,7 +282,7 @@ struct FlowGraph {
CONNECT,
CELL_SYNC,
CELL_EVAL,
PRINT_SYNC,
EFFECT_SYNC,
PROCESS_SYNC,
PROCESS_CASE,
MEM_RDPORT,
@ -292,7 +292,7 @@ struct FlowGraph {
Type type;
RTLIL::SigSig connect = {};
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 Mem *mem = nullptr;
int portidx;
@ -480,11 +480,11 @@ struct FlowGraph {
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->type = Node::Type::PRINT_SYNC;
node->print_sync_cells = cells;
node->type = Node::Type::EFFECT_SYNC;
node->cells = cells;
nodes.push_back(node);
return node;
}
@ -1063,99 +1063,6 @@ struct CxxrtlWorker {
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)
{
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)
{
std::vector<const RTLIL::Cell*> inlined_cells;
@ -1322,30 +1367,34 @@ struct CxxrtlWorker {
f << " = ";
dump_cell_expr(cell, for_debug);
f << ";\n";
// $print cell
} else if (cell->type == ID($print)) {
// Effectful cells
} else if (is_effectful_cell(cell->type)) {
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));
if (!cell->getParam(ID::TRG_ENABLE).as_bool()) { // async $print cell
f << indent << "auto " << mangle(cell) << "_curr = ";
if (!cell->getParam(ID::TRG_ENABLE).as_bool()) { // async effectful cell
f << indent << "auto " << mangle(cell) << "_next = ";
dump_sigspec_rhs(cell->getPort(ID::EN));
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 << indent << "if (" << mangle(cell) << " != " << mangle(cell) << "_curr) {\n";
f << indent << "if (" << mangle(cell) << " != " << mangle(cell) << "_next) {\n";
inc_indent();
dump_print(cell);
f << indent << mangle(cell) << " = " << mangle(cell) << "_curr;\n";
dump_effect(cell);
f << indent << mangle(cell) << " = " << mangle(cell) << "_next;\n";
dec_indent();
f << indent << "}\n";
} else { // initial $print cell
} else { // initial effectful cell
f << indent << "if (!" << mangle(cell) << ") {\n";
inc_indent();
dump_print(cell);
dump_effect(cell);
f << indent << mangle(cell) << " = value<1>{1u};\n";
dec_indent();
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)
{
auto &port = mem->rd_ports[portidx];
@ -2047,11 +2137,10 @@ struct CxxrtlWorker {
}
}
for (auto cell : module->cells()) {
// Certain $print cells have additional state, which must be reset as well.
if (cell->type == ID($print) && !cell->getParam(ID::TRG_ENABLE).as_bool())
f << indent << mangle(cell) << " = value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << ">();\n";
if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0)
f << indent << mangle(cell) << " = value<1>();\n";
// Async and initial effectful cells have additional state, which must be reset as well.
if (is_effectful_cell(cell->type))
if (!cell->getParam(ID::TRG_ENABLE).as_bool() || cell->getParam(ID::TRG_WIDTH).as_int() == 0)
f << indent << mangle(cell) << " = {};\n";
if (is_internal_cell(cell->type))
continue;
f << indent << mangle(cell);
@ -2099,8 +2188,8 @@ struct CxxrtlWorker {
case FlowGraph::Node::Type::CELL_EVAL:
dump_cell_eval(node.cell);
break;
case FlowGraph::Node::Type::PRINT_SYNC:
dump_sync_print(node.print_sync_cells);
case FlowGraph::Node::Type::EFFECT_SYNC:
dump_cell_effect_sync(node.cells);
break;
case FlowGraph::Node::Type::PROCESS_CASE:
dump_process_case(node.process);
@ -2481,11 +2570,15 @@ struct CxxrtlWorker {
f << "\n";
bool has_cells = false;
for (auto cell : module->cells()) {
// Certain $print cells have additional state, which requires storage.
if (cell->type == ID($print) && !cell->getParam(ID::TRG_ENABLE).as_bool())
f << indent << "value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << "> " << mangle(cell) << ";\n";
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 and initial effectful cells have additional state, which requires storage.
if (is_effectful_cell(cell->type)) {
if (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
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))
continue;
dump_attrs(cell);
@ -2803,8 +2896,8 @@ struct CxxrtlWorker {
cell->parameters[ID::CLK_POLARITY].as_bool() ? RTLIL::STp : RTLIL::STn);
}
// $print cells may be triggered on posedge/negedge events.
if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool()) {
// Effectful cells may be triggered on posedge/negedge events.
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++) {
RTLIL::SigBit trg = cell->getPort(ID::TRG).extract(i, 1);
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.
pool<FlowGraph::Node*, hash_ptr_ops> worklist;
for (auto node : flow.nodes) {
if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type))
worklist.insert(node); // node has effects
else if (node->type == FlowGraph::Node::Type::PRINT_SYNC)
worklist.insert(node); // node is sync $print
if (node->type == FlowGraph::Node::Type::CELL_EVAL && !is_internal_cell(node->cell->type))
worklist.insert(node); // node evaluates a submodule
else if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type))
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)
worklist.insert(node); // node is memory write
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().
// Accumulate sync $print cells per trigger condition.
dict<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> sync_print_cells;
// Accumulate sync effectful cells per trigger condition.
dict<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> effect_sync_cells;
for (auto node : node_order)
if (live_nodes[node]) {
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_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
schedule[module].push_back(*node);
}
for (auto &it : sync_print_cells) {
auto node = flow.add_print_sync_node(it.second);
for (auto &it : effect_sync_cells) {
auto node = flow.add_effect_sync_node(it.second);
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;
};
// 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 {
// Called by generated formatting code to evaluate a Verilog `$time` expression.
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) {
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

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)
{
Fmt fmt = {};
Fmt fmt;
fmt.parse_rtlil(cell);
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");
}
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_)) {
@ -1814,6 +1831,39 @@ 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") {
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
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) {
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) {
f << stringf("%s" " if (", indent.c_str());
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());
@ -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)
{
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);
@ -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;
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;
}
@ -2274,8 +2344,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);

6
docs/source/CHAPTER_CellLib.rst
View file

@ -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.
@ -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:

189
frontends/ast/genrtlil.cc
View file

@ -163,6 +163,28 @@ static RTLIL::SigSpec mux2rtlil(AstNode *that, const RTLIL::SigSpec &cond, const
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
struct AST_INTERNAL::LookaheadRewriter
{
@ -316,10 +338,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);
@ -703,8 +725,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;
@ -717,18 +741,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;
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);
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));
cell->setPort(ID::EN, en);
int default_base = 10;
if (ast->str.back() == 'b')
@ -766,7 +787,7 @@ struct AST_INTERNAL::ProcessGenerator
args.push_back(arg);
}
Fmt fmt = {};
Fmt fmt;
fmt.parse_verilog(args, /*sformat_like=*/false, default_base, /*task_name=*/ast->str, current_module->name);
if (ast->str.substr(0, 8) == "$display")
fmt.append_string("\n");
@ -776,6 +797,70 @@ 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 ()"; }
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_FOR:
break;
@ -1242,28 +1327,6 @@ void AstNode::detectSignWidth(int &width_hint, bool &sign_hint, bool *found_real
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
// 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.
@ -1945,48 +2008,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);
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 ()"; }
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();
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++);
else
cellname = str;
check_unique_id(current_module, cellname, this, "procedural assertion");
RTLIL::Cell *cell = current_module->addCell(cellname, celltype);
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);
// No message is emitted to ensure Verilog code roundtrips correctly.
Fmt fmt;
fmt.emit_rtlil(cell);
}
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);
}
Fmt fmt = {};
Fmt fmt;
fmt.parse_verilog(args, sformat_like, default_base, /*task_name=*/str, current_module->name);
return fmt;
}
@ -784,7 +784,7 @@ AstNode *AstNode::clone_at_zero()
pointee->type != AST_MEMORY)
break;
YS_FALLTHROUGH;
YS_FALLTHROUGH
case AST_MEMRD:
detectSignWidth(width_hint, sign_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:;
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
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) {

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($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($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($get_tag), {ID::A}, {ID::Y});
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(extract_order)
X(F)
X(FLAVOR)
X(FORMAT)
X(force_downto)
X(force_upto)

22
kernel/rtlil.cc
View file

@ -1068,6 +1068,12 @@ namespace {
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)
{
auto it = cell->connections_.find(name);
@ -1747,6 +1753,22 @@ namespace {
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($_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; }

183
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);
@ -238,25 +310,31 @@ struct ChformalPass : public Pass {
cell->setPort(ID::A, A_map.first);
cell->setPort(ID::EN, EN_map.first);
}
}
}
else
if (mode == 'd')
{
for (auto cell : constr_cells)
for (int i = 0; i < mode_arg; i++)
{
SigSpec orig_a = cell->getPort(ID::A);
SigSpec orig_en = cell->getPort(ID::EN);
if (is_triggered_check_cell(cell))
log_error("Cannot delay edge triggered $check cell %s, run async2sync or clk2fflogic first.\n", log_id(cell));
Wire *new_a = module->addWire(NEW_ID);
Wire *new_en = module->addWire(NEW_ID);
new_en->attributes[ID::init] = State::S0;
for (int i = 0; i < mode_arg; i++)
{
SigSpec orig_a = cell->getPort(ID::A);
SigSpec orig_en = cell->getPort(ID::EN);
module->addFf(NEW_ID, orig_a, new_a);
module->addFf(NEW_ID, orig_en, new_en);
Wire *new_a = module->addWire(NEW_ID);
Wire *new_en = module->addWire(NEW_ID);
new_en->attributes[ID::init] = State::S0;
cell->setPort(ID::A, new_a);
cell->setPort(ID::EN, new_en);
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
@ -278,21 +356,76 @@ struct ChformalPass : public Pass {
if (mode =='p')
{
for (auto cell : constr_cells)
module->addCover(NEW_ID_SUFFIX("coverenable"),
cell->getPort(ID::EN), State::S1, cell->get_src_attribute());
{
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));
}
}
}
}
}

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)
for (auto c : mod->cells()) {
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];

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)))
return true;
if (cell->type == ID($print))
if (cell->type == ID($print) || cell->type == ID($check))
return true;
if (cell->has_keep_attr())

73
passes/sat/async2sync.cc
View file

@ -41,31 +41,88 @@ struct Async2syncPass : public Pass {
log("reset value in the next cycle regardless of the data-in value at the time of\n");
log("the clock edge.\n");
log("\n");
log(" -nolower\n");
log(" Do not automatically run 'chformal -lower' to lower $check cells.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
// bool flag_noinit = false;
bool flag_nolower = false;
log_header(design, "Executing ASYNC2SYNC pass.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
// if (args[argidx] == "-noinit") {
// flag_noinit = true;
// continue;
// }
if (args[argidx] == "-nolower") {
flag_nolower = true;
continue;
}
break;
}
extra_args(args, argidx, design);
bool have_check_cells = false;
for (auto module : design->selected_modules())
{
SigMap sigmap(module);
FfInitVals initvals(&sigmap, module);
SigBit initstate;
for (auto cell : vector<Cell*>(module->selected_cells()))
{
if (cell->type.in(ID($print), ID($check)))
{
if (cell->type == ID($check))
have_check_cells = true;
bool trg_enable = cell->getParam(ID(TRG_ENABLE)).as_bool();
if (!trg_enable)
continue;
int trg_width = cell->getParam(ID(TRG_WIDTH)).as_int();
if (trg_width > 1)
log_error("$check cell %s with TRG_WIDTH > 1 is not support by async2sync, use clk2fflogic.\n", log_id(cell));
if (trg_width == 0) {
if (initstate == State::S0)
initstate = module->Initstate(NEW_ID);
SigBit sig_en = cell->getPort(ID::EN);
cell->setPort(ID::EN, module->And(NEW_ID, sig_en, initstate));
} else {
SigBit sig_en = cell->getPort(ID::EN);
SigSpec sig_args = cell->getPort(ID::ARGS);
bool trg_polarity = cell->getParam(ID(TRG_POLARITY)).as_bool();
SigBit sig_trg = cell->getPort(ID::TRG);
Wire *sig_en_q = module->addWire(NEW_ID);
Wire *sig_args_q = module->addWire(NEW_ID, GetSize(sig_args));
sig_en_q->attributes.emplace(ID::init, State::S0);
module->addDff(NEW_ID, sig_trg, sig_en, sig_en_q, trg_polarity, cell->get_src_attribute());
module->addDff(NEW_ID, sig_trg, sig_args, sig_args_q, trg_polarity, cell->get_src_attribute());
cell->setPort(ID::EN, sig_en_q);
cell->setPort(ID::ARGS, sig_args_q);
if (cell->type == ID($check)) {
SigBit sig_a = cell->getPort(ID::A);
Wire *sig_a_q = module->addWire(NEW_ID);
sig_a_q->attributes.emplace(ID::init, State::S1);
module->addDff(NEW_ID, sig_trg, sig_a, sig_a_q, trg_polarity, cell->get_src_attribute());
cell->setPort(ID::A, sig_a_q);
}
}
cell->setPort(ID::TRG, SigSpec());
cell->setParam(ID::TRG_ENABLE, false);
cell->setParam(ID::TRG_WIDTH, 0);
cell->setParam(ID::TRG_POLARITY, false);
cell->set_bool_attribute(ID(trg_on_gclk));
continue;
}
if (!RTLIL::builtin_ff_cell_types().count(cell->type))
continue;
@ -273,6 +330,12 @@ struct Async2syncPass : public Pass {
ff.emit();
}
}
if (have_check_cells && !flag_nolower) {
log_push();
Pass::call(design, "chformal -lower");
log_pop();
}
}
} Async2syncPass;

191
passes/sat/clk2fflogic.cc
View file

@ -48,6 +48,9 @@ struct Clk2fflogicPass : public Pass {
log("reset value in the next cycle regardless of the data-in value at the time of\n");
log("the clock edge.\n");
log("\n");
log(" -nolower\n");
log(" Do not automatically run 'chformal -lower' to lower $check cells.\n");
log("\n");
}
// Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted.
SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) {
@ -117,21 +120,23 @@ struct Clk2fflogicPass : public Pass {
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
// bool flag_noinit = false;
bool flag_nolower = false;
log_header(design, "Executing CLK2FFLOGIC pass (convert clocked FFs to generic $ff cells).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
// if (args[argidx] == "-noinit") {
// flag_noinit = true;
// continue;
// }
if (args[argidx] == "-nolower") {
flag_nolower = true;
continue;
}
break;
}
extra_args(args, argidx, design);
bool have_check_cells = false;
for (auto module : design->selected_modules())
{
SigMap sigmap(module);
@ -194,79 +199,137 @@ struct Clk2fflogicPass : public Pass {
mem.emit();
}
SigBit initstate;
for (auto cell : vector<Cell*>(module->selected_cells()))
{
SigSpec qval;
if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
FfData ff(&initvals, cell);
if (cell->type.in(ID($print), ID($check)))
{
if (cell->type == ID($check))
have_check_cells = true;
if (ff.has_gclk) {
// Already a $ff or $_FF_ cell.
bool trg_enable = cell->getParam(ID(TRG_ENABLE)).as_bool();
if (!trg_enable)
continue;
}
if (ff.has_clk) {
log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_signal(ff.sig_clk), log_signal(ff.sig_d), log_signal(ff.sig_q));
} else if (ff.has_aload) {
log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_q));
int trg_width = cell->getParam(ID(TRG_WIDTH)).as_int();
if (trg_width == 0) {
if (initstate == State::S0)
initstate = module->Initstate(NEW_ID);
SigBit sig_en = cell->getPort(ID::EN);
cell->setPort(ID::EN, module->And(NEW_ID, sig_en, initstate));
} else {
// $sr.
log("Replacing %s.%s (%s): SET=%s, CLR=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_q));
SigBit sig_en = cell->getPort(ID::EN);
SigSpec sig_args = cell->getPort(ID::ARGS);
Const trg_polarity = cell->getParam(ID(TRG_POLARITY));
SigSpec sig_trg = cell->getPort(ID::TRG);
SigSpec sig_trg_sampled;
for (auto const &bit : sig_trg)
sig_trg_sampled.append(sample_control_edge(module, bit, trg_polarity[GetSize(sig_trg_sampled)] == State::S1, false));
SigSpec sig_args_sampled = sample_data(module, sig_args, Const(State::S0, GetSize(sig_args)), false, false).sampled;
SigBit sig_en_sampled = sample_data(module, sig_en, State::S0, false, false).sampled;
SigBit sig_trg_combined = module->ReduceOr(NEW_ID, sig_trg_sampled);
cell->setPort(ID::EN, module->And(NEW_ID, sig_en_sampled, sig_trg_combined));
cell->setPort(ID::ARGS, sig_args_sampled);
if (cell->type == ID($check)) {
SigBit sig_a_sampled = sample_data(module, sig_en, State::S1, false, false).sampled;
cell->setPort(ID::A, sig_a_sampled);
}
}
ff.remove();
cell->setPort(ID::TRG, SigSpec());
if (ff.has_clk)
ff.unmap_ce_srst();
cell->setParam(ID::TRG_ENABLE, false);
cell->setParam(ID::TRG_WIDTH, 0);
cell->setParam(ID::TRG_POLARITY, false);
cell->set_bool_attribute(ID(trg_on_gclk));
auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine, true).sampled;
if (ff.has_clk) {
// The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs
auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine);
auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine);
next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine);
}
SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst;
// The check for a constant sig_aload is also done by opt_dff, but when using verific and running
// clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
// generating a lot of extra logic.
bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1);
if (has_nonconst_aload) {
sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine);
// The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs
sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine);
}
if (ff.has_sr) {
sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine);
sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine);
}
if (ff.has_arst)
sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine);
// First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous
// implementation, this approach correctly handles all the cases of multiple signals changing simultaneously.
for (int current = 0; current < 2; current++) {
if (has_nonconst_aload)
next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine);
if (ff.has_sr)
next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine);
if (ff.has_arst)
next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine);
}
module->connect(ff.sig_q, next_q);
continue;
}
if (!RTLIL::builtin_ff_cell_types().count(cell->type))
continue;
FfData ff(&initvals, cell);
if (ff.has_gclk) {
// Already a $ff or $_FF_ cell.
continue;
}
if (ff.has_clk) {
log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_signal(ff.sig_clk), log_signal(ff.sig_d), log_signal(ff.sig_q));
} else if (ff.has_aload) {
log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_q));
} else {
// $sr.
log("Replacing %s.%s (%s): SET=%s, CLR=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_q));
}
ff.remove();
if (ff.has_clk)
ff.unmap_ce_srst();
auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine, true).sampled;
if (ff.has_clk) {
// The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs
auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine);
auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine);
next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine);
}
SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst;
// The check for a constant sig_aload is also done by opt_dff, but when using verific and running
// clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
// generating a lot of extra logic.
bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1);
if (has_nonconst_aload) {
sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine);
// The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs
sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine);
}
if (ff.has_sr) {
sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine);
sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine);
}
if (ff.has_arst)
sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine);
// First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous
// implementation, this approach correctly handles all the cases of multiple signals changing simultaneously.
for (int current = 0; current < 2; current++) {
if (has_nonconst_aload)
next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine);
if (ff.has_sr)
next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine);
if (ff.has_arst)
next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine);
}
module->connect(ff.sig_q, next_q);
}
}
if (have_check_cells && !flag_nolower) {
log_push();
Pass::call(design, "chformal -lower");
log_pop();
}
}
} Clk2fflogicPass;

26
techlibs/common/simlib.v
View file

@ -1803,11 +1803,12 @@ endmodule
module \$print (EN, TRG, ARGS);
parameter PRIORITY = 0;
parameter FORMAT = "";
parameter ARGS_WIDTH = 0;
parameter PRIORITY = 0;
parameter TRG_ENABLE = 1;
parameter TRG_ENABLE = 1;
parameter TRG_WIDTH = 0;
parameter TRG_POLARITY = 0;
@ -1817,6 +1818,27 @@ input [ARGS_WIDTH-1:0] ARGS;
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

3
tests/arch/quicklogic/qlf_k6n10f/dsp.ys
View file

@ -107,7 +107,7 @@ reg [7:0] i = 0;
always @(posedge clk) begin
if (i < VECTORLEN) begin
// FIXME: for some reason the first assert fails (despite comparing zero to zero)
if (i > 0)
if (i > 0)
assert(y == y_expected);
i <= i + 1;
end
@ -117,4 +117,5 @@ EOF
read_verilog +/quicklogic/qlf_k6n10f/dsp_sim.v
hierarchy -top testbench
proc
async2sync
sim -assert -q -clock clk -n 20

17
tests/arch/quicklogic/qlf_k6n10f/mem_gen.py
View file

@ -36,7 +36,7 @@ blockram_tests: "list[tuple[list[tuple[str, int]], str, list[str]]]" = [
([("ADDRESS_WIDTH", 14), ("DATA_WIDTH", 2)], "sync_ram_*dp", ["-assert-count 1 t:TDP36K", "-assert-count 1 t:TDP36K a:port_a_width=2 %i"]),
([("ADDRESS_WIDTH", 15), ("DATA_WIDTH", 1)], "sync_ram_*dp", ["-assert-count 1 t:TDP36K", "-assert-count 1 t:TDP36K a:port_a_width=1 %i"]),
# 2x asymmetric (1024x36bit write / 2048x18bit read or vice versa = 1TDP36K)
# 2x asymmetric (1024x36bit write / 2048x18bit read or vice versa = 1TDP36K)
([("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 18), ("SHIFT_VAL", 1)], "sync_ram_sdp_w*r", ["-assert-count 1 t:TDP36K"]),
([("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 16), ("SHIFT_VAL", 1)], "sync_ram_sdp_w*r", ["-assert-count 1 t:TDP36K"]),
([("ADDRESS_WIDTH", 12), ("DATA_WIDTH", 9), ("SHIFT_VAL", 1)], "sync_ram_sdp_w*r", ["-assert-count 1 t:TDP36K"]),
@ -131,6 +131,7 @@ read_verilog -defer -formal mem_tb.v
chparam{param_str} -set VECTORLEN {vectorlen} TB
hierarchy -top TB -check
prep
async2sync
log ** CHECKING SIMULATION FOR TEST {top} WITH PARAMS{param_str}
sim -clock clk -n {vectorlen} -assert
"""
@ -254,16 +255,16 @@ sim_tests: list[TestClass] = [
{"rq_a": 0x5678},
]
),
TestClass( # basic TDP test
TestClass( # basic TDP test
# note that the testbench uses ra and wa, while the common TDP model
# uses a shared address
params={"ADDRESS_WIDTH": 10, "DATA_WIDTH": 36},
top="sync_ram_tdp",
assertions=[],
test_steps=[
{"wce_a": 1, "ra_a": 0x0A, "wce_b": 1, "ra_b": 0xBA,
{"wce_a": 1, "ra_a": 0x0A, "wce_b": 1, "ra_b": 0xBA,
"wd_a": 0xdeadbeef, "wd_b": 0x5a5a5a5a},
{"wce_a": 1, "ra_a": 0xFF,
{"wce_a": 1, "ra_a": 0xFF,
"wd_a": 0},
{"rce_a": 1, "ra_a": 0x0A, "rce_b": 1, "ra_b": 0x0A},
{"rq_a": 0xdeadbeef, "rq_b": 0xdeadbeef},
@ -276,9 +277,9 @@ sim_tests: list[TestClass] = [
top="sync_ram_tdp",
assertions=[],
test_steps=[
{"wce_a": 1, "ra_a": 0x0F, "wce_b": 1, "ra_b": 0xBA,
{"wce_a": 1, "ra_a": 0x0F, "wce_b": 1, "ra_b": 0xBA,
"wd_a": 0xdeadbeef, "wd_b": 0x5a5a5a5a},
{"wce_a": 1, "ra_a": 0xFF,
{"wce_a": 1, "ra_a": 0xFF,
"wd_a": 0},
{"rce_a": 1, "ra_a": 0x0F, "rce_b": 1, "ra_b": 0x0A},
{"rq_a": 0, "rq_b": 0x00005a5a},
@ -291,7 +292,7 @@ sim_tests: list[TestClass] = [
top="sync_ram_tdp",
assertions=[],
test_steps=[
{"wce_a": 1, "ra_a": 0x0A, "wce_b": 1, "ra_b": 0xBA,
{"wce_a": 1, "ra_a": 0x0A, "wce_b": 1, "ra_b": 0xBA,
"wd_a": 0xdeadbeef, "wd_b": 0x5a5a5a5a},
{"wce_a": 1, "ra_a": 0xBA, "rce_b": 1, "ra_b": 0xBA,
"wd_a": 0xa5a5a5a5},
@ -409,7 +410,7 @@ for sim_test in sim_tests:
fn = f"t_mem{i}.ys"
f = open(fn, mode="w")
j = 0
# output yosys script test file
print(
blockram_template.format(param_str=param_str, top=top),

1
tests/arch/quicklogic/qlf_k6n10f/meminit.ys
View file

@ -10,5 +10,6 @@ select -assert-count 1 t:TDP36K a:is_split=0 %i
select -assert-count 1 t:TDP36K a:was_split_candidate=0 %i
read_verilog +/quicklogic/common/cells_sim.v +/quicklogic/qlf_k6n10f/cells_sim.v +/quicklogic/qlf_k6n10f/brams_sim.v +/quicklogic/qlf_k6n10f/sram1024x18_mem.v +/quicklogic/qlf_k6n10f/ufifo_ctl.v +/quicklogic/qlf_k6n10f/TDP18K_FIFO.v
prep
async2sync
hierarchy -top top
sim -assert -q -n 12 -clock clk

1
tests/arch/xilinx/dsp_abc9.ys
View file

@ -30,6 +30,7 @@ module top(output [42:0] P);
assert property (P == 42*42);
endmodule
EOT
async2sync
techmap -map +/xilinx/xc7_dsp_map.v
verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
synth_xilinx -abc9

2
tests/gen-tests-makefile.sh
View file

@ -75,7 +75,7 @@ generate_tests() {
if [[ $do_sv = true ]]; then
for x in *.sv; do
if [ ! -f "${x%.sv}.ys" ]; then
generate_ys_test "$x" "-p \"prep -top top; sat -enable_undef -verify -prove-asserts\" $yosys_args"
generate_ys_test "$x" "-p \"prep -top top; async2sync; sat -enable_undef -verify -prove-asserts\" $yosys_args"
fi;
done
fi;

2
tests/sat/asserts.ys
View file

@ -1,3 +1,3 @@
read_verilog -sv asserts.v
hierarchy; proc; opt
hierarchy; proc; opt; async2sync
sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts

2
tests/sat/asserts_seq.ys
View file

@ -1,5 +1,5 @@
read_verilog -sv asserts_seq.v
hierarchy; proc; opt
hierarchy; proc; opt; async2sync
sat -verify -prove-asserts -tempinduct -seq 1 test_001
sat -falsify -prove-asserts -tempinduct -seq 1 test_002

2
tests/sat/initval.ys
View file

@ -1,5 +1,5 @@
read_verilog -sv initval.v
proc;;
proc; async2sync;;
sat -seq 10 -prove-asserts

2
tests/sat/sizebits.ys
View file

@ -1,2 +1,2 @@
read_verilog -sv sizebits.sv
prep; sat -verify -prove-asserts
prep; async2sync; sat -verify -prove-asserts

2
tests/svtypes/enum_simple.ys
View file

@ -1,5 +1,5 @@
read_verilog -sv enum_simple.sv
hierarchy; proc; opt
hierarchy; proc; opt; async2sync
sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts -show-all

1
tests/svtypes/struct_dynamic_range.ys
View file

@ -4,4 +4,5 @@ select -assert-count 2 t:$shift
select -assert-count 2 t:$shiftx
prep -top top
flatten
async2sync
sat -enable_undef -verify -prove-asserts

4
tests/svtypes/typedef_initial_and_assign.ys
View file

@ -9,6 +9,6 @@ logger -expect warning "reg '\\var_18' is assigned in a continuous assignment" 1
logger -expect warning "reg '\\var_19' is assigned in a continuous assignment" 1
read_verilog -sv typedef_initial_and_assign.sv
hierarchy; proc; opt
hierarchy; proc; opt; async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

2
tests/svtypes/typedef_struct_port.ys
View file

@ -1,5 +1,5 @@
read_verilog -sv typedef_struct_port.sv
hierarchy; proc; opt
hierarchy; proc; opt; async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all
select -module test_parser

68
tests/various/chformal_check.ys Normal file
View file

@ -0,0 +1,68 @@
read_verilog -formal <<EOT
module top(input clk, a, en);
wire a_q = '0;
wire en_q = '0;
always @(posedge clk) begin
a_q <= a;
en_q <= en;
end
always @(posedge clk)
if (en_q)
assert(a_q);
endmodule
EOT
prep
design -save prep
select -assert-count 1 t:$check r:FLAVOR=assert %i
chformal -assert2assume
select -assert-count 1 t:$check r:FLAVOR=assume %i
chformal -assume2assert
select -assert-count 1 t:$check r:FLAVOR=assert %i
async2sync
chformal -lower
select -assert-count 1 t:$assert
design -load prep
chformal -assert2assume
async2sync
chformal -lower
chformal -assume -early
rename -enumerate -pattern assume_% t:$assume
expose -evert t:$assume
design -save gold
design -load prep
chformal -assert2assume
chformal -assume -early
async2sync
chformal -lower
rename -enumerate -pattern assume_% t:$assume
expose -evert t:$assume
design -save gate
design -reset
design -copy-from gold -as gold top
design -copy-from gate -as gate top
miter -equiv -flatten -make_assert gold gate miter
sat -verify -prove-asserts -tempinduct miter

45
tests/various/chformal_coverenable.ys
View file

@ -2,10 +2,10 @@ read_verilog -formal <<EOT
module top(input a, b, c, d);
always @* begin
if (a) assert (b == c);
if (!a) assert (b != c);
if (b) assume (c);
if (c) cover (d);
if (a) c0: assert (b == c);
if (!a) c1: assert (b != c);
if (b) c2: assume (c);
if (c) c3: cover (d);
end
endmodule
@ -13,6 +13,10 @@ EOT
prep -top top
design -save prep
async2sync
select -assert-count 1 t:$cover
chformal -cover -coverenable
@ -23,3 +27,36 @@ select -assert-count 4 t:$cover
chformal -assume -coverenable
select -assert-count 5 t:$cover
autoname */t:$cover
expose -evert */c? */c?_EN_$cover_*
design -save a2s_first
design -load prep
select -assert-count 1 r:FLAVOR=cover
chformal -cover -coverenable
select -assert-count 2 r:FLAVOR=cover
chformal -assert -coverenable
select -assert-count 4 r:FLAVOR=cover
chformal -assume -coverenable
select -assert-count 5 r:FLAVOR=cover
async2sync
autoname */t:$cover
expose -evert */c? */c?_EN_$cover_*
design -save a2s_last
design -reset
design -copy-from a2s_first -as gold top
design -copy-from a2s_last -as gate top
miter -equiv -flatten -make_assert gold gate miter
sat -verify -prove-asserts -tempinduct miter

3
tests/various/chparam.sh
View file

@ -37,14 +37,17 @@ EOT
if ../../yosys -q -p 'verific -sv chparam1.sv'; then
../../yosys -q -p 'verific -sv chparam1.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
-p 'async2sync' \
-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
../../yosys -q -p 'verific -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
-p 'async2sync' \
-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
fi
../../yosys -q -p 'read_verilog -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
-p 'async2sync' \
-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'

27
tests/various/clk2fflogic_effects.sh Executable file
View file

@ -0,0 +1,27 @@
#!/usr/bin/env bash
set -ex
../../yosys -p "
read_verilog -formal -DFAST clk2fflogic_effects.sv
hierarchy -top top; proc;;
tee -o clk2fflogic_effects.sim.log sim -fst /tmp/sim.fst -q -n 16
"
../../yosys -p "
read_verilog -formal -DFAST clk2fflogic_effects.sv
hierarchy -top top; proc;;
clk2fflogic;;
tee -o clk2fflogic_effects.clk2fflogic.log sim -fst /tmp/sim.fst -q -n 16
"
iverilog -g2012 -o clk2fflogic_effects.iv.out clk2fflogic_effects.sv
./clk2fflogic_effects.iv.out > clk2fflogic_effects.iv.log
sort clk2fflogic_effects.iv.log > clk2fflogic_effects.iv.sorted.log
tail +3 clk2fflogic_effects.sim.log | sort > clk2fflogic_effects.sim.sorted.log
tail +3 clk2fflogic_effects.clk2fflogic.log | sort > clk2fflogic_effects.clk2fflogic.sorted.log
cmp clk2fflogic_effects.iv.sorted.log clk2fflogic_effects.sim.sorted.log
cmp clk2fflogic_effects.iv.sorted.log clk2fflogic_effects.clk2fflogic.sorted.log

82
tests/various/clk2fflogic_effects.sv Normal file
View file

@ -0,0 +1,82 @@
module top;
(* gclk *)
reg gclk;
reg clk = 0;
always @(posedge gclk)
clk <= !clk;
reg [4:0] counter = 0;
reg eff_0_trg = '0;
reg eff_0_en = '0;
reg eff_1_trgA = '0;
reg eff_1_trgB = '0;
reg eff_1_en = '0;
reg eff_2_trgA = '0;
reg eff_2_trgB = '0;
reg eff_2_en = '0;
`ifdef FAST
always @(posedge gclk) begin
`else
always @(posedge clk) begin
`endif
counter <= counter + 1;
eff_0_trg = 32'b00000000000000110011001100101010 >> counter;
eff_0_en <= 32'b00000000000001100000110110110110 >> counter;
eff_1_trgA = 32'b00000000000000000011110000011110 >> counter;
eff_1_trgB = 32'b00000000000000001111000001111000 >> counter;
eff_1_en <= 32'b00000000000000001010101010101010 >> counter;
eff_2_trgA = counter[0];
eff_2_trgB = !counter[0];
eff_2_en <= 32'b00000000000000000000001111111100 >> counter;
end
always @(posedge eff_0_trg)
if (eff_0_en)
$display("%02d: eff0 +", counter);
always @(negedge eff_0_trg)
if (eff_0_en)
$display("%02d: eff0 -", counter);
always @(posedge eff_0_trg, negedge eff_0_trg)
if (eff_0_en)
$display("%02d: eff0 *", counter);
always @(posedge eff_1_trgA, posedge eff_1_trgB)
if (eff_1_en)
$display("%02d: eff1 ++", counter);
always @(posedge eff_1_trgA, negedge eff_1_trgB)
if (eff_1_en)
$display("%02d: eff1 +-", counter);
always @(negedge eff_1_trgA, posedge eff_1_trgB)
if (eff_1_en)
$display("%02d: eff1 -+", counter);
always @(negedge eff_1_trgA, negedge eff_1_trgB)
if (eff_1_en)
$display("%02d: eff1 --", counter);
always @(posedge eff_2_trgA, posedge eff_2_trgB)
if (eff_2_en)
$display("repeated");
`ifdef __ICARUS__
initial gclk = 0;
always @(gclk) gclk <= #5 !gclk;
always @(posedge gclk)
if (counter == 31)
$finish(0);
`endif
endmodule

1
tests/various/const_arg_loop.ys
View file

@ -3,4 +3,5 @@ hierarchy
proc
opt -full
select -module top
async2sync
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

1
tests/various/const_func.ys
View file

@ -4,4 +4,5 @@ proc
flatten
opt -full
select -module top
async2sync
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

1
tests/various/countbits.ys
View file

@ -4,4 +4,5 @@ proc
flatten
opt -full
select -module top
async2sync
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

1
tests/various/param_struct.ys
View file

@ -47,4 +47,5 @@ end
endmodule
EOF
hierarchy; proc; opt
async2sync
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

96
tests/various/smtlib2_module-expected.smt2
View file

@ -1,96 +0,0 @@
; SMT-LIBv2 description generated by Yosys $VERSION
; yosys-smt2-module smtlib2
(declare-sort |smtlib2_s| 0)
(declare-fun |smtlib2_is| (|smtlib2_s|) Bool)
(declare-fun |smtlib2#0| (|smtlib2_s|) (_ BitVec 8)) ; \a
; yosys-smt2-input a 8
; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": "a", "smtoffset": 0, "type": "input", "width": 8}
(define-fun |smtlib2_n a| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#0| state))
(declare-fun |smtlib2#1| (|smtlib2_s|) (_ BitVec 8)) ; \b
; yosys-smt2-input b 8
; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": "b", "smtoffset": 0, "type": "input", "width": 8}
(define-fun |smtlib2_n b| ((state |smtlib2_s|)) (_ BitVec 8) (|smtlib2#1| state))
; yosys-smt2-output add 8
; yosys-smt2-witness {"offset": 0, "path": ["\\add"], "smtname": "add", "smtoffset": 0, "type": "blackbox", "width": 8}
(define-fun |smtlib2_n add| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
)
(bvadd a b)
))
; yosys-smt2-output eq 1
; yosys-smt2-witness {"offset": 0, "path": ["\\eq"], "smtname": "eq", "smtoffset": 0, "type": "blackbox", "width": 1}
(define-fun |smtlib2_n eq| ((state |smtlib2_s|)) Bool (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
)
(= a b)
))
; yosys-smt2-output sub 8
; yosys-smt2-witness {"offset": 0, "path": ["\\sub"], "smtname": "sub", "smtoffset": 0, "type": "blackbox", "width": 8}
(define-fun |smtlib2_n sub| ((state |smtlib2_s|)) (_ BitVec 8) (let (
(|a| (|smtlib2_n a| state))
(|b| (|smtlib2_n b| state))
)
(bvadd a (bvneg b))
))
(define-fun |smtlib2_a| ((state |smtlib2_s|)) Bool true)
(define-fun |smtlib2_u| ((state |smtlib2_s|)) Bool true)
(define-fun |smtlib2_i| ((state |smtlib2_s|)) Bool true)
(define-fun |smtlib2_h| ((state |smtlib2_s|)) Bool true)
(define-fun |smtlib2_t| ((state |smtlib2_s|) (next_state |smtlib2_s|)) Bool true) ; end of module smtlib2
; yosys-smt2-module uut
(declare-sort |uut_s| 0)
(declare-fun |uut_is| (|uut_s|) Bool)
; yosys-smt2-cell smtlib2 s
; yosys-smt2-witness {"path": ["\\s"], "smtname": "s", "type": "cell"}
(declare-fun |uut#0| (|uut_s|) (_ BitVec 8)) ; \add
(declare-fun |uut#1| (|uut_s|) Bool) ; \eq
(declare-fun |uut#2| (|uut_s|) (_ BitVec 8)) ; \sub
(declare-fun |uut_h s| (|uut_s|) |smtlib2_s|)
; yosys-smt2-anyconst uut#3 8 smtlib2_module.v:14.17-14.26
; yosys-smt2-witness {"offset": 0, "path": ["\\a"], "smtname": 3, "smtoffset": 0, "type": "init", "width": 8}
(declare-fun |uut#3| (|uut_s|) (_ BitVec 8)) ; \a
; yosys-smt2-anyconst uut#4 8 smtlib2_module.v:14.32-14.41
; yosys-smt2-witness {"offset": 0, "path": ["\\b"], "smtname": 4, "smtoffset": 0, "type": "init", "width": 8}
(declare-fun |uut#4| (|uut_s|) (_ BitVec 8)) ; \b
(define-fun |uut#5| ((state |uut_s|)) (_ BitVec 8) (bvadd (|uut#3| state) (|uut#4| state))) ; \add2
(define-fun |uut#6| ((state |uut_s|)) Bool (= (|uut#0| state) (|uut#5| state))) ; $0$formal$smtlib2_module.v:28$1_CHECK[0:0]$9
; yosys-smt2-assert 0 $assert$smtlib2_module.v:28$19 smtlib2_module.v:28.17-29.22
(define-fun |uut_a 0| ((state |uut_s|)) Bool (or (|uut#6| state) (not true))) ; $assert$smtlib2_module.v:28$19
(define-fun |uut#7| ((state |uut_s|)) (_ BitVec 8) (bvsub (|uut#3| state) (|uut#4| state))) ; \sub2
(define-fun |uut#8| ((state |uut_s|)) Bool (= (|uut#2| state) (|uut#7| state))) ; $0$formal$smtlib2_module.v:29$2_CHECK[0:0]$11
; yosys-smt2-assert 1 $assert$smtlib2_module.v:29$20 smtlib2_module.v:29.23-30.22
(define-fun |uut_a 1| ((state |uut_s|)) Bool (or (|uut#8| state) (not true))) ; $assert$smtlib2_module.v:29$20
(define-fun |uut#9| ((state |uut_s|)) Bool (= (|uut#3| state) (|uut#4| state))) ; $eq$smtlib2_module.v:31$17_Y
(define-fun |uut#10| ((state |uut_s|)) Bool (= (ite (|uut#1| state) #b1 #b0) (ite (|uut#9| state) #b1 #b0))) ; $0$formal$smtlib2_module.v:30$3_CHECK[0:0]$13
; yosys-smt2-assert 2 $assert$smtlib2_module.v:30$21 smtlib2_module.v:30.23-31.25
(define-fun |uut_a 2| ((state |uut_s|)) Bool (or (|uut#10| state) (not true))) ; $assert$smtlib2_module.v:30$21
(define-fun |uut_a| ((state |uut_s|)) Bool (and
(|uut_a 0| state)
(|uut_a 1| state)
(|uut_a 2| state)
(|smtlib2_a| (|uut_h s| state))
))
(define-fun |uut_u| ((state |uut_s|)) Bool
(|smtlib2_u| (|uut_h s| state))
)
(define-fun |uut_i| ((state |uut_s|)) Bool
(|smtlib2_i| (|uut_h s| state))
)
(define-fun |uut_h| ((state |uut_s|)) Bool (and
(= (|uut_is| state) (|smtlib2_is| (|uut_h s| state)))
(= (|uut#3| state) (|smtlib2_n a| (|uut_h s| state))) ; smtlib2.a
(= (|uut#0| state) (|smtlib2_n add| (|uut_h s| state))) ; smtlib2.add
(= (|uut#4| state) (|smtlib2_n b| (|uut_h s| state))) ; smtlib2.b
(= (|uut#1| state) (|smtlib2_n eq| (|uut_h s| state))) ; smtlib2.eq
(= (|uut#2| state) (|smtlib2_n sub| (|uut_h s| state))) ; smtlib2.sub
(|smtlib2_h| (|uut_h s| state))
))
(define-fun |uut_t| ((state |uut_s|) (next_state |uut_s|)) Bool (and
(= (|uut#4| state) (|uut#4| next_state)) ; $anyconst$5 \b
(= (|uut#3| state) (|uut#3| next_state)) ; $anyconst$4 \a
(|smtlib2_t| (|uut_h s| state) (|uut_h s| next_state))
)) ; end of module uut
; yosys-smt2-topmod uut
; end of yosys output

5
tests/various/smtlib2_module.sh
View file

@ -1,5 +0,0 @@
#!/usr/bin/env bash
set -ex
../../yosys -q -p 'read_verilog -formal smtlib2_module.v; prep; write_smt2 smtlib2_module.smt2'
sed 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/;s/ *$//' smtlib2_module.smt2 > smtlib2_module-filtered.smt2
diff -au smtlib2_module-expected.smt2 smtlib2_module-filtered.smt2

33
tests/various/smtlib2_module.v
View file

@ -1,33 +0,0 @@
(* smtlib2_module *)
module smtlib2(a, b, add, sub, eq);
input [7:0] a, b;
(* smtlib2_comb_expr = "(bvadd a b)" *)
output [7:0] add;
(* smtlib2_comb_expr = "(bvadd a (bvneg b))" *)
output [7:0] sub;
(* smtlib2_comb_expr = "(= a b)" *)
output eq;
endmodule
(* top *)
module uut;
wire [7:0] a = $anyconst, b = $anyconst, add, sub, add2, sub2;
wire eq;
assign add2 = a + b;
assign sub2 = a - b;
smtlib2 s (
.a(a),
.b(b),
.add(add),
.sub(sub),
.eq(eq)
);
always @* begin
assert(add == add2);
assert(sub == sub2);
assert(eq == (a == b));
end
endmodule

1
tests/various/struct_access.ys
View file

@ -2,4 +2,5 @@ read_verilog -sv struct_access.sv
hierarchy
proc
opt
async2sync
sat -verify -seq 1 -prove-asserts -show-all

1
tests/verilog/asgn_expr.ys
View file

@ -1,3 +1,4 @@
read_verilog -sv asgn_expr.sv
proc
async2sync
sat -verify -prove-asserts -show-all

2
tests/verilog/atom_type_signedness.ys
View file

@ -14,6 +14,6 @@ always_comb begin
end
endmodule
EOT
hierarchy; proc; opt
hierarchy; proc; opt; async2sync
select -module dut
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

2
tests/verilog/bug2042-sv.ys
View file

@ -17,6 +17,7 @@ output reg b
endmodule
EOT
proc
async2sync
sat -verify -prove-asserts
@ -42,6 +43,7 @@ output b, c
endmodule
EOT
proc
async2sync
sat -verify -prove-asserts

1
tests/verilog/func_tern_hint.ys
View file

@ -1,4 +1,5 @@
read_verilog -sv func_tern_hint.sv
proc
opt
async2sync
sat -verify -seq 1 -prove-asserts -show-all

1
tests/verilog/func_upto.ys
View file

@ -3,5 +3,6 @@ hierarchy -top top
proc
flatten
opt -full
async2sync
select -module top
sat -verify -seq 1 -prove-asserts -enable_undef

1
tests/verilog/int_types.ys
View file

@ -3,5 +3,6 @@ hierarchy
proc
flatten
opt -full
async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

1
tests/verilog/mem_bounds.ys
View file

@ -3,4 +3,5 @@ proc
flatten
opt -full
select -module top
async2sync
sat -verify -seq 1 -tempinduct -prove-asserts -show-all -enable_undef

1
tests/verilog/net_types.ys
View file

@ -2,4 +2,5 @@ read_verilog -sv net_types.sv
hierarchy
proc
opt -full
async2sync
sat -verify -prove-asserts -show-all

1
tests/verilog/package_task_func.ys
View file

@ -1,4 +1,5 @@
read_verilog -sv package_task_func.sv
proc
opt -full
async2sync
sat -verify -seq 1 -prove-asserts -show-all

1
tests/verilog/param_no_default.ys
View file

@ -3,5 +3,6 @@ hierarchy
proc
flatten
opt -full
async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

1
tests/verilog/parameters_across_files.ys
View file

@ -16,5 +16,6 @@ hierarchy
proc
flatten
opt -full
async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

2
tests/verilog/past_signedness.ys
View file

@ -14,6 +14,7 @@ endmodule
EOT
prep -top top
async2sync
sim -n 3 -clock clk
design -reset
@ -32,4 +33,5 @@ endmodule
EOT
prep -top top
async2sync
sim -n 3 -clock clk

1
tests/verilog/prefix.ys
View file

@ -2,4 +2,5 @@ read_verilog -sv prefix.sv
hierarchy
proc
select -module top
async2sync
sat -verify -seq 1 -prove-asserts -show-all

3
tests/verilog/sign_array_query.ys
View file

@ -14,6 +14,7 @@ endmodule
EOT
prep -top top
async2sync
sim -n 3 -clock clk
design -reset
@ -32,6 +33,7 @@ endmodule
EOT
prep -top top
async2sync
sim -n 3 -clock clk
design -reset
@ -49,4 +51,5 @@ endmodule
EOT
prep -top top
async2sync
sim -n 3 -clock clk

1
tests/verilog/size_cast.ys
View file

@ -2,4 +2,5 @@ read_verilog -sv size_cast.sv
proc
opt -full
select -module top
async2sync
sat -verify -prove-asserts -show-all

1
tests/verilog/struct_access.ys
View file

@ -1,4 +1,5 @@
read_verilog -formal -sv struct_access.sv
proc
opt -full
async2sync
sat -verify -seq 1 -prove-asserts -show-all

1
tests/verilog/typedef_across_files.ys
View file

@ -19,5 +19,6 @@ EOF
proc
opt -full
async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

1
tests/verilog/typedef_legacy_conflict.ys
View file

@ -33,5 +33,6 @@ hierarchy
proc
flatten
opt -full
async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

1
tests/verilog/unbased_unsized.ys
View file

@ -3,5 +3,6 @@ hierarchy
proc
flatten
opt -full
async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

1
tests/verilog/unbased_unsized_shift.ys
View file

@ -3,5 +3,6 @@ hierarchy
proc
flatten
opt -full
async2sync
select -module top
sat -verify -seq 1 -tempinduct -prove-asserts -show-all

2
tests/verilog/unreachable_case_sign.ys
View file

@ -12,6 +12,7 @@ endmodule
EOT
prep -top top
async2sync
sim -n 3 -clock clk
design -reset
@ -29,5 +30,6 @@ endmodule
EOT
prep -top top
async2sync
sim -n 3 -clock clk