diff options
author | Tristan Gingold <tgingold@free.fr> | 2020-06-16 07:47:44 +0200 |
---|---|---|
committer | Tristan Gingold <tgingold@free.fr> | 2020-06-16 07:47:44 +0200 |
commit | 667ab51811b612da68524043874277e6484f3392 (patch) | |
tree | 09f3ab6f6013a5464c4b07b8a838b72208ed3e27 | |
parent | 57cf7923209710dd45870ae42d38581747f81e99 (diff) | |
download | ghdl-667ab51811b612da68524043874277e6484f3392.tar.gz ghdl-667ab51811b612da68524043874277e6484f3392.tar.bz2 ghdl-667ab51811b612da68524043874277e6484f3392.zip |
ghdlsynth: add --no-formal and help.
-rw-r--r-- | src/ghdldrv/ghdlsynth.adb | 23 | ||||
-rw-r--r-- | src/synth/synth-flags.ads | 3 | ||||
-rw-r--r-- | src/synth/synth-stmts.adb | 26 |
3 files changed, 52 insertions, 0 deletions
diff --git a/src/ghdldrv/ghdlsynth.adb b/src/ghdldrv/ghdlsynth.adb index 8ca51b81e..1ce7d3e36 100644 --- a/src/ghdldrv/ghdlsynth.adb +++ b/src/ghdldrv/ghdlsynth.adb @@ -29,6 +29,7 @@ with Errorout.Console; with Version; with Default_Paths; with Bug; +with Simple_IO; with Libraries; with Flags; @@ -81,6 +82,7 @@ package body Ghdlsynth is function Decode_Command (Cmd : Command_Synth; Name : String) return Boolean; function Get_Short_Help (Cmd : Command_Synth) return String; + procedure Disp_Long_Help (Cmd : Command_Synth); procedure Decode_Option (Cmd : in out Command_Synth; Option : String; Arg : String; @@ -103,6 +105,23 @@ package body Ghdlsynth is return "--synth [FILES... -e] UNIT [ARCH] Synthesis from UNIT"; end Get_Short_Help; + procedure Disp_Long_Help (Cmd : Command_Synth) + is + pragma Unreferenced (Cmd); + procedure P (Str : String) renames Simple_IO.Put_Line; + begin + P ("You can directly pass the list of files to synthesize:"); + P (" --synth [OPTIONS] { [--work=NAME] FILE } -e [UNIT]"); + P (" If UNIT is not present, the top unit is automatically found"); + P (" You can use --work=NAME to change the library between files"); + P ("Or use already analysed files:"); + P (" --synth [OPTIONS] -e UNIT"); + P ("In addition to analyze options, you can use:"); + P (" -gNAME=VALUE Override the generic NAME of the top unit"); + P (" --vendor-library=NAME Any unit from library NAME is a black boxe"); + P (" --no-formal Neither synthesize assert nor PSL"); + end Disp_Long_Help; + procedure Decode_Option (Cmd : in out Command_Synth; Option : String; Arg : String; @@ -117,6 +136,10 @@ package body Ghdlsynth is and then Is_Generic_Override_Option (Option) then Res := Decode_Generic_Override_Option (Option); + elsif Option = "--no-formal" then + Synth.Flags.Flag_Formal := False; + elsif Option = "--formal" then + Synth.Flags.Flag_Formal := True; elsif Option = "--top-name=hash" then Cmd.Top_Encoding := Name_Hash; elsif Option = "--top-name=asis" then diff --git a/src/synth/synth-flags.ads b/src/synth/synth-flags.ads index 0586ba58c..825cc946f 100644 --- a/src/synth/synth-flags.ads +++ b/src/synth/synth-flags.ads @@ -69,5 +69,8 @@ package Synth.Flags is -- Level at which an assert stop the simulation. Severity_Level : Integer := Grt.Severity.Error_Severity; + -- Synthesize PSL and assertions. + Flag_Formal : Boolean := True; + Flag_Verbose : Boolean := False; end Synth.Flags; diff --git a/src/synth/synth-stmts.adb b/src/synth/synth-stmts.adb index 9418c6e22..af9f89143 100644 --- a/src/synth/synth-stmts.adb +++ b/src/synth/synth-stmts.adb @@ -2811,6 +2811,10 @@ package body Synth.Stmts is En : Net; Inst : Instance; begin + if not Flags.Flag_Formal then + return; + end if; + Cond := Synth_Expression (C.Inst, Get_Assertion_Condition (Stmt)); if Cond = No_Valtyp then Set_Error (C.Inst); @@ -3075,6 +3079,12 @@ package body Synth.Stmts is end if; return; end if; + + if not Flags.Flag_Formal then + -- Ignore the net. + return; + end if; + Inst := Build_Assert (Ctxt, Synth_Label (Syn_Inst, Stmt), Get_Net (Ctxt, Val)); Set_Location (Inst, Get_Location (Stmt)); @@ -3243,6 +3253,10 @@ package body Synth.Stmts is Res : Net; Inst : Instance; begin + if not Flags.Flag_Formal then + return; + end if; + -- Build assume gate. -- Note: for synthesis, we assume the next state will be correct. -- (If we assume on States, then the first cycle is ignored). @@ -3263,6 +3277,10 @@ package body Synth.Stmts is Res : Net; Inst : Instance; begin + if not Flags.Flag_Formal then + return; + end if; + -- Build cover gate. -- Note: for synthesis, we assume the next state will be correct. -- (If we assume on States, then the first cycle is ignored). @@ -3283,6 +3301,10 @@ package body Synth.Stmts is Next_States : Net; Inst : Instance; begin + if not Flags.Flag_Formal then + return; + end if; + -- Build assume gate. -- Note: for synthesis, we assume the next state will be correct. -- (If we assume on States, then the first cycle is ignored). @@ -3307,6 +3329,10 @@ package body Synth.Stmts is Inst : Instance; Lab : Sname; begin + if not Flags.Flag_Formal then + return; + end if; + -- Build assert gate. -- Note: for synthesis, we assume the next state will be correct. -- (If we assert on States, then the first cycle is ignored). |