Add support for SVA throughout via Verific

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index c32095927d40bfaeb5df2346065cd46da333bad0..c3b2a2f5e1cbd9f7eebdcd987177b9366b6f8239 100644 (file)
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -433,10 +433,14 @@ struct VerificSvaImporter
                        return;
                }
 
-               if (inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL ||
+               if (inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL || inst->Type() == PRIM_SVA_S_UNTIL ||
                                inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH)
                {
-                       bool flag_with = inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH;
+                       bool flag_with = inst->Type() == PRIM_SVA_THROUGHOUT || inst->Type() == PRIM_SVA_UNTIL_WITH || inst->Type() == PRIM_SVA_S_UNTIL_WITH;
+
+                       if (get_ast_input1(inst) != nullptr)
+                               log_error("Currently only simple expression properties are supported as first operand to SVA_UNTIL.\n");
+
                        SigBit expr = importer->net_map_at(inst->GetInput1());
 
                        if (flag_with)

diff --git a/tests/sva/sva_throughout.sv b/tests/sva/sva_throughout.sv
new file mode 100644 (file)
index 0000000..7e036a0
--- /dev/null
+++ b/tests/sva/sva_throughout.sv
@@ -0,0 +1,19 @@
+module top (
+       input clk,
+       input a, b, c, d
+);
+       default clocking @(posedge clk); endclocking
+
+       assert property (
+               a |=> b throughout (c ##1 d)
+       );
+
+`ifndef FAIL
+       assume property (
+               a |=> b && c
+       );
+       assume property (
+               b && c |=> b && d
+       );
+`endif
+endmodule

diff --git a/tests/sva/sva_until.sv b/tests/sva/sva_until.sv
deleted file mode 100644 (file)
index a721e44..0000000
--- a/tests/sva/sva_until.sv
+++ /dev/null
@@ -1,19 +0,0 @@
-module top (
-       input clk,
-       input a, b, c, d
-);
-       default clocking @(posedge clk); endclocking
-
-       assert property (
-               a |=> b until_with (c ##1 d)
-       );
-
-`ifndef FAIL
-       assume property (
-               a |=> b && c
-       );
-       assume property (
-               b && c |=> b && d
-       );
-`endif
-endmodule