#ifdef YOSYS_ENABLE_VERIFIC
+pool<int> verific_sva_prims = {
+ // Copy&paste from Verific 3.16_484_32_170630 Netlist.h
+ PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
+ PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
+ PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
+ PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
+ PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
+ PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
+ PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
+ PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
+ PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
+ PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
+ PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
+ PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
+ PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
+ PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
+ PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
+ PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
+ PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
+ PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
+ PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
+};
+
string verific_error_msg;
void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
void import_sva_assert(VerificImporter *importer, Instance *inst);
void import_sva_assume(VerificImporter *importer, Instance *inst);
void import_sva_cover(VerificImporter *importer, Instance *inst);
-void svapp_assert(VerificImporter *importer, Instance *inst);
-void svapp_assume(VerificImporter *importer, Instance *inst);
-void svapp_cover(VerificImporter *importer, Instance *inst);
+void svapp_assert(Instance *inst);
+void svapp_assume(Instance *inst);
+void svapp_cover(Instance *inst);
struct VerificClockEdge {
Net *clock_net = nullptr;
bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
- pool<int> verific_sva_prims;
-
VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
{
- // Copy&paste from Verific 3.16_484_32_170630 Netlist.h
- vector<int> sva_prims {
- PRIM_SVA_IMMEDIATE_ASSERT, PRIM_SVA_ASSERT, PRIM_SVA_COVER, PRIM_SVA_ASSUME,
- PRIM_SVA_EXPECT, PRIM_SVA_POSEDGE, PRIM_SVA_NOT, PRIM_SVA_FIRST_MATCH,
- PRIM_SVA_ENDED, PRIM_SVA_MATCHED, PRIM_SVA_CONSECUTIVE_REPEAT,
- PRIM_SVA_NON_CONSECUTIVE_REPEAT, PRIM_SVA_GOTO_REPEAT,
- PRIM_SVA_MATCH_ITEM_TRIGGER, PRIM_SVA_AND, PRIM_SVA_OR, PRIM_SVA_SEQ_AND,
- PRIM_SVA_SEQ_OR, PRIM_SVA_EVENT_OR, PRIM_SVA_OVERLAPPED_IMPLICATION,
- PRIM_SVA_NON_OVERLAPPED_IMPLICATION, PRIM_SVA_OVERLAPPED_FOLLOWED_BY,
- PRIM_SVA_NON_OVERLAPPED_FOLLOWED_BY, PRIM_SVA_INTERSECT, PRIM_SVA_THROUGHOUT,
- PRIM_SVA_WITHIN, PRIM_SVA_AT, PRIM_SVA_DISABLE_IFF, PRIM_SVA_SAMPLED,
- PRIM_SVA_ROSE, PRIM_SVA_FELL, PRIM_SVA_STABLE, PRIM_SVA_PAST,
- PRIM_SVA_MATCH_ITEM_ASSIGN, PRIM_SVA_SEQ_CONCAT, PRIM_SVA_IF,
- PRIM_SVA_RESTRICT, PRIM_SVA_TRIGGERED, PRIM_SVA_STRONG, PRIM_SVA_WEAK,
- PRIM_SVA_NEXTTIME, PRIM_SVA_S_NEXTTIME, PRIM_SVA_ALWAYS, PRIM_SVA_S_ALWAYS,
- PRIM_SVA_S_EVENTUALLY, PRIM_SVA_EVENTUALLY, PRIM_SVA_UNTIL, PRIM_SVA_S_UNTIL,
- PRIM_SVA_UNTIL_WITH, PRIM_SVA_S_UNTIL_WITH, PRIM_SVA_IMPLIES, PRIM_SVA_IFF,
- PRIM_SVA_ACCEPT_ON, PRIM_SVA_REJECT_ON, PRIM_SVA_SYNC_ACCEPT_ON,
- PRIM_SVA_SYNC_REJECT_ON, PRIM_SVA_GLOBAL_CLOCKING_DEF,
- PRIM_SVA_GLOBAL_CLOCKING_REF, PRIM_SVA_IMMEDIATE_ASSUME,
- PRIM_SVA_IMMEDIATE_COVER, OPER_SVA_SAMPLED, OPER_SVA_STABLE
- };
-
- for (int p : sva_prims)
- verific_sva_prims.insert(p);
}
RTLIL::SigBit net_map_at(Net *net)
Instance *inst;
PortRef *pr;
+ if (!mode_nosvapp)
+ {
+ vector<Instance*> asserts, assumes, covers;
+
+ FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
+ {
+ if (inst->Type() == PRIM_SVA_ASSERT)
+ asserts.push_back(inst);
+
+ if (inst->Type() == PRIM_SVA_ASSUME)
+ assumes.push_back(inst);
+
+ if (inst->Type() == PRIM_SVA_COVER)
+ covers.push_back(inst);
+ }
+
+ for (auto inst : asserts)
+ svapp_assert(inst);
+
+ for (auto inst : assumes)
+ svapp_assume(inst);
+
+ for (auto inst : covers)
+ svapp_cover(inst);
+ }
+
FOREACH_PORT_OF_NETLIST(nl, mi, port)
{
if (port->Bus())
}
}
- if (!mode_nosvapp)
- {
- for (auto inst : sva_asserts)
- svapp_assert(this, inst);
-
- for (auto inst : sva_assumes)
- svapp_assume(this, inst);
-
- for (auto inst : sva_covers)
- svapp_cover(this, inst);
- }
-
if (!mode_nosva)
{
for (auto inst : sva_asserts)
struct VerificSvaPP
{
- VerificImporter *importer;
- Module *module;
-
Netlist *netlist;
Instance *root;
bool mode_assert = false;
bool mode_assume = false;
bool mode_cover = false;
+ bool did_something = false;
Instance *net_to_ast_driver(Net *n)
{
if (inst == nullptr)
return nullptr;
- if (!importer->verific_sva_prims.count(inst->Type()))
+ if (!verific_sva_prims.count(inst->Type()))
return nullptr;
if (inst->Type() == PRIM_SVA_PAST)
Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
- Net *impl_to_seq(Instance *inst)
+ Net *rewrite(Instance *inst)
{
if (inst == nullptr)
return nullptr;
if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME) {
- Net *new_net = impl_to_seq(get_ast_input(inst));
+ Net *new_net = rewrite(get_ast_input(inst));
if (new_net) {
inst->Disconnect(inst->View()->GetInput());
inst->Connect(inst->View()->GetInput(), new_net);
}
if (inst->Type() == PRIM_SVA_AT) {
- Net *new_net = impl_to_seq(get_ast_input2(inst));
+ Net *new_net = rewrite(get_ast_input2(inst));
if (new_net) {
inst->Disconnect(inst->View()->GetInput2());
inst->Connect(inst->View()->GetInput2(), new_net);
if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
{
if (mode_cover) {
- Net *new_in1 = impl_to_seq(get_ast_input1(inst));
- Net *new_in2 = impl_to_seq(get_ast_input2(inst));
+ did_something = true;
+ Net *new_in1 = rewrite(get_ast_input1(inst));
+ Net *new_in2 = rewrite(get_ast_input2(inst));
if (!new_in1) new_in1 = inst->GetInput1();
- if (!new_in2) new_in2 = inst->GetInput2();
+ if (!new_in2) new_in1 = inst->GetInput2();
return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
}
+ return nullptr;
}
return nullptr;
void run()
{
- module = importer->module;
netlist = root->Owner();
-
- // impl_to_seq(root);
+ do {
+ did_something = false;
+ rewrite(root);
+ } while (did_something);
}
};
-void svapp_assert(VerificImporter *importer, Instance *inst)
+void svapp_assert(Instance *inst)
{
VerificSvaPP worker;
- worker.importer = importer;
worker.root = inst;
worker.mode_assert = true;
worker.run();
}
-void svapp_assume(VerificImporter *importer, Instance *inst)
+void svapp_assume(Instance *inst)
{
VerificSvaPP worker;
- worker.importer = importer;
worker.root = inst;
worker.mode_assume = true;
worker.run();
}
-void svapp_cover(VerificImporter *importer, Instance *inst)
+void svapp_cover(Instance *inst)
{
VerificSvaPP worker;
- worker.importer = importer;
worker.root = inst;
worker.mode_cover = true;
worker.run();
if (inst == nullptr)
return nullptr;
- if (!importer->verific_sva_prims.count(inst->Type()))
+ if (!verific_sva_prims.count(inst->Type()))
return nullptr;
if (inst->Type() == PRIM_SVA_PAST)
projects / yosys.git / commitdiff