diff options
| -rw-r--r-- | frontends/verific/verific.cc | 430 |
1 files changed, 320 insertions, 110 deletions
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index dc5448f88..3608655c6 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -92,6 +92,11 @@ string get_full_netlist_name(Netlist *nl) return nl->CellBaseName(); } +struct VerificImporter; +void import_sva_assert(VerificImporter *importer, Instance *inst); +void import_sva_assume(VerificImporter *importer, Instance *inst); +void import_sva_cover(VerificImporter *importer, Instance *inst); + struct VerificImporter { RTLIL::Module *module; @@ -102,9 +107,60 @@ struct VerificImporter bool mode_gates, mode_keep, verbose; + pool<int> verific_sva_prims; + pool<int> verific_psl_prims; + VerificImporter(bool mode_gates, bool mode_keep, bool verbose) : mode_gates(mode_gates), mode_keep(mode_keep), 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); + + // Copy&paste from Verific 3.16_484_32_170630 Netlist.h + vector<int> psl_prims { + OPER_PSLPREV, OPER_PSLNEXTFUNC, PRIM_PSL_ASSERT, PRIM_PSL_ASSUME, + PRIM_PSL_ASSUME_GUARANTEE, PRIM_PSL_RESTRICT, PRIM_PSL_RESTRICT_GUARANTEE, + PRIM_PSL_COVER, PRIM_ENDPOINT, PRIM_ROSE, PRIM_FELL, PRIM_AT, PRIM_ATSTRONG, + PRIM_ABORT, PRIM_PSL_NOT, PRIM_PSL_AND, PRIM_PSL_OR, PRIM_IMPL, PRIM_EQUIV, + PRIM_PSL_X, PRIM_PSL_XSTRONG, PRIM_PSL_G, PRIM_PSL_F, PRIM_PSL_U, PRIM_PSL_W, + PRIM_NEXT, PRIM_NEXTSTRONG, PRIM_ALWAYS, PRIM_NEVER, PRIM_EVENTUALLY, + PRIM_UNTIL, PRIM_UNTIL_, PRIM_UNTILSTRONG, PRIM_UNTILSTRONG_, PRIM_BEFORE, + PRIM_BEFORE_, PRIM_BEFORESTRONG, PRIM_BEFORESTRONG_, PRIM_NEXT_A, + PRIM_NEXT_ASTRONG, PRIM_NEXT_E, PRIM_NEXT_ESTRONG, PRIM_NEXT_EVENT, + PRIM_NEXT_EVENTSTRONG, PRIM_NEXT_EVENT_A, PRIM_NEXT_EVENT_ASTRONG, + PRIM_NEXT_EVENT_E, PRIM_NEXT_EVENT_ESTRONG, PRIM_SEQ_IMPL, PRIM_OSUFFIX_IMPL, + PRIM_SUFFIX_IMPL, PRIM_OSUFFIX_IMPLSTRONG, PRIM_SUFFIX_IMPLSTRONG, PRIM_WITHIN, + PRIM_WITHIN_, PRIM_WITHINSTRONG, PRIM_WITHINSTRONG_, PRIM_WHILENOT, + PRIM_WHILENOT_, PRIM_WHILENOTSTRONG, PRIM_WHILENOTSTRONG_, PRIM_CONCAT, + PRIM_FUSION, PRIM_SEQ_AND_LEN, PRIM_SEQ_AND, PRIM_SEQ_OR, PRIM_CONS_REP, + PRIM_NONCONS_REP, PRIM_GOTO_REP + }; + + for (int p : sva_prims) + verific_psl_prims.insert(p); } RTLIL::SigBit net_map_at(Net *net) @@ -206,59 +262,59 @@ struct VerificImporter return sig; } - bool import_netlist_instance_gates(Instance *inst) + bool import_netlist_instance_gates(Instance *inst, RTLIL::IdString inst_name) { if (inst->Type() == PRIM_AND) { - module->addAndGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + module->addAndGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_NAND) { RTLIL::SigSpec tmp = module->addWire(NEW_ID); module->addAndGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp); - module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetOutput())); + module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_OR) { - module->addOrGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + module->addOrGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_NOR) { RTLIL::SigSpec tmp = module->addWire(NEW_ID); module->addOrGate(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp); - module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetOutput())); + module->addNotGate(inst_name, tmp, net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_XOR) { - module->addXorGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + module->addXorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_XNOR) { - module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + module->addXnorGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_BUF) { - module->addBufGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_INV) { - module->addNotGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + module->addNotGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_MUX) { - module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); + module->addMuxGate(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_TRI) { - module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); + module->addMuxGate(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); return true; } @@ -271,7 +327,7 @@ struct VerificImporter RTLIL::SigSpec tmp2 = module->addWire(NEW_ID); RTLIL::SigSpec tmp3 = module->addWire(NEW_ID); module->addXorGate(NEW_ID, a, b, tmp1); - module->addXorGate(RTLIL::escape_id(inst->Name()), tmp1, c, y); + module->addXorGate(inst_name, tmp1, c, y); module->addAndGate(NEW_ID, tmp1, c, tmp2); module->addAndGate(NEW_ID, a, b, tmp3); module->addOrGate(NEW_ID, tmp2, tmp3, x); @@ -281,15 +337,15 @@ struct VerificImporter if (inst->Type() == PRIM_DFFRS) { if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) - module->addDffGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + module->addDffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); else if (inst->GetSet()->IsGnd()) - module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetReset()), + module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), false); else if (inst->GetReset()->IsGnd()) - module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), + module->addAdffGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), true); else - module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), + module->addDffsrGate(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); return true; } @@ -297,54 +353,54 @@ struct VerificImporter return false; } - bool import_netlist_instance_cells(Instance *inst) + bool import_netlist_instance_cells(Instance *inst, RTLIL::IdString inst_name) { if (inst->Type() == PRIM_AND) { - module->addAnd(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + module->addAnd(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_NAND) { RTLIL::SigSpec tmp = module->addWire(NEW_ID); module->addAnd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp); - module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetOutput())); + module->addNot(inst_name, tmp, net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_OR) { - module->addOr(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + module->addOr(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_NOR) { RTLIL::SigSpec tmp = module->addWire(NEW_ID); module->addOr(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), tmp); - module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetOutput())); + module->addNot(inst_name, tmp, net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_XOR) { - module->addXor(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + module->addXor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_XNOR) { - module->addXnor(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); + module->addXnor(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_INV) { - module->addNot(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + module->addNot(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_MUX) { - module->addMux(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); + module->addMux(inst_name, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); return true; } if (inst->Type() == PRIM_TRI) { - module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); + module->addMux(inst_name, RTLIL::State::Sz, net_map_at(inst->GetInput()), net_map_at(inst->GetControl()), net_map_at(inst->GetOutput())); return true; } @@ -355,22 +411,22 @@ struct VerificImporter if (inst->GetCout()) y.append(net_map_at(inst->GetCout())); module->addAdd(NEW_ID, net_map_at(inst->GetInput1()), net_map_at(inst->GetInput2()), a_plus_b); - module->addAdd(RTLIL::escape_id(inst->Name()), a_plus_b, net_map_at(inst->GetCin()), y); + module->addAdd(inst_name, a_plus_b, net_map_at(inst->GetCin()), y); return true; } if (inst->Type() == PRIM_DFFRS) { if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) - module->addDff(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + module->addDff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); else if (inst->GetSet()->IsGnd()) - module->addAdff(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetReset()), + module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S0); else if (inst->GetReset()->IsGnd()) - module->addAdff(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), + module->addAdff(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()), RTLIL::State::S1); else - module->addDffsr(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), + module->addDffsr(inst_name, net_map_at(inst->GetClock()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); return true; } @@ -378,9 +434,9 @@ struct VerificImporter if (inst->Type() == PRIM_DLATCHRS) { if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd()) - module->addDlatch(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + module->addDlatch(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); else - module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), + module->addDlatchsr(inst_name, net_map_at(inst->GetControl()), net_map_at(inst->GetSet()), net_map_at(inst->GetReset()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); return true; } @@ -396,37 +452,37 @@ struct VerificImporter if (inst->GetCout() != NULL) out.append(net_map_at(inst->GetCout())); if (inst->GetCin()->IsGnd()) { - module->addAdd(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED); + module->addAdd(inst_name, IN1, IN2, out, SIGNED); } else { RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out)); module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED); - module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map_at(inst->GetCin()), out, false); + module->addAdd(inst_name, tmp, net_map_at(inst->GetCin()), out, false); } return true; } if (inst->Type() == OPER_MULTIPLIER) { - module->addMul(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + module->addMul(inst_name, IN1, IN2, OUT, SIGNED); return true; } if (inst->Type() == OPER_DIVIDER) { - module->addDiv(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + module->addDiv(inst_name, IN1, IN2, OUT, SIGNED); return true; } if (inst->Type() == OPER_MODULO) { - module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + module->addMod(inst_name, IN1, IN2, OUT, SIGNED); return true; } if (inst->Type() == OPER_REMAINDER) { - module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + module->addMod(inst_name, IN1, IN2, OUT, SIGNED); return true; } if (inst->Type() == OPER_SHIFT_LEFT) { - module->addShl(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false); + module->addShl(inst_name, IN1, IN2, OUT, false); return true; } @@ -436,7 +492,7 @@ struct VerificImporter for (unsigned i = 1; i < inst->OutputSize(); i++) { vec.append(RTLIL::State::S0); } - module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false); + module->addShl(inst_name, vec, IN, OUT, false); return true; } @@ -446,7 +502,7 @@ struct VerificImporter for (unsigned i = 1; i < inst->OutputSize(); i++) { vec.append(RTLIL::State::S0); } - module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false); + module->addShl(inst_name, vec, IN, OUT, false); return true; } @@ -454,102 +510,102 @@ struct VerificImporter Net *net_cin = inst->GetCin(); Net *net_a_msb = inst->GetInput1Bit(0); if (net_cin->IsGnd()) - module->addShr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false); + module->addShr(inst_name, IN1, IN2, OUT, false); else if (net_cin == net_a_msb) - module->addSshr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, true); + module->addSshr(inst_name, IN1, IN2, OUT, true); else log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name()); return true; } if (inst->Type() == OPER_REDUCE_AND) { - module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map_at(inst->GetOutput()), SIGNED); + module->addReduceAnd(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); return true; } if (inst->Type() == OPER_REDUCE_OR) { - module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map_at(inst->GetOutput()), SIGNED); + module->addReduceOr(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); return true; } if (inst->Type() == OPER_REDUCE_XOR) { - module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map_at(inst->GetOutput()), SIGNED); + module->addReduceXor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); return true; } if (inst->Type() == OPER_REDUCE_XNOR) { - module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map_at(inst->GetOutput()), SIGNED); + module->addReduceXnor(inst_name, IN, net_map_at(inst->GetOutput()), SIGNED); return true; } if (inst->Type() == OPER_LESSTHAN) { Net *net_cin = inst->GetCin(); if (net_cin->IsGnd()) - module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); + module->addLt(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); else if (net_cin->IsPwr()) - module->addLe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); + module->addLe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); else log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name()); return true; } if (inst->Type() == OPER_WIDE_AND) { - module->addAnd(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + module->addAnd(inst_name, IN1, IN2, OUT, SIGNED); return true; } if (inst->Type() == OPER_WIDE_OR) { - module->addOr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + module->addOr(inst_name, IN1, IN2, OUT, SIGNED); return true; } if (inst->Type() == OPER_WIDE_XOR) { - module->addXor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + module->addXor(inst_name, IN1, IN2, OUT, SIGNED); return true; } if (inst->Type() == OPER_WIDE_XNOR) { - module->addXnor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + module->addXnor(inst_name, IN1, IN2, OUT, SIGNED); return true; } if (inst->Type() == OPER_WIDE_BUF) { - module->addPos(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED); + module->addPos(inst_name, IN, OUT, SIGNED); return true; } if (inst->Type() == OPER_WIDE_INV) { - module->addNot(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED); + module->addNot(inst_name, IN, OUT, SIGNED); return true; } if (inst->Type() == OPER_MINUS) { - module->addSub(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED); + module->addSub(inst_name, IN1, IN2, OUT, SIGNED); return true; } if (inst->Type() == OPER_UMINUS) { - module->addNeg(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED); + module->addNeg(inst_name, IN, OUT, SIGNED); return true; } if (inst->Type() == OPER_EQUAL) { - module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); + module->addEq(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); return true; } if (inst->Type() == OPER_NEQUAL) { - module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); + module->addNe(inst_name, IN1, IN2, net_map_at(inst->GetOutput()), SIGNED); return true; } if (inst->Type() == OPER_WIDE_MUX) { - module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map_at(inst->GetControl()), OUT); + module->addMux(inst_name, IN1, IN2, net_map_at(inst->GetControl()), OUT); return true; } if (inst->Type() == OPER_WIDE_TRI) { - module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT); + module->addMux(inst_name, RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map_at(inst->GetControl()), OUT); return true; } @@ -557,9 +613,9 @@ struct VerificImporter RTLIL::SigSpec sig_set = operatorInport(inst, "set"); RTLIL::SigSpec sig_reset = operatorInport(inst, "reset"); if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool()) - module->addDff(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), IN, OUT); + module->addDff(inst_name, net_map_at(inst->GetClock()), IN, OUT); else - module->addDffsr(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT); + module->addDffsr(inst_name, net_map_at(inst->GetClock()), sig_set, sig_reset, IN, OUT); return true; } @@ -757,10 +813,11 @@ struct VerificImporter if (net->Bus()) continue; + RTLIL::IdString wire_name = module->uniquify(net->IsUserDeclared() ? RTLIL::escape_id(net->Name()) : NEW_ID); + if (verbose) - log(" importing net %s.\n", net->Name()); + log(" importing net %s as %s.\n", net->Name(), log_id(wire_name)); - RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name())); RTLIL::Wire *wire = module->addWire(wire_name); import_attributes(wire->attributes, net); @@ -877,58 +934,30 @@ struct VerificImporter for (auto net : anyseq_nets) module->connect(net_map_at(net), module->Anyseq(NEW_ID)); - FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) - { - if (inst->Type() == PRIM_SVA_POSEDGE) { - Net *in_net = inst->GetInput(); - Net *out_net = inst->GetOutput(); - sva_posedge_map[out_net] = in_net; - continue; - } - } + pool<Instance*, hash_ptr_ops> sva_asserts; + pool<Instance*, hash_ptr_ops> sva_assumes; + pool<Instance*, hash_ptr_ops> sva_covers; FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst) { - if (inst->Type() == PRIM_SVA_POSEDGE) - continue; + RTLIL::IdString inst_name = module->uniquify(inst->IsUserDeclared() ? RTLIL::escape_id(inst->Name()) : NEW_ID); if (verbose) - log(" importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name()); - - - if (inst->Type() == PRIM_SVA_AT) - { - Net *in1 = inst->GetInput1(); - Net *in2 = inst->GetInput2(); - Net *out = inst->GetOutput(); + log(" importing cell %s (%s) as %s.\n", inst->Name(), inst->View()->Owner()->Name(), log_id(inst_name)); - if (sva_posedge_map.count(in2)) - std::swap(in1, in2); - - log_assert(sva_posedge_map.count(in1)); - Net *clk = sva_posedge_map.at(in1); - - SigBit outsig = net_map_at(out); - log_assert(outsig.wire && GetSize(outsig.wire) == 1); - outsig.wire->attributes["\\init"] = Const(1, 1); - - module->addDff(NEW_ID, net_map_at(clk), net_map_at(in2), net_map_at(out)); - continue; - } - - if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_ASSERT) { + if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT) { Net *in = inst->GetInput(); module->addAssert(NEW_ID, net_map_at(in), State::S1); continue; } - if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_ASSUME) { + if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME) { Net *in = inst->GetInput(); module->addAssume(NEW_ID, net_map_at(in), State::S1); continue; } - if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_COVER) { + if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER) { Net *in = inst->GetInput(); module->addCover(NEW_ID, net_map_at(in), State::S1); continue; @@ -945,7 +974,7 @@ struct VerificImporter } if (inst->Type() == PRIM_BUF) { - module->addBufGate(RTLIL::escape_id(inst->Name()), net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); + module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput())); continue; } @@ -968,7 +997,7 @@ struct VerificImporter RTLIL::SigSpec addr = operatorInput1(inst); RTLIL::SigSpec data = operatorOutput(inst); - RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memrd"); + RTLIL::Cell *cell = module->addCell(inst_name, "$memrd"); cell->parameters["\\MEMID"] = memory->name.str(); cell->parameters["\\CLK_ENABLE"] = false; cell->parameters["\\CLK_POLARITY"] = true; @@ -991,7 +1020,7 @@ struct VerificImporter RTLIL::SigSpec addr = operatorInput1(inst); RTLIL::SigSpec data = operatorInput2(inst); - RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memwr"); + RTLIL::Cell *cell = module->addCell(inst_name, "$memwr"); cell->parameters["\\MEMID"] = memory->name.str(); cell->parameters["\\CLK_ENABLE"] = false; cell->parameters["\\CLK_POLARITY"] = true; @@ -1011,27 +1040,47 @@ struct VerificImporter } if (!mode_gates) { - if (import_netlist_instance_cells(inst)) + if (import_netlist_instance_cells(inst, inst_name)) continue; if (inst->IsOperator()) log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name()); } else { - if (import_netlist_instance_gates(inst)) + if (import_netlist_instance_gates(inst, inst_name)) continue; } + if (inst->Type() == PRIM_SVA_ASSERT) + sva_asserts.insert(inst); + + if (inst->Type() == PRIM_SVA_ASSUME) + sva_asserts.insert(inst); + + if (inst->Type() == PRIM_SVA_COVER) + sva_covers.insert(inst); + + if (!mode_keep && (verific_sva_prims.count(inst->Type()) || verific_psl_prims.count(inst->Type()))) { + if (verbose) + log(" skipping SVA/PSL cell in non k-mode\n"); + continue; + } + if (inst->IsPrimitive()) { if (!mode_keep) log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); - log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); + + if (!verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type())) + log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name()); } nl_todo.insert(inst->View()); - RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), inst->IsOperator() ? + RTLIL::Cell *cell = module->addCell(inst_name, inst->IsOperator() ? std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name())); + if (inst->IsPrimitive() && mode_keep) + cell->attributes["\\keep"] = 1; + dict<IdString, vector<SigBit>> cell_port_conns; if (verbose) @@ -1066,9 +1115,170 @@ struct VerificImporter cell->setPort(it.first, it.second); } } + + for (auto inst : sva_asserts) + import_sva_assert(this, inst); + + for (auto inst : sva_assumes) + import_sva_assume(this, inst); + + for (auto inst : sva_covers) + import_sva_cover(this, inst); } }; +struct VerificSvaImporter +{ + VerificImporter *importer; + Module *module; + + Netlist *netlist; + Instance *root; + + SigBit clock = State::Sx; + bool clock_posedge = false; + + SigBit disable_iff = State::S0; + + bool import_sva_disable_hiactive = true; + int import_sva_init_disable_steps = 0; + + bool mode_assert = false; + bool mode_assume = false; + bool mode_cover = false; + + Instance *net_to_ast_driver(Net *n) + { + if (n == nullptr) + return nullptr; + + if (n->IsMultipleDriven()) + return nullptr; + + Instance *inst = n->Driver(); + + if (inst == nullptr) + return nullptr; + + if (!importer->verific_sva_prims.count(inst->Type()) && + !importer->verific_psl_prims.count(inst->Type())) + return nullptr; + + return inst; + } + + Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); } + Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); } + Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); } + 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()); } + + SigBit parse_sequence(Net *n) + { + Instance *inst = net_to_ast_driver(n); + + if (inst == nullptr) + return importer->net_map_at(n); + + if (!importer->mode_keep) + log_error("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name()); + log_warning("Unsupported Verific SVA primitive %s of type %s.\n", inst->Name(), inst->View()->Owner()->Name()); + + return importer->net_map_at(n); + } + + void run() + { + module = importer->module; + netlist = root->Owner(); + + // parse SVA property clock event + + Instance *at_node = get_ast_input(root); + log_assert(at_node && at_node->Type() == PRIM_SVA_AT); + + Instance *clock_node = get_ast_input1(at_node); + log_assert(clock_node && (clock_node->Type() == PRIM_SVA_POSEDGE || clock_node->Type() == PRIM_SVA_POSEDGE)); + + clock = importer->net_map_at(clock_node->GetInput()); + clock_posedge = (clock_node->Type() == PRIM_SVA_POSEDGE); + + import_sva_init_disable_steps = 1; + + // parse disable_iff expression + + Net *sequence_net = at_node->GetInput2(); + Instance *sequence_node = net_to_ast_driver(sequence_net); + + if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { + disable_iff = importer->net_map_at(sequence_node->GetInput1()); + sequence_net = sequence_node->GetInput2(); + } + + // parse SVA sequence into trigger signal + + SigBit sig_a_d = parse_sequence(sequence_net); + Wire *sig_a_q = module->addWire(NEW_ID); + sig_a_q->attributes["\\init"] = Const(import_sva_disable_hiactive ? State::S1 : State::S0, 1); + module->addDff(NEW_ID, clock, sig_a_d, sig_a_q, clock_posedge); + + // generate properly delayed enable signal + + SigBit sig_en = State::S1; + + if (disable_iff != State::S0) + sig_en = module->Mux(NEW_ID, sig_en, State::S0, disable_iff); + + for (int i = 0; i < import_sva_init_disable_steps; i++) + { + Wire *new_en = module->addWire(NEW_ID); + new_en->attributes["\\init"] = Const(0, 1); + + module->addDff(NEW_ID, clock, sig_en, new_en, clock_posedge); + + if (disable_iff != State::S0 && i+1 < import_sva_init_disable_steps) + sig_en = module->Mux(NEW_ID, new_en, State::S0, disable_iff); + else + sig_en = new_en; + } + + // generate assert/assume/cover cell + + RTLIL::IdString root_name = module->uniquify(root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); + + if (mode_assert) module->addAssert(root_name, sig_a_q, sig_en); + if (mode_assume) module->addAssume(root_name, sig_a_q, sig_en); + if (mode_cover) module->addCover(root_name, sig_a_q, sig_en); + } +}; + +void import_sva_assert(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_assert = true; + worker.run(); +} + +void import_sva_assume(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_assume = true; + worker.run(); +} + +void import_sva_cover(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_cover = true; + worker.run(); +} + struct VerificExtNets { int portname_cnt = 0; @@ -1206,7 +1416,7 @@ struct VerificPass : public Pass { #ifdef YOSYS_ENABLE_VERIFIC virtual void execute(std::vector<std::string> args, RTLIL::Design *design) { - log_header(design, "Executing VERIFIC (loading Verilog and VHDL designs using Verific).\n"); + log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n"); Message::SetConsoleOutput(0); Message::RegisterCallBackMsg(msg_func); |