mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-07 18:05:24 +00:00
Merge pull request #1515 from YosysHQ/clifford/svastuff
Add Verific/SVA support for "always" and "nexttime" properties
This commit is contained in:
commit
caa3b21f8b
|
@ -789,7 +789,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
|
|||
std::string netlist_name = nl->GetAtt(" \\top") ? nl->CellBaseName() : nl->Owner()->Name();
|
||||
std::string module_name = netlist_name;
|
||||
|
||||
if (nl->IsOperator()) {
|
||||
if (nl->IsOperator() || nl->IsPrimitive()) {
|
||||
module_name = "$verific$" + module_name;
|
||||
} else {
|
||||
if (!norename && *nl->Name()) {
|
||||
|
@ -1409,7 +1409,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
|
|||
|
||||
std::string inst_type = inst->View()->Owner()->Name();
|
||||
|
||||
if (inst->View()->IsOperator()) {
|
||||
if (inst->View()->IsOperator() || inst->View()->IsPrimitive()) {
|
||||
inst_type = "$verific$" + inst_type;
|
||||
} else {
|
||||
if (*inst->View()->Name()) {
|
||||
|
|
|
@ -36,6 +36,8 @@
|
|||
// basic_property:
|
||||
// sequence
|
||||
// not basic_property
|
||||
// nexttime basic_property
|
||||
// nexttime[N] basic_property
|
||||
// sequence #-# basic_property
|
||||
// sequence #=# basic_property
|
||||
// basic_property or basic_property (cover only)
|
||||
|
@ -1264,6 +1266,26 @@ struct VerificSvaImporter
|
|||
return node;
|
||||
}
|
||||
|
||||
if (inst->Type() == PRIM_SVA_NEXTTIME || inst->Type() == PRIM_SVA_S_NEXTTIME)
|
||||
{
|
||||
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);
|
||||
log_assert(sva_low == sva_high);
|
||||
|
||||
int node = start_node;
|
||||
|
||||
for (int i = 0; i < sva_low; i++) {
|
||||
int next_node = fsm.createNode();
|
||||
fsm.createEdge(node, next_node);
|
||||
node = next_node;
|
||||
}
|
||||
|
||||
return parse_sequence(fsm, node, inst->GetInput());
|
||||
}
|
||||
|
||||
if (inst->Type() == PRIM_SVA_SEQ_CONCAT)
|
||||
{
|
||||
const char *sva_low_s = inst->GetAttValue("sva:low");
|
||||
|
@ -1590,15 +1612,25 @@ struct VerificSvaImporter
|
|||
Instance *consequent_inst = net_to_ast_driver(consequent_net);
|
||||
|
||||
if (consequent_inst && (consequent_inst->Type() == PRIM_SVA_UNTIL || consequent_inst->Type() == PRIM_SVA_S_UNTIL ||
|
||||
consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH))
|
||||
consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH ||
|
||||
consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS))
|
||||
{
|
||||
bool until_with = consequent_inst->Type() == PRIM_SVA_UNTIL_WITH || consequent_inst->Type() == PRIM_SVA_S_UNTIL_WITH;
|
||||
|
||||
Net *until_net = consequent_inst->GetInput2();
|
||||
consequent_net = consequent_inst->GetInput1();
|
||||
consequent_inst = net_to_ast_driver(consequent_net);
|
||||
Net *until_net = nullptr;
|
||||
if (consequent_inst->Type() == PRIM_SVA_ALWAYS || consequent_inst->Type() == PRIM_SVA_S_ALWAYS)
|
||||
{
|
||||
consequent_net = consequent_inst->GetInput();
|
||||
consequent_inst = net_to_ast_driver(consequent_net);
|
||||
}
|
||||
else
|
||||
{
|
||||
until_net = consequent_inst->GetInput2();
|
||||
consequent_net = consequent_inst->GetInput1();
|
||||
consequent_inst = net_to_ast_driver(consequent_net);
|
||||
}
|
||||
|
||||
SigBit until_sig = parse_expression(until_net);
|
||||
SigBit until_sig = until_net ? parse_expression(until_net) : RTLIL::S0;
|
||||
SigBit not_until_sig = module->Not(NEW_ID, until_sig);
|
||||
antecedent_fsm.createEdge(node, node, not_until_sig);
|
||||
|
||||
|
|
Loading…
Reference in a new issue