diff options
| -rw-r--r-- | src/ghdldrv/ghdlsynth.adb | 5 | ||||
| -rw-r--r-- | src/synth/synth-flags.ads | 4 | ||||
| -rw-r--r-- | src/synth/synth-stmts.adb | 15 |
3 files changed, 18 insertions, 6 deletions
diff --git a/src/ghdldrv/ghdlsynth.adb b/src/ghdldrv/ghdlsynth.adb index 8c00776e0..8051c8838 100644 --- a/src/ghdldrv/ghdlsynth.adb +++ b/src/ghdldrv/ghdlsynth.adb @@ -120,6 +120,7 @@ package body Ghdlsynth is 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"); + P (" --no-assert-cover Cover PSL assertion activation"); end Disp_Long_Help; procedure Decode_Option (Cmd : in out Command_Synth; @@ -140,6 +141,10 @@ package body Ghdlsynth is Synth.Flags.Flag_Formal := False; elsif Option = "--formal" then Synth.Flags.Flag_Formal := True; + elsif Option = "--no-assert-cover" then + Synth.Flags.Flag_Assert_Cover := False; + elsif Option = "--assert-cover" then + Synth.Flags.Flag_Assert_Cover := 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 f218f76fb..803e0d99d 100644 --- a/src/synth/synth-flags.ads +++ b/src/synth/synth-flags.ads @@ -72,5 +72,9 @@ package Synth.Flags is -- Synthesize PSL and assertions. Flag_Formal : Boolean := True; + -- If true, automatically add a cover on PSL asserts to know if the + -- asserted has been started. + Flag_Assert_Cover : Boolean := True; + Flag_Verbose : Boolean := False; end Synth.Flags; diff --git a/src/synth/synth-stmts.adb b/src/synth/synth-stmts.adb index 1dc25d67c..c89cc7ca9 100644 --- a/src/synth/synth-stmts.adb +++ b/src/synth/synth-stmts.adb @@ -3339,14 +3339,17 @@ package body Synth.Stmts is -- Note: for synthesis, we assume the next state will be correct. -- (If we assert on States, then the first cycle is ignored). Synth_Psl_Dff (Syn_Inst, Stmt, Next_States); - if Next_States /= No_Net then - Lab := Synth_Label (Syn_Inst, Stmt); + if Next_States = No_Net then + return; + end if; + Lab := Synth_Label (Syn_Inst, Stmt); - Inst := Build_Assert - (Ctxt, Lab, - Synth_Psl_Not_Final (Syn_Inst, Stmt, Next_States)); - Set_Location (Inst, Get_Location (Stmt)); + Inst := Build_Assert + (Ctxt, Lab, Synth_Psl_Not_Final (Syn_Inst, Stmt, Next_States)); + Set_Location (Inst, Get_Location (Stmt)); + -- Also add a cover gate to cover assertion activation. + if Flags.Flag_Assert_Cover then Active := Get_Active_State (NFA); if Active /= No_State then if Lab /= No_Sname then |