synth: add option to treat asserts as assumes and vice-versa

3 files changed, 18 insertions, 3 deletions

diff --git a/src/synth/netlists-disp_vhdl.adb b/src/synth/netlists-disp_vhdl.adb
index 89703642f..b833e05b1 100644
--- a/src/synth/netlists-disp_vhdl.adb
+++ b/src/synth/netlists-disp_vhdl.adb
@@ -1343,7 +1343,8 @@ package body Netlists.Disp_Vhdl is
             Put_Line (";");
          when Id_Assert =>
             Disp_Template
-              ("  \l0: postponed assert \i0 = '1' severity error;" & NL, Inst);
+              ("  \l0: postponed assert \i0 = '1' severity error; --  assert"
+               & NL, Inst);
          when Id_Assume =>
             Disp_Template
               ("  \l0: assert \i0 = '1' severity warning; --  assume" & NL,
diff --git a/src/synth/synth-flags.ads b/src/synth/synth-flags.ads
index 803e0d99d..81f4fe82f 100644
--- a/src/synth/synth-flags.ads
+++ b/src/synth/synth-flags.ads
@@ -76,5 +76,11 @@ package Synth.Flags is
    --  asserted has been started.
    Flag_Assert_Cover : Boolean := True;
 
+   --  If true, treat all PSL assert directives like assume directives
+   Flag_Assert_As_Assume : Boolean := False;
+
+   --  If true, treat all PSL assume directives like assert directives
+   Flag_Assume_As_Assert : Boolean := False;
+
    Flag_Verbose : Boolean := False;
 end Synth.Flags;
diff --git a/src/synth/synth-stmts.adb b/src/synth/synth-stmts.adb
index 338f1421d..1109b9491 100644
--- a/src/synth/synth-stmts.adb
+++ b/src/synth/synth-stmts.adb
@@ -3587,11 +3587,19 @@ package body Synth.Stmts is
          when Iir_Kind_Psl_Restrict_Directive =>
             Synth_Psl_Restrict_Directive (Syn_Inst, Stmt);
          when Iir_Kind_Psl_Assume_Directive =>
-            Synth_Psl_Assume_Directive (Syn_Inst, Stmt);
+            if Flags.Flag_Assume_As_Assert then
+               Synth_Psl_Assert_Directive (Syn_Inst, Stmt);
+            else
+               Synth_Psl_Assume_Directive (Syn_Inst, Stmt);
+            end if;
          when Iir_Kind_Psl_Cover_Directive =>
             Synth_Psl_Cover_Directive (Syn_Inst, Stmt);
          when Iir_Kind_Psl_Assert_Directive =>
-            Synth_Psl_Assert_Directive (Syn_Inst, Stmt);
+            if Flags.Flag_Assert_As_Assume then
+               Synth_Psl_Assume_Directive (Syn_Inst, Stmt);
+            else
+               Synth_Psl_Assert_Directive (Syn_Inst, Stmt);
+            end if;
          when Iir_Kind_Concurrent_Assertion_Statement =>
             --  Passive statement.
             Synth_Concurrent_Assertion_Statement (Syn_Inst, Stmt);