From 36ae5c1f75b11a36fad9ef95881a99128db19f26 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Thu, 31 Dec 2020 22:28:43 +0100 Subject: synth: add option to treat asserts as assumes and vice-versa --- src/ghdldrv/ghdlsynth.adb | 8 ++++++++ src/synth/netlists-disp_vhdl.adb | 3 ++- src/synth/synth-flags.ads | 6 ++++++ src/synth/synth-stmts.adb | 12 ++++++++++-- 4 files changed, 26 insertions(+), 3 deletions(-) (limited to 'src') 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); -- cgit v1.2.3