From 480e8e676a41559138a690759e90cec2ae60bc28 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sun, 4 Mar 2018 19:29:26 +0100 Subject: [PATCH] Add proper SVA seq.triggered support Signed-off-by: Clifford Wolf --- frontends/verific/verific.cc | 7 ++ frontends/verific/verific.h | 12 +++- frontends/verific/verificsva.cc | 120 ++++++++++++++++++++++---------- 3 files changed, 102 insertions(+), 37 deletions(-) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 2e669dc45..9db5f6a02 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1001,6 +1001,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se pool sva_asserts; pool sva_assumes; pool sva_covers; + pool sva_triggers; pool past_ffs; @@ -1106,6 +1107,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_IMMEDIATE_COVER) sva_covers.insert(inst); + if (inst->Type() == PRIM_SVA_TRIGGERED) + sva_triggers.insert(inst); + if (inst->Type() == OPER_SVA_STABLE) { VerificClocking clocking(this, inst->GetInput2Bit(0)); @@ -1264,6 +1268,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se for (auto inst : sva_covers) import_sva_cover(this, inst); + for (auto inst : sva_triggers) + import_sva_trigger(this, inst); + merge_past_ffs(past_ffs); } } diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index 63d81fc3e..5f927d5cf 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -45,6 +45,16 @@ struct VerificClocking { RTLIL::Cell *addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value = Const()); RTLIL::Cell *addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value); RTLIL::Cell *addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q); + + bool property_matches_sequence(const VerificClocking &seq) const { + if (clock_net != seq.clock_net) + return false; + if (enable_net != seq.enable_net) + return false; + if (posedge != seq.posedge) + return false; + return true; + } }; struct VerificImporter @@ -78,10 +88,10 @@ struct VerificImporter void import_netlist(RTLIL::Design *design, Verific::Netlist *nl, std::set &nl_todo); }; - void import_sva_assert(VerificImporter *importer, Verific::Instance *inst); void import_sva_assume(VerificImporter *importer, Verific::Instance *inst); void import_sva_cover(VerificImporter *importer, Verific::Instance *inst); +void import_sva_trigger(VerificImporter *importer, Verific::Instance *inst); YOSYS_NAMESPACE_END diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 78f4484c7..ecff42679 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -24,9 +24,7 @@ // seq |-> seq // seq |-> not seq // seq |-> seq until expr -// seq |-> seq until seq.triggered // seq |-> not seq until expr -// seq |-> not seq until seq.triggered // // Currently supported sequence operators: // seq ##[N:M] seq @@ -42,6 +40,9 @@ // [*N:M] includes [*N], [*], [+] // [=N:M], [->N:M] includes [=N], [->N] // +// Expressions can be any boolean expression, including expressions +// that use $past, $rose, $fell, $stable, and sequence.triggered. +// // ------------------------------------------------------- // // SVA Properties Simplified Syntax (essentially a todo-list): @@ -772,6 +773,7 @@ struct VerificSvaImporter bool mode_assert = false; bool mode_assume = false; bool mode_cover = false; + bool mode_trigger = false; bool eventually = false; Instance *net_to_ast_driver(Net *n) @@ -791,7 +793,8 @@ struct VerificSvaImporter return nullptr; if (inst->Type() == PRIM_SVA_ROSE || inst->Type() == PRIM_SVA_FELL || - inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || inst->Type() == PRIM_SVA_PAST) + inst->Type() == PRIM_SVA_STABLE || inst->Type() == OPER_SVA_STABLE || + inst->Type() == PRIM_SVA_PAST || inst->Type() == PRIM_SVA_TRIGGERED) return nullptr; return inst; @@ -819,10 +822,12 @@ struct VerificSvaImporter [[noreturn]] void parser_error(std::string errmsg, linefile_type loc) { - if (!importer->mode_keep) - log_error("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc)); - log_warning("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc)); - throw ParserErrorException(); + parser_error(stringf("%s at %s:%d.\n", errmsg.c_str(), LineFile::GetFileName(loc), LineFile::GetLineNo(loc))); + } + + [[noreturn]] void parser_error(std::string errmsg, Instance *inst) + { + parser_error(stringf("%s at %s (%s)", errmsg.c_str(), inst->View()->Owner()->Name(), inst->Name()), inst->Linefile()); } [[noreturn]] void parser_error(Instance *inst) @@ -841,6 +846,14 @@ struct VerificSvaImporter return node; } + if (inst->Type() == PRIM_SVA_AT) + { + VerificClocking new_clocking(importer, net); + if (!clocking.property_matches_sequence(new_clocking)) + parser_error("Mixed clocking is currently not supported", inst); + return parse_sequence(fsm, start_node, new_clocking.body_net); + } + if (inst->Type() == PRIM_SVA_SEQ_CONCAT) { const char *sva_low_s = inst->GetAttValue("sva:low"); @@ -1003,11 +1016,8 @@ struct VerificSvaImporter consequent_net = consequent_inst->GetInput1(); consequent_inst = net_to_ast_driver(consequent_net); - if (until_inst != nullptr) { - if (until_inst->Type() != PRIM_SVA_TRIGGERED) - parser_error("Currently only boolean expressions or sequence.triggered is allowed in SVA_UNTIL condition", until_inst->Linefile()); - until_net = until_inst->GetInput(); - } + if (until_inst != nullptr) + parser_error("Currently only expressions are allowed in SVA_UNTIL condition", until_inst); SvaFsm until_fsm(clocking); node = parse_sequence(until_fsm, until_fsm.startNode, until_net); @@ -1043,7 +1053,7 @@ struct VerificSvaImporter consequent_fsm.createLink(node, consequent_fsm.acceptNode); SigBit prop_okay; - if (mode_cover) { + if (mode_cover || mode_trigger) { prop_okay = consequent_not ? consequent_fsm.getReject() : consequent_fsm.getAccept(); } else { SigBit consequent_match = consequent_not ? consequent_fsm.getAccept() : consequent_fsm.getReject(); @@ -1058,13 +1068,19 @@ struct VerificSvaImporter return prop_okay; } else - if (inst->Type() == PRIM_SVA_NOT || mode_cover) + if (inst->Type() == PRIM_SVA_NOT) { SvaFsm fsm(clocking); - int node = parse_sequence(fsm, fsm.startNode, mode_cover ? net : inst->GetInput()); + int node = parse_sequence(fsm, fsm.startNode, inst->GetInput()); fsm.createLink(node, fsm.acceptNode); - SigBit accept = fsm.getAccept(); - SigBit prop_okay = module->Not(NEW_ID, accept); + + SigBit prop_okay; + if (mode_cover || mode_trigger) { + prop_okay = fsm.getReject(); + } else { + SigBit accept = fsm.getAccept(); + prop_okay = module->Not(NEW_ID, accept); + } if (verific_verbose) { log(" Sequence FSM:\n"); @@ -1075,8 +1091,24 @@ struct VerificSvaImporter } else { - // Handle unsupported primitives - parser_error(inst); + SvaFsm fsm(clocking); + int node = parse_sequence(fsm, fsm.startNode, net); + fsm.createLink(node, fsm.acceptNode); + + SigBit prop_okay; + if (mode_cover || mode_trigger) { + prop_okay = fsm.getAccept(); + } else { + SigBit accept = fsm.getReject(); + prop_okay = module->Not(NEW_ID, accept); + } + + if (verific_verbose) { + log(" Sequence FSM:\n"); + fsm.dump(); + } + + return prop_okay; } } @@ -1096,34 +1128,41 @@ struct VerificSvaImporter clocking = VerificClocking(importer, root->GetInput()); if (clocking.body_net == nullptr) - parser_error(stringf("Failed to parse SVA clocking at %s (%s) at %s:%d.", root->Name(), root->View()->Owner()->Name(), - LineFile::GetFileName(root->Linefile()), LineFile::GetLineNo(root->Linefile()))); + parser_error(stringf("Failed to parse SVA clocking"), root); // parse SVA sequence into trigger signal Net *net = clocking.body_net; SigBit prop_okay = parse_property(net); - // add final FF stage + if (mode_trigger) + { + module->connect(importer->net_map_at(root->GetOutput()), prop_okay); + } + else + { + // add final FF stage - SigBit prop_okay_q = module->addWire(NEW_ID); - clocking.addDff(NEW_ID, prop_okay, prop_okay_q, Const(mode_cover ? 0 : 1, 1)); + SigBit prop_okay_q = module->addWire(NEW_ID); + clocking.addDff(NEW_ID, prop_okay, prop_okay_q, Const(mode_cover ? 0 : 1, 1)); - // generate assert/assume/cover cell + // generate assert/assume/cover cell - RTLIL::Cell *c = nullptr; + RTLIL::Cell *c = nullptr; - if (eventually) { - parser_error("No support for eventually in Verific SVA bindings yet.\n"); - // if (mode_assert) c = module->addLive(root_name, prop_okay_q, prop_start_q); - // if (mode_assume) c = module->addFair(root_name, prop_okay_q, prop_start_q); - } else { - if (mode_assert) c = module->addAssert(root_name, prop_okay_q, State::S1); - if (mode_assume) c = module->addAssume(root_name, prop_okay_q, State::S1); - if (mode_cover) c = module->addCover(root_name, prop_okay_q, State::S1); - } + if (eventually) { + parser_error("No support for eventually in Verific SVA bindings yet", root); + // if (mode_assert) c = module->addLive(root_name, prop_okay_q, prop_start_q); + // if (mode_assume) c = module->addFair(root_name, prop_okay_q, prop_start_q); + } else { + if (mode_assert) c = module->addAssert(root_name, prop_okay_q, State::S1); + if (mode_assume) c = module->addAssume(root_name, prop_okay_q, State::S1); + if (mode_cover) c = module->addCover(root_name, prop_okay_q, State::S1); + } - importer->import_attributes(c->attributes, root); + if (c != nullptr) + importer->import_attributes(c->attributes, root); + } } catch (ParserErrorException) { @@ -1158,4 +1197,13 @@ void import_sva_cover(VerificImporter *importer, Instance *inst) worker.import(); } +void import_sva_trigger(VerificImporter *importer, Instance *inst) +{ + VerificSvaImporter worker; + worker.importer = importer; + worker.root = inst; + worker.mode_trigger = true; + worker.import(); +} + YOSYS_NAMESPACE_END -- 2.30.2