aboutsummaryrefslogtreecommitdiffstats
path: root/frontends/verific
diff options
context:
space:
mode:
Diffstat (limited to 'frontends/verific')
-rw-r--r--frontends/verific/README8
-rw-r--r--frontends/verific/verific.cc27
-rw-r--r--frontends/verific/verificsva.cc42
3 files changed, 65 insertions, 12 deletions
diff --git a/frontends/verific/README b/frontends/verific/README
index 89584f2e8..c37d76343 100644
--- a/frontends/verific/README
+++ b/frontends/verific/README
@@ -1,7 +1,11 @@
-
This directory contains Verific bindings for Yosys.
-See http://www.verific.com/ for details.
+
+Use Symbiotic EDA Suite if you need Yosys+Verifc.
+https://www.symbioticeda.com/seda-suite
+
+Contact office@symbioticeda.com for free evaluation
+binaries of Symbiotic EDA Suite.
Verific Features that should be enabled in your Verific library
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index de41e1a5c..9274cf5ca 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -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()) {
@@ -2065,7 +2065,12 @@ struct VerificPass : public Pass {
log(" -d <dump_file>\n");
log(" Dump the Verific netlist as a verilog file.\n");
log("\n");
- log("Visit http://verific.com/ for more information on Verific.\n");
+ log("\n");
+ log("Use Symbiotic EDA Suite if you need Yosys+Verifc.\n");
+ log("https://www.symbioticeda.com/seda-suite\n");
+ log("\n");
+ log("Contact office@symbioticeda.com for free evaluation\n");
+ log("binaries of Symbiotic EDA Suite.\n");
log("\n");
}
#ifdef YOSYS_ENABLE_VERIFIC
@@ -2074,7 +2079,13 @@ struct VerificPass : public Pass {
static bool set_verific_global_flags = true;
if (check_noverific_env())
- log_cmd_error("This version of Yosys is built without Verific support.\n");
+ log_cmd_error("This version of Yosys is built without Verific support.\n"
+ "\n"
+ "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
+ "https://www.symbioticeda.com/seda-suite\n"
+ "\n"
+ "Contact office@symbioticeda.com for free evaluation\n"
+ "binaries of Symbiotic EDA Suite.\n");
log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
@@ -2493,7 +2504,13 @@ struct VerificPass : public Pass {
}
#else /* YOSYS_ENABLE_VERIFIC */
void execute(std::vector<std::string>, RTLIL::Design *) YS_OVERRIDE {
- log_cmd_error("This version of Yosys is built without Verific support.\n");
+ log_cmd_error("This version of Yosys is built without Verific support.\n"
+ "\n"
+ "Use Symbiotic EDA Suite if you need Yosys+Verifc.\n"
+ "https://www.symbioticeda.com/seda-suite\n"
+ "\n"
+ "Contact office@symbioticeda.com for free evaluation\n"
+ "binaries of Symbiotic EDA Suite.\n");
}
#endif
} VerificPass;
diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 909e9b4f1..49c0c40ac 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -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);
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-09 10:58:39 +0000