From 25e33d7ab8ebeb96d6a7fb842e33f35770367587 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Tue, 27 Feb 2018 20:33:15 +0100 Subject: [PATCH] Major redesign of Verific SVA importer Signed-off-by: Clifford Wolf --- frontends/verific/verificsva.cc | 578 +++++++++++++++++++++++++++++++- tests/sva/sva_range.sv | 2 +- 2 files changed, 574 insertions(+), 6 deletions(-) diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 94443cd3e..ceaca287d 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -24,7 +24,6 @@ // not prop // prop or prop // prop and prop -// seq |-> prop // seq |=> prop // if (expr) prop [else prop] // prop until prop @@ -35,7 +34,6 @@ // // seq: // expr -// expr ##N seq // expr ##[N:M] seq // seq or seq // seq and seq @@ -43,12 +41,24 @@ // first_match (seq) // expr throughout seq // seq within seq -// seq [*N] // seq [*N:M] -// expr [=N] // expr [=N:M] -// expr [->N] // expr [->N:M] +// +// Notes: +// |=> is a placeholder for |-> and |=> +// "until" is a placeholder for all until operators +// ##[N:M], [*N:M], [=N:M], [->N:M] includes ##N, [*N], [=N], [->N] +// +// Currently supported property styles: +// not seq +// seq |=> seq +// seq |=> seq until seq +// +// Currently supported sequence operators: +// ##[N:M] +// [*N:M] +// throughout #include "kernel/yosys.h" @@ -60,6 +70,316 @@ USING_YOSYS_NAMESPACE using namespace Verific; #endif +PRIVATE_NAMESPACE_BEGIN + +struct SvaFsmNode +{ + vector> edges, links; +}; + +struct SvaFsm +{ + Module *module; + SigBit clock; + bool clockpol; + + SigBit trigger_sig = State::S1, disable_sig; + SigBit accept_sig = State::Sz, reject_sig = State::Sz; + SigBit throughout_sig = State::S1; + bool materialized = false; + + vector disable_stack; + vector throughout_stack; + + int startNode, acceptNode, rejectNode; + vector nodes; + + SvaFsm(Module *mod, SigBit clk, bool clkpol, SigBit dis = State::S0, SigBit trig = State::S1) + { + module = mod; + clock = clk; + clockpol = clkpol; + disable_sig = dis; + trigger_sig = trig; + + startNode = createNode(); + acceptNode = createNode(); + rejectNode = createNode(); + } + + void pushDisable(SigBit sig) + { + log_assert(!materialized); + + disable_stack.push_back(disable_sig); + + if (disable_sig == State::S0) + disable_sig = sig; + else + disable_sig = module->Or(NEW_ID, disable_sig, sig); + } + + void popDisable() + { + log_assert(!materialized); + log_assert(!disable_stack.empty()); + + disable_sig = disable_stack.back(); + disable_stack.pop_back(); + } + + void pushThroughout(SigBit sig) + { + log_assert(!materialized); + + throughout_stack.push_back(throughout_sig); + + if (throughout_sig == State::S1) + throughout_sig = sig; + else + throughout_sig = module->And(NEW_ID, throughout_sig, sig); + } + + void popThroughout() + { + log_assert(!materialized); + log_assert(!throughout_stack.empty()); + + throughout_sig = throughout_stack.back(); + throughout_stack.pop_back(); + } + + SigBit getAccept() + { + if (accept_sig != State::Sz) + return accept_sig; + + log_assert(!materialized); + accept_sig = module->addWire(NEW_ID); + return accept_sig; + } + + SigBit getReject() + { + if (reject_sig != State::Sz) + return reject_sig; + + log_assert(!materialized); + reject_sig = module->addWire(NEW_ID); + return reject_sig; + } + + int createNode() + { + log_assert(!materialized); + + int idx = GetSize(nodes); + nodes.push_back(SvaFsmNode()); + return idx; + } + + void createEdge(int from_node, int to_node, SigBit ctrl = State::S1) + { + log_assert(!materialized); + log_assert(0 <= from_node && from_node < GetSize(nodes)); + log_assert(0 <= to_node && to_node < GetSize(nodes)); + + if (throughout_sig != State::S1) { + if (ctrl != State::S1) + ctrl = module->And(NEW_ID, throughout_sig, ctrl); + else + ctrl = throughout_sig; + } + + nodes[from_node].edges.push_back(make_pair(to_node, ctrl)); + } + + void createLink(int from_node, int to_node, SigBit ctrl = State::S1) + { + log_assert(!materialized); + log_assert(0 <= from_node && from_node < GetSize(nodes)); + log_assert(0 <= to_node && to_node < GetSize(nodes)); + + if (throughout_sig != State::S1) { + if (ctrl != State::S1) + ctrl = module->And(NEW_ID, throughout_sig, ctrl); + else + ctrl = throughout_sig; + } + + nodes[from_node].links.push_back(make_pair(to_node, ctrl)); + } + + void make_link_order(vector &order, int node, int min) + { + order[node] = std::max(order[node], min); + for (auto &it : nodes[node].links) + make_link_order(order, it.first, order[node]+1); + } + + void materialize_ndfsm() + { + log_assert(!materialized); + materialized = true; + + vector next_state_sig(GetSize(nodes)); + vector state_sig(GetSize(nodes)); + + // Create state FFs + + { + SigBit not_disable = State::S1; + + if (disable_sig != State::S0) + not_disable = module->Not(NEW_ID, disable_sig); + + for (int i = 0; i < GetSize(nodes); i++) + { + next_state_sig[i] = module->addWire(NEW_ID); + + Wire *w = module->addWire(NEW_ID); + w->attributes["\\init"] = Const(0, 1); + state_sig[i] = w; + + module->addDff(NEW_ID, clock, next_state_sig[i], state_sig[i], clockpol); + + if (i == startNode) + state_sig[i] = module->Or(NEW_ID, state_sig[i], trigger_sig); + + if (disable_sig != State::S0) + state_sig[i] = module->And(NEW_ID, state_sig[i], not_disable); + } + } + + // Follow Links + + { + vector node_order(GetSize(nodes)); + vector> order_to_nodes; + + for (int i = 0; i < GetSize(nodes); i++) + make_link_order(node_order, i, 0); + + for (int i = 0; i < GetSize(nodes); i++) { + if (node_order[i] >= GetSize(order_to_nodes)) + order_to_nodes.resize(node_order[i]+1); + order_to_nodes[node_order[i]].push_back(i); + } + + for (int order = 0; order < GetSize(order_to_nodes); order++) + for (int node : order_to_nodes[order]) + { + for (auto &it : nodes[node].links) + { + int target = it.first; + SigBit ctrl = state_sig[node]; + + if (it.second != State::S1) + ctrl = module->And(NEW_ID, ctrl, it.second); + + state_sig[target] = module->Or(NEW_ID, state_sig[target], ctrl); + } + } + } + + // Construct activations + + { + vector activate_sig(GetSize(nodes)); + vector activate_bit(GetSize(nodes)); + + for (int i = 0; i < GetSize(nodes); i++) { + for (auto &it : nodes[i].edges) + activate_sig[it.first].append(module->And(NEW_ID, state_sig[i], it.second)); + } + + for (int i = 0; i < GetSize(nodes); i++) { + if (GetSize(activate_sig[i]) == 0) + activate_bit[i] = State::S0; + else if (GetSize(activate_sig[i]) == 1) + activate_bit[i] = activate_sig[i]; + else + activate_bit[i] = module->ReduceOr(NEW_ID, activate_sig[i]); + } + + if (activate_bit[rejectNode] != State::S0) + { + SigBit not_rej = module->Not(NEW_ID, next_state_sig[rejectNode]); + for (int i = 0; i < GetSize(nodes); i++) + if (i != rejectNode && activate_bit[i] != State::S0) + activate_bit[i] = module->And(NEW_ID, activate_bit[i], not_rej); + activate_bit[rejectNode] = State::S0; + } + + for (int i = 0; i < GetSize(nodes); i++) { + module->connect(next_state_sig[i], activate_bit[i]); + } + } + + // Construct output signals + + if (accept_sig != State::Sz) { + module->connect(accept_sig, state_sig[acceptNode]); + } + + if (reject_sig != State::Sz) + { + SigBit fsm_active = module->ReduceOr(NEW_ID, state_sig); + SigBit fsm_next_active = module->ReduceOr(NEW_ID, next_state_sig); + module->addEq(NEW_ID, {state_sig[acceptNode], fsm_next_active, fsm_active}, SigSpec(1, 3), reject_sig); + } + } + + void materialize_dfsm() + { + // FIXME + log_abort(); + } + + bool is_linear() + { + for (int i = 0; i < GetSize(nodes); i++) + if (GetSize(nodes[i].edges) + GetSize(nodes[i].links) > 1) + return false; + return true; + } + + void dump() + { + log("-----------\n"); + for (int i = 0; i < GetSize(nodes); i++) + { + log("node %d:\n", i); + + if (i == startNode) + log(" startNode\n"); + + if (i == rejectNode) + log(" rejectNode\n"); + + if (i == acceptNode) + log(" acceptNode\n"); + + for (auto &it : nodes[i].edges) { + if (it.second != State::S1) + log(" egde %s -> %d\n", log_signal(it.second), it.first); + else + log(" egde -> %d\n", it.first); + } + + for (auto &it : nodes[i].links) { + if (it.second != State::S1) + log(" link %s -> %d\n", log_signal(it.second), it.first); + else + log(" link -> %d\n", it.first); + } + } + log("-----------\n"); + } +}; + +PRIVATE_NAMESPACE_END + YOSYS_NAMESPACE_BEGIN pool verific_sva_prims = { @@ -254,6 +574,253 @@ struct VerificSvaImporter // ---------------------------------------------------------- // SVA Importer + int parse_sequence(SvaFsm *fsm, int start_node, Net *net) + { + Instance *inst = net_to_ast_driver(net); + + if (inst == nullptr) { + int node = fsm->createNode(); + fsm->createLink(start_node, node, importer->net_map_at(net)); + return node; + } + + if (inst->Type() == PRIM_SVA_SEQ_CONCAT) + { + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); + + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + bool sva_inf = !strcmp(sva_high_s, "$"); + + int node = parse_sequence(fsm, start_node, inst->GetInput1()); + + for (int i = 0; i < sva_low; i++) { + int next_node = fsm->createNode(); + fsm->createEdge(node, next_node); + node = next_node; + } + + if (sva_inf) + { + fsm->createEdge(node, node); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + int next_node = fsm->createNode(); + fsm->createEdge(node, next_node); + fsm->createLink(node, next_node); + node = next_node; + } + } + + node = parse_sequence(fsm, node, inst->GetInput2()); + + return node; + } + + if (inst->Type() == PRIM_SVA_CONSECUTIVE_REPEAT) + { + const char *sva_low_s = inst->GetAttValue("sva:low"); + const char *sva_high_s = inst->GetAttValue("sva:high"); + + int sva_low = atoi(sva_low_s); + int sva_high = atoi(sva_high_s); + bool sva_inf = !strcmp(sva_high_s, "$"); + + int node = parse_sequence(fsm, start_node, inst->GetInput()); + + for (int i = 1; i < sva_low; i++) + { + int next_node = fsm->createNode(); + fsm->createEdge(node, next_node); + node = parse_sequence(fsm, next_node, inst->GetInput()); + } + + if (sva_inf) + { + int next_node = fsm->createNode(); + fsm->createEdge(node, next_node); + next_node = parse_sequence(fsm, next_node, inst->GetInput()); + fsm->createLink(next_node, node); + } + else + { + for (int i = sva_low; i < sva_high; i++) + { + int next_node = fsm->createNode(); + fsm->createEdge(node, next_node); + next_node = parse_sequence(fsm, next_node, inst->GetInput()); + fsm->createLink(node, next_node); + node = next_node; + } + } + + return node; + } + + if (inst->Type() == PRIM_SVA_THROUGHOUT) + { + log_assert(get_ast_input1(inst) == nullptr); + SigBit expr = importer->net_map_at(inst->GetInput1()); + + fsm->pushThroughout(expr); + int node = parse_sequence(fsm, start_node, inst->GetInput2()); + fsm->popThroughout(); + + return node; + } + + // Handle unsupported primitives + + if (!importer->mode_keep) + log_error("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name()); + log_warning("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name()); + + return start_node; + } + + void import() + { + module = importer->module; + netlist = root->Owner(); + + RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID); + + // parse SVA property clock event + + Instance *at_node = get_ast_input(root); + + // asynchronous immediate assertion/assumption/cover + if (at_node == nullptr && (root->Type() == PRIM_SVA_IMMEDIATE_ASSERT || + root->Type() == PRIM_SVA_IMMEDIATE_COVER || root->Type() == PRIM_SVA_IMMEDIATE_ASSUME)) + { + SigSpec sig_a = importer->net_map_at(root->GetInput()); + RTLIL::Cell *c = nullptr; + + if (eventually) { + if (mode_assert) c = module->addLive(root_name, sig_a, State::S1); + if (mode_assume) c = module->addFair(root_name, sig_a, State::S1); + } else { + if (mode_assert) c = module->addAssert(root_name, sig_a, State::S1); + if (mode_assume) c = module->addAssume(root_name, sig_a, State::S1); + if (mode_cover) c = module->addCover(root_name, sig_a, State::S1); + } + + importer->import_attributes(c->attributes, root); + return; + } + + log_assert(at_node && at_node->Type() == PRIM_SVA_AT); + + VerificClockEdge clock_edge(importer, get_ast_input1(at_node)); + clock = clock_edge.clock_sig; + clock_posedge = clock_edge.posedge; + + // parse disable_iff expression + + Net *sequence_net = at_node->GetInput2(); + + while (1) + { + Instance *sequence_node = net_to_ast_driver(sequence_net); + + if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) { + eventually = true; + sequence_net = sequence_node->GetInput(); + continue; + } + + if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) { + disable_iff = importer->net_map_at(sequence_node->GetInput1()); + sequence_net = sequence_node->GetInput2(); + continue; + } + + break; + } + + // parse SVA sequence into trigger signal + + SigBit prop_okay; + Instance *inst = net_to_ast_driver(sequence_net); + + if (inst == nullptr) + { + prop_okay = importer->net_map_at(sequence_net); + } + else + if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || + inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) + { + Net *antecedent_net = inst->GetInput1(); + Net *consequent_net = inst->GetInput2(); + int node; + + SvaFsm antecedent_fsm(module, clock, clock_posedge, disable_iff); + node = parse_sequence(&antecedent_fsm, antecedent_fsm.startNode, 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); + + SigBit antecedent_accept = antecedent_fsm.getAccept(); + antecedent_fsm.materialize_ndfsm(); + antecedent_fsm.dump(); + + SvaFsm consequent_fsm(module, clock, clock_posedge, disable_iff, antecedent_accept); + node = parse_sequence(&consequent_fsm, consequent_fsm.startNode, consequent_net); + consequent_fsm.createLink(node, consequent_fsm.acceptNode); + + SigBit consequent_reject = consequent_fsm.getReject(); + prop_okay = module->Not(NEW_ID, consequent_reject); + + if (consequent_fsm.is_linear()) + consequent_fsm.materialize_ndfsm(); + else + log_error("Currently only linear sequences are allowed as impliciation consequent.\n"); + } + else + { + // Handle unsupported primitives + + if (!importer->mode_keep) + log_error("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name()); + log_warning("Verific SVA primitive %s (%s) is currently unsupported in this context.\n", inst->View()->Owner()->Name(), inst->Name()); + return; + } + + // add final FF stage + + Wire *prop_okay_q = module->addWire(NEW_ID); + prop_okay_q->attributes["\\init"] = Const(mode_cover ? 0 : 1, 1); + module->addDff(NEW_ID, clock, prop_okay, prop_okay_q, clock_posedge); + + // generate assert/assume/cover cell + + RTLIL::Cell *c = nullptr; + + if (eventually) { + log_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); + } + + importer->import_attributes(c->attributes, root); + } + +#if 0 + // ---------------------------------------------------------- + // Old SVA Importer + vector sva_until_list_inclusive; vector sva_until_list_exclusive; vector*> sva_sequence_alive_list; @@ -603,6 +1170,7 @@ struct VerificSvaImporter importer->import_attributes(c->attributes, root); } +#endif }; void svapp_assert(Instance *inst) diff --git a/tests/sva/sva_range.sv b/tests/sva/sva_range.sv index 38199bff1..d1569fc83 100644 --- a/tests/sva/sva_range.sv +++ b/tests/sva/sva_range.sv @@ -5,7 +5,7 @@ module top ( default clocking @(posedge clk); endclocking assert property ( - a ##[*] b |=> c until ##[*] d + a ##[*] b |=> c until d ); `ifndef FAIL -- 2.30.2