diff options
-rw-r--r-- | doc/using/Synthesis.rst | 29 | ||||
-rw-r--r-- | src/ghdldrv/ghdlsynth.adb | 8 | ||||
-rw-r--r-- | src/synth/netlists-disp_vhdl.adb | 3 | ||||
-rw-r--r-- | src/synth/synth-flags.ads | 6 | ||||
-rw-r--r-- | src/synth/synth-stmts.adb | 12 | ||||
-rw-r--r-- | testsuite/synth/assertassumes0/assert0.vhdl | 21 | ||||
-rwxr-xr-x | testsuite/synth/assertassumes0/testsuite.sh | 36 | ||||
-rw-r--r-- | testsuite/synth/assumeasserts0/assume0.vhdl | 21 | ||||
-rwxr-xr-x | testsuite/synth/assumeasserts0/testsuite.sh | 36 |
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" |