9 files changed, 168 insertions, 4 deletions
diff --git a/doc/using/Synthesis.rst b/doc/using/Synthesis.rst
index 582c7b425..032f207eb 100644
--- a/doc/using/Synthesis.rst
+++ b/doc/using/Synthesis.rst
@@ -92,12 +92,39 @@ simulation back-ends. Hence, available options for synthesis are the same as for
 .. option:: --no-assert-cover
 
   Disable automatic cover PSL assertion activation. If this option isn't used, GHDL generates
-  `cover` directives for each `assert` directive automatically during synthesis.
+  `cover` directives for each `assert` directive (with an implication operator) automatically during synthesis.
 
   Example::
 
     $ ghdl --synth --std=08 --no-assert-cover my_unit
 
+.. option:: --assert-assumes
+
+  Treat all PSL asserts like PSL assumes. If this option is used, GHDL generates an `assume` directive
+  for each `assert` directive during synthesis. This is similar to the `-assert-assumes`
+  option of Yosys' `read_verilog <http://www.clifford.at/yosys/cmd_read_verilog.html>`_ command.
+
+  Example::
+
+    $ ghdl --synth --std=08 --assert-assumes my_unit
+
+  As all PSL asserts are treated like PSL assumes, no `cover` directives are automatically generated for them,
+  regardless of using the :option:`--no-assert-cover` or not.
+
+
+.. option:: --assume-asserts
+
+  Treat all PSL assumes like PSL asserts. If this option is used, GHDL generates an `assert` directive
+  for each `assume` directive during synthesis. This is similar to the `-assume-asserts`
+  option of Yosys' `read_verilog <http://www.clifford.at/yosys/cmd_read_verilog.html>`_ command.
+
+  Example::
+
+    $ ghdl --synth --std=08 --assume-asserts my_unit
+
+  `cover` directives are automatically generated for the resulting asserts (with an implication operator)
+  if :option:`--no-assert-cover` isn't used.
+
 .. TIP::
   Furthermore there are lot of debug options available. Beware: these debug options should only used
   for debugging purposes as they aren't guaranteed to be stable during development of GHDL's synthesis feature.
diff --git a/src/ghdldrv/ghdlsynth.adb b/src/ghdldrv/ghdlsynth.adb
index 94b51c3ab..8bc0250ba 100644
--- a/src/ghdldrv/ghdlsynth.adb
+++ b/src/ghdldrv/ghdlsynth.adb
@@ -128,6 +128,10 @@ package body Ghdlsynth is
       P ("    Neither synthesize assert nor PSL");
       P ("  --no-assert-cover");
       P ("    Cover PSL assertion activation");
+      P ("  --assert-assumes");
+      P ("    Treat all PSL asserts like PSL assumes");
+      P ("  --assume-asserts");
+      P ("    Treat all PSL assumes like PSL asserts");
    end Disp_Long_Help;
 
    procedure Decode_Option (Cmd : in out Command_Synth;
@@ -152,6 +156,10 @@ package body Ghdlsynth is
          Synth.Flags.Flag_Assert_Cover := False;
       elsif Option = "--assert-cover" then
          Synth.Flags.Flag_Assert_Cover := True;
+      elsif Option = "--assert-assumes" then
+         Synth.Flags.Flag_Assert_As_Assume := True;
+      elsif Option = "--assume-asserts" then
+         Synth.Flags.Flag_Assume_As_Assert := True;
       elsif Option = "--top-name=hash" then
          Cmd.Top_Encoding := Name_Hash;
       elsif Option = "--top-name=asis" then
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);
diff --git a/testsuite/synth/assertassumes0/assert0.vhdl b/testsuite/synth/assertassumes0/assert0.vhdl
new file mode 100644
index 000000000..8e25ec87d
--- /dev/null
+++ b/testsuite/synth/assertassumes0/assert0.vhdl
@@ -0,0 +1,21 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity assert0 is
+  port (
+    clk : in  std_logic;
+    i   : out integer
+  );
+end assert0;
+
+architecture behav of assert0 is
+
+begin
+
+  i <= 1;
+
+  default clock is rising_edge(clk);
+
+  psl_a : assert always i = 1;
+
+end behav;
diff --git a/testsuite/synth/assertassumes0/testsuite.sh b/testsuite/synth/assertassumes0/testsuite.sh
new file mode 100755
index 000000000..68d3ae989
--- /dev/null
+++ b/testsuite/synth/assertassumes0/testsuite.sh
@@ -0,0 +1,36 @@
+#! /bin/sh
+
+. ../../testenv.sh
+
+UNIT=assert0
+GHDL_STD_FLAGS=--std=08
+
+synth_only $UNIT
+
+# There should be no assume gate without assert-assume option.
+if grep -q -e "--  assume" syn_$UNIT.vhdl; then
+  exit 1
+fi
+
+# There should be an assert gate without assert-assume option.
+if ! grep -q -e "--  assert" syn_$UNIT.vhdl; then
+  exit 1
+fi
+
+GHDL_FLAGS=--assert-assumes
+
+synth_only $UNIT
+
+# There should be an assume gate with assert-assume option.
+if ! grep -q -e "--  assume" syn_$UNIT.vhdl; then
+  exit 1
+fi
+
+# There should be no assert gate with assert-assume option.
+if grep -q -e "--  assert" syn_$UNIT.vhdl; then
+  exit 1
+fi
+
+clean
+
+echo "Test successful"
diff --git a/testsuite/synth/assumeasserts0/assume0.vhdl b/testsuite/synth/assumeasserts0/assume0.vhdl
new file mode 100644
index 000000000..a2b9ff409
--- /dev/null
+++ b/testsuite/synth/assumeasserts0/assume0.vhdl
@@ -0,0 +1,21 @@
+library ieee;
+use ieee.std_logic_1164.all;
+
+entity assume0 is
+  port (
+    clk : in  std_logic;
+    i   : out integer
+  );
+end assume0;
+
+architecture behav of assume0 is
+
+begin
+
+  i <= 1;
+
+  default clock is rising_edge(clk);
+
+  psl_a : assume always i = 1;
+
+end behav;
diff --git a/testsuite/synth/assumeasserts0/testsuite.sh b/testsuite/synth/assumeasserts0/testsuite.sh
new file mode 100755
index 000000000..bc0544ae2
--- /dev/null
+++ b/testsuite/synth/assumeasserts0/testsuite.sh
@@ -0,0 +1,36 @@
+#! /bin/sh
+
+. ../../testenv.sh
+
+UNIT=assume0
+GHDL_STD_FLAGS=--std=08
+
+synth_only $UNIT
+
+# There should be no assert gate without assert-assume option.
+if grep -q -e "--  assert" syn_$UNIT.vhdl; then
+  exit 1
+fi
+
+# There should be an assume gate with assume-assert option.
+if ! grep -q -e "--  assume" syn_$UNIT.vhdl; then
+  exit 1
+fi
+
+GHDL_FLAGS=--assume-asserts
+
+synth_only $UNIT
+
+# There should be an assert gate with assume-assert option.
+if ! grep -q -e "--  assert" syn_$UNIT.vhdl; then
+  exit 1
+fi
+
+# There should be no assume gate with assert-assume option.
+if grep -q -e "--  assume" syn_$UNIT.vhdl; then
+  exit 1
+fi
+
+clean
+
+echo "Test successful"