diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index c26750c98..86ea70b51 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -844,6 +844,7 @@ struct AST_INTERNAL::ProcessGenerator RTLIL::Cell *cell = current_module->addCell(cellname, ID($check)); set_src_attr(cell, ast); + cell->set_bool_attribute(ID(keep)); for (auto &attr : ast->attributes) { if (attr.second->type != AST_CONSTANT) log_file_error(*ast->location.begin.filename, ast->location.begin.line, "Attribute `%s' with non-constant value!\n", attr.first); diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index dffe6e8e0..c2cfe7e75 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -1846,7 +1846,10 @@ struct VerificSvaImporter if (mode_assume) c = module->addAssume(root_name, sig_a_q, sig_en_q); if (mode_cover) c = module->addCover(root_name, sig_a_q, sig_en_q); - if (c) importer->import_attributes(c->attributes, root); + if (c) { + c->set_bool_attribute(ID(keep)); + importer->import_attributes(c->attributes, root); + } } } catch (ParserErrorException) diff --git a/passes/opt/opt_merge.cc b/passes/opt/opt_merge.cc index 6cdcbc822..307c2bcd3 100644 --- a/passes/opt/opt_merge.cc +++ b/passes/opt/opt_merge.cc @@ -227,6 +227,11 @@ struct OptMergeWorker ct.cell_types.erase(ID($anyconst)); ct.cell_types.erase(ID($allseq)); ct.cell_types.erase(ID($allconst)); + ct.cell_types.erase(ID($check)); + ct.cell_types.erase(ID($assert)); + ct.cell_types.erase(ID($assume)); + ct.cell_types.erase(ID($live)); + ct.cell_types.erase(ID($cover)); log("Finding identical cells in module `%s'.\n", module->name); assign_map.set(module); diff --git a/tests/opt/opt_merge_properties.ys b/tests/opt/opt_merge_properties.ys new file mode 100644 index 000000000..dddc13bfb --- /dev/null +++ b/tests/opt/opt_merge_properties.ys @@ -0,0 +1,16 @@ +read_verilog -sv <