mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-15 13:28:59 +00:00
Code Activity

Add get_fsm_accept_reject for parsing SVA properties

Browse source 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-03-06 11:50:38 +01:00
parent 588ce0e34a
commit d86e875f0f
1 changed files with 88 additions and 75 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

163
frontends/verific/verificsva.cc
View file

@ -483,7 +483,7 @@ struct SvaFsm
dnodes[state] = dnode; dnodes[state] = dnode;
} }
SigBit getReject(SigBit *accept_sigptr = nullptr) void getFirstAcceptReject(SigBit *accept_p, SigBit *reject_p)
{ {
log_assert(!materialized); log_assert(!materialized);
materialized = true; materialized = true;
@ -525,13 +525,15 @@ struct SvaFsm
dnodes.at(edge.first).nextstate.append(trig); dnodes.at(edge.first).nextstate.append(trig);
} }
if (accept_sigptr) { if (accept_p) {
for (auto &value : dnode.accept) for (auto &value : dnode.accept)
accept_sig.append(module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {value, State::S1})); accept_sig.append(module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {value, State::S1}));
} }
for (auto &value : dnode.reject) if (reject_p) {
reject_sig.append(module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {value, State::S1})); for (auto &value : dnode.reject)
reject_sig.append(module->Eq(NEW_ID, {dnode.ctrl, dnode.statesig}, {value, State::S1}));
}
} }
for (auto &it : dnodes) for (auto &it : dnodes)
@ -548,7 +550,7 @@ struct SvaFsm
} }
} }
if (accept_sigptr) if (accept_p)
{ {
if (GetSize(accept_sig) == 0) if (GetSize(accept_sig) == 0)
final_accept_sig = State::S0; final_accept_sig = State::S0;
@ -556,17 +558,33 @@ struct SvaFsm
final_accept_sig = accept_sig; final_accept_sig = accept_sig;
else else
final_accept_sig = module->ReduceOr(NEW_ID, accept_sig); final_accept_sig = module->ReduceOr(NEW_ID, accept_sig);
*accept_sigptr = final_accept_sig; *accept_p = final_accept_sig;
} }
if (GetSize(reject_sig) == 0) if (reject_p)
final_reject_sig = State::S0; {
else if (GetSize(reject_sig) == 1) if (GetSize(reject_sig) == 0)
final_reject_sig = reject_sig; final_reject_sig = State::S0;
else else if (GetSize(reject_sig) == 1)
final_reject_sig = module->ReduceOr(NEW_ID, reject_sig); final_reject_sig = reject_sig;
else
final_reject_sig = module->ReduceOr(NEW_ID, reject_sig);
*reject_p = final_reject_sig;
}
}
return final_reject_sig; SigBit getFirstAccept()
{
SigBit accept;
getFirstAcceptReject(nullptr, &accept);
return accept;
}
SigBit getReject()
{
SigBit reject;
getFirstAcceptReject(nullptr, &reject);
return reject;
} }
void getDFsm(SvaFsm &output_fsm, int output_start_node, int output_accept_node, int output_reject_node) void getDFsm(SvaFsm &output_fsm, int output_start_node, int output_accept_node, int output_reject_node)
@ -903,20 +921,26 @@ struct VerificSvaImporter
int sva_high = atoi(sva_high_s); int sva_high = atoi(sva_high_s);
bool sva_inf = !strcmp(sva_high_s, "$"); bool sva_inf = !strcmp(sva_high_s, "$");
int node = parse_sequence(fsm, start_node, inst->GetInput()); Net *body_net = inst->GetInput();
Instance *body_inst = net_to_ast_driver(body_net);
if (body_inst != nullptr)
parser_error(body_inst);
int node = parse_sequence(fsm, start_node, body_net);
for (int i = 1; i < sva_low; i++) for (int i = 1; i < sva_low; i++)
{ {
int next_node = fsm.createNode(); int next_node = fsm.createNode();
fsm.createEdge(node, next_node); fsm.createEdge(node, next_node);
node = parse_sequence(fsm, next_node, inst->GetInput()); node = parse_sequence(fsm, next_node, body_net);
} }
if (sva_inf) if (sva_inf)
{ {
int next_node = fsm.createNode(); int next_node = fsm.createNode();
fsm.createEdge(node, next_node); fsm.createEdge(node, next_node);
next_node = parse_sequence(fsm, next_node, inst->GetInput()); next_node = parse_sequence(fsm, next_node, body_net);
fsm.createLink(next_node, node); fsm.createLink(next_node, node);
} }
else else
@ -925,7 +949,7 @@ struct VerificSvaImporter
{ {
int next_node = fsm.createNode(); int next_node = fsm.createNode();
fsm.createEdge(node, next_node); fsm.createEdge(node, next_node);
next_node = parse_sequence(fsm, next_node, inst->GetInput()); next_node = parse_sequence(fsm, next_node, body_net);
fsm.createLink(node, next_node); fsm.createLink(node, next_node);
node = next_node; node = next_node;
} }
@ -974,13 +998,30 @@ struct VerificSvaImporter
parser_error(inst); parser_error(inst);
} }
SigBit parse_property(Net *net) void get_fsm_accept_reject(SvaFsm &fsm, SigBit *accept_p, SigBit *reject_p, bool swap_accpet_reject = false)
{
log_assert(accept_p != nullptr || reject_p != nullptr);
if (swap_accpet_reject)
get_fsm_accept_reject(fsm, reject_p, accept_p);
else if (reject_p == nullptr)
*accept_p = fsm.getAccept();
else if (accept_p == nullptr)
*reject_p = fsm.getReject();
else
fsm.getFirstAcceptReject(accept_p, reject_p);
}
void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p)
{ {
Instance *inst = net_to_ast_driver(net); Instance *inst = net_to_ast_driver(net);
if (inst == nullptr) if (inst == nullptr)
{ {
return importer->net_map_at(net); if (accept_p != nullptr)
*accept_p = importer->net_map_at(net);
if (reject_p != nullptr)
*reject_p = module->Not(NEW_ID, importer->net_map_at(net));
} }
else else
if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION || if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
@ -1012,7 +1053,7 @@ struct VerificSvaImporter
consequent_inst = net_to_ast_driver(consequent_net); consequent_inst = net_to_ast_driver(consequent_net);
if (until_inst != nullptr) if (until_inst != nullptr)
parser_error("Currently only expressions are allowed in SVA_UNTIL condition", until_inst); parser_error(until_inst);
SigBit until_sig = importer->net_map_at(until_net); SigBit until_sig = importer->net_map_at(until_net);
SigBit not_until_sig = module->Not(NEW_ID, until_sig); SigBit not_until_sig = module->Not(NEW_ID, until_sig);
@ -1043,63 +1084,31 @@ struct VerificSvaImporter
node = parse_sequence(consequent_fsm, consequent_fsm.startNode, consequent_net); node = parse_sequence(consequent_fsm, consequent_fsm.startNode, consequent_net);
consequent_fsm.createLink(node, consequent_fsm.acceptNode); consequent_fsm.createLink(node, consequent_fsm.acceptNode);
SigBit prop_okay; get_fsm_accept_reject(consequent_fsm, accept_p, reject_p, consequent_not);
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();
prop_okay = module->Not(NEW_ID, consequent_match);
}
if (verific_verbose) { if (verific_verbose) {
log(" Consequent FSM:\n"); log(" Consequent FSM:\n");
consequent_fsm.dump(); consequent_fsm.dump();
} }
return prop_okay;
}
else
if (inst->Type() == PRIM_SVA_NOT)
{
SvaFsm fsm(clocking);
int node = parse_sequence(fsm, fsm.startNode, inst->GetInput());
fsm.createLink(node, fsm.acceptNode);
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");
fsm.dump();
}
return prop_okay;
} }
else else
{ {
bool prop_not = inst->Type() == PRIM_SVA_NOT;
if (prop_not) {
net = inst->GetInput();
inst = net_to_ast_driver(net);
}
SvaFsm fsm(clocking); SvaFsm fsm(clocking);
int node = parse_sequence(fsm, fsm.startNode, net); int node = parse_sequence(fsm, fsm.startNode, net);
fsm.createLink(node, fsm.acceptNode); fsm.createLink(node, fsm.acceptNode);
SigBit prop_okay; get_fsm_accept_reject(fsm, accept_p, reject_p, prop_not);
if (mode_cover || mode_trigger) {
prop_okay = fsm.getAccept();
} else {
SigBit accept = fsm.getReject();
prop_okay = module->Not(NEW_ID, accept);
}
if (verific_verbose) { if (verific_verbose) {
log(" Sequence FSM:\n"); log(" Sequence FSM:\n");
fsm.dump(); fsm.dump();
} }
return prop_okay;
} }
} }
@ -1124,35 +1133,39 @@ struct VerificSvaImporter
// parse SVA sequence into trigger signal // parse SVA sequence into trigger signal
Net *net = clocking.body_net; Net *net = clocking.body_net;
SigBit prop_okay = parse_property(net); SigBit accept_bit = State::S0, reject_bit = State::S0;
if (mode_assert || mode_assume) {
parse_property(net, nullptr, &reject_bit);
} else {
parse_property(net, &accept_bit, nullptr);
}
if (mode_trigger) if (mode_trigger)
{ {
module->connect(importer->net_map_at(root->GetOutput()), prop_okay); module->connect(importer->net_map_at(root->GetOutput()), accept_bit);
} }
else else
{ {
SigBit sig_a = module->Not(NEW_ID, reject_bit);
SigBit sig_en = module->Or(NEW_ID, accept_bit, reject_bit);
// add final FF stage // add final FF stage
SigBit prop_okay_q = module->addWire(NEW_ID); SigBit sig_a_q = module->addWire(NEW_ID);
clocking.addDff(NEW_ID, prop_okay, prop_okay_q, Const(mode_cover ? 0 : 1, 1)); SigBit 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 assert/assume/cover cell // generate assert/assume/cover cell
RTLIL::Cell *c = nullptr; RTLIL::Cell *c = nullptr;
if (eventually) { if (mode_assert) c = module->addAssert(root_name, sig_a_q, sig_en_q);
parser_error("No support for eventually in Verific SVA bindings yet", root); if (mode_assume) c = module->addAssume(root_name, sig_a_q, sig_en_q);
// if (mode_assert) c = module->addLive(root_name, prop_okay_q, prop_start_q); if (mode_cover) c = module->addCover(root_name, sig_a_q, sig_en_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 (c != nullptr) importer->import_attributes(c->attributes, root);
importer->import_attributes(c->attributes, root);
} }
} }
catch (ParserErrorException) catch (ParserErrorException)