ghdlsynth: add --no-formal and help.

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).