aboutsummaryrefslogtreecommitdiffstats
path: root/src/synth
diff options
context:
space:
mode:
authorTristan Gingold <tgingold@free.fr>2020-07-31 07:38:34 +0200
committerTristan Gingold <tgingold@free.fr>2020-07-31 07:38:34 +0200
commit9efb27060dc5ca23493fb3d3aab6d455049a5790 (patch)
tree5b64e68246673b90f54cf01b6aa90bfa79e7b001 /src/synth
parent5a5419cf64271dc3acfb84affd22c9f7cb4aaa46 (diff)
downloadghdl-9efb27060dc5ca23493fb3d3aab6d455049a5790.tar.gz
ghdl-9efb27060dc5ca23493fb3d3aab6d455049a5790.tar.bz2
ghdl-9efb27060dc5ca23493fb3d3aab6d455049a5790.zip
synth: add --no-assert-cover option. Fix #1414
Diffstat (limited to 'src/synth')
-rw-r--r--src/synth/synth-flags.ads4
-rw-r--r--src/synth/synth-stmts.adb15
2 files changed, 13 insertions, 6 deletions
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