diff options
| -rw-r--r-- | src/psl/psl-nfas-utils.adb | 26 | ||||
| -rw-r--r-- | src/psl/psl-nfas-utils.ads | 4 | ||||
| -rw-r--r-- | src/vhdl/vhdl-canon.adb | 7 |
3 files changed, 37 insertions, 0 deletions
diff --git a/src/psl/psl-nfas-utils.adb b/src/psl/psl-nfas-utils.adb index 16c0ac6d5..a773b0702 100644 --- a/src/psl/psl-nfas-utils.adb +++ b/src/psl/psl-nfas-utils.adb @@ -347,4 +347,30 @@ package body PSL.NFAs.Utils is end case; end Has_EOS; + procedure Set_Init_Loop (N : NFA) + is + Start : constant NFA_State := Get_Start_State (N); + E : NFA_Edge; + Expr : Node; + begin + -- Look for existing edge. + E := Get_First_Src_Edge (Start); + while E /= No_Edge loop + if Get_Edge_Dest (E) = Start then + Expr := Get_Edge_Expr (E); + if Get_Kind (Expr) = N_True then + return; + end if; + Expr := Create_Node (N_True); + Set_Edge_Expr (E, Expr); + return; + end if; + E := Get_Next_Src_Edge (E); + end loop; + + -- No existing edge. Create one. + Expr := Create_Node (N_True); + Add_Edge (Start, Start, Expr); + end Set_Init_Loop; + end PSL.NFAs.Utils; diff --git a/src/psl/psl-nfas-utils.ads b/src/psl/psl-nfas-utils.ads index f30f665a8..3f11ee880 100644 --- a/src/psl/psl-nfas-utils.ads +++ b/src/psl/psl-nfas-utils.ads @@ -33,6 +33,10 @@ package PSL.NFAs.Utils is -- N must be a boolean expression. function Has_EOS (N : Node) return Boolean; + -- Ensure there is an edge from init state to itself, for the implicit + -- [*] of cover directive. + procedure Set_Init_Loop (N : NFA); + -- Raise Program_Error if N is not internally coherent. procedure Check_NFA (N : NFA); end PSL.NFAs.Utils; diff --git a/src/vhdl/vhdl-canon.adb b/src/vhdl/vhdl-canon.adb index bddcc228f..f7778db00 100644 --- a/src/vhdl/vhdl-canon.adb +++ b/src/vhdl/vhdl-canon.adb @@ -1795,6 +1795,13 @@ package body Vhdl.Canon is -- Generate the NFA. Fa := PSL.Build.Build_SERE_FA (Seq); + + -- IEEE1850-2005 PSL 7.1.6 + -- cover {r} is semantically equivalent to cover {[*]; r}. That is, + -- there is an implicit [*] starting the sequence. + if Get_Kind (Stmt) = Iir_Kind_Psl_Cover_Directive then + PSL.NFAs.Utils.Set_Init_Loop (Fa); + end if; Set_PSL_NFA (Stmt, Fa); Canon_Psl_Clocked_NFA (Stmt); |