aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2018-06-29 19:21:04 +0200
committerClifford Wolf <clifford@clifford.at>2018-06-29 19:21:04 +0200
commit0404cf61d5f230de70bc6e6e6bf907bf7b112e0d (patch)
tree0b126f66c9bc92a9d71e60ef88c0fdcff5a3191d /frontends/verific
parentebf0f003d3e8d219b396d4c6a3943e1ce54d2879 (diff)
downloadyosys-0404cf61d5f230de70bc6e6e6bf907bf7b112e0d.tar.gz
yosys-0404cf61d5f230de70bc6e6e6bf907bf7b112e0d.tar.bz2
yosys-0404cf61d5f230de70bc6e6e6bf907bf7b112e0d.zip
Add verific support for eventually properties
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'frontends/verific')
-rw-r--r--frontends/verific/verificsva.cc110
1 files changed, 105 insertions, 5 deletions
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 4e440b4ca..9312fd6e6 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -980,7 +980,6 @@ struct VerificSvaImporter
bool mode_assume = false;
bool mode_cover = false;
bool mode_trigger = false;
- bool eventually = false;
Instance *net_to_ast_driver(Net *n)
{
@@ -1487,6 +1486,69 @@ struct VerificSvaImporter
fsm.getFirstAcceptReject(accept_p, reject_p);
}
+ bool eventually_property(Net *&net, SigBit &trig)
+ {
+ if (clocking.cond_net != nullptr)
+ trig = importer->net_map_at(clocking.cond_net);
+ else
+ trig = State::S1;
+
+ Instance *inst = net_to_ast_driver(net);
+
+ if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
+ {
+ if (mode_cover || mode_trigger)
+ parser_error(inst);
+
+ net = inst->GetInput();
+ clocking.cond_net = nullptr;
+
+ return true;
+ }
+
+ if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
+ inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+ {
+ Net *antecedent_net = inst->GetInput1();
+ Net *consequent_net = inst->GetInput2();
+
+ Instance *consequent_inst = net_to_ast_driver(consequent_net);
+
+ if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY) {
+ return false;
+ }
+
+ if (mode_cover || mode_trigger)
+ parser_error(consequent_inst);
+
+ int node;
+
+ log_dump(trig);
+ SvaFsm antecedent_fsm(clocking, trig);
+ node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
+ if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
+ int next_node = antecedent_fsm.createNode();
+ antecedent_fsm.createEdge(node, next_node);
+ node = next_node;
+ }
+ antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
+
+ trig = antecedent_fsm.getAccept();
+ net = consequent_inst->GetInput();
+ clocking.cond_net = nullptr;
+
+ if (verific_verbose) {
+ log(" Eventually Antecedent FSM:\n");
+ antecedent_fsm.dump();
+ log_dump(trig);
+ }
+
+ return true;
+ }
+
+ return false;
+ }
+
void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p)
{
Instance *inst = net_to_ast_driver(net);
@@ -1620,10 +1682,48 @@ struct VerificSvaImporter
}
else
{
- if (mode_assert || mode_assume) {
- parse_property(clocking.body_net, nullptr, &reject_bit);
- } else {
- parse_property(clocking.body_net, &accept_bit, nullptr);
+ Net *net = clocking.body_net;
+ SigBit trig;
+
+ if (eventually_property(net, trig))
+ {
+ SigBit sig_a, sig_en = trig;
+ parse_property(net, &sig_a, nullptr);
+
+ log_dump(trig, sig_a, sig_en);
+
+ // add final FF stage
+
+ SigBit sig_a_q, sig_en_q;
+
+ if (clocking.body_net == nullptr) {
+ sig_a_q = sig_a;
+ sig_en_q = sig_en;
+ } else {
+ sig_a_q = module->addWire(NEW_ID);
+ sig_en_q = module->addWire(NEW_ID);
+ clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
+ clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
+ }
+
+ // generate fair/live cell
+
+ RTLIL::Cell *c = nullptr;
+
+ if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q);
+ if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q);
+
+ importer->import_attributes(c->attributes, root);
+
+ return;
+ }
+ else
+ {
+ if (mode_assert || mode_assume) {
+ parse_property(net, nullptr, &reject_bit);
+ } else {
+ parse_property(net, &accept_bit, nullptr);
+ }
}
}