From ace70f3cc4d5ac8d5fb7e02e96d5b3187319e520 Mon Sep 17 00:00:00 2001 From: Tristan Gingold Date: Sat, 13 Feb 2016 18:00:36 +0100 Subject: psl: cover directive works on a sequence, not on a property. --- src/psl/psl-build.adb | 2 -- src/psl/psl-build.ads | 1 + src/psl/psl-prints.adb | 14 +++++--- src/psl/psl-prints.ads | 6 ++-- src/vhdl/canon.adb | 58 +++++++++++++++++++++++--------- src/vhdl/disp_vhdl.adb | 41 ++++++++++++++++++++++- src/vhdl/disp_vhdl.ads | 2 ++ src/vhdl/iirs.adb | 16 +++++++++ src/vhdl/iirs.ads | 8 +++++ src/vhdl/nodes_meta.adb | 24 +++++++++----- src/vhdl/nodes_meta.ads | 2 ++ src/vhdl/parse.adb | 62 ++++++++++++++++++++++------------ src/vhdl/parse_psl.adb | 21 ++++++------ src/vhdl/parse_psl.ads | 1 + src/vhdl/sem_psl.adb | 68 ++++++++++++++++++++++++++++---------- src/vhdl/sem_psl.ads | 4 +++ src/vhdl/sem_stmts.adb | 5 +-- src/vhdl/simulate/debugger.adb | 47 ++++++++++++++++++++++++-- src/vhdl/simulate/simulation.adb | 3 ++ src/vhdl/translate/trans-chap9.adb | 8 ++++- 20 files changed, 307 insertions(+), 86 deletions(-) diff --git a/src/psl/psl-build.adb b/src/psl/psl-build.adb index 661d758bf..7a047b6de 100644 --- a/src/psl/psl-build.adb +++ b/src/psl/psl-build.adb @@ -29,8 +29,6 @@ with PSL.Prints; with PSL.NFAs; use PSL.NFAs; package body PSL.Build is - function Build_SERE_FA (N : Node) return NFA; - package Intersection is function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA; end Intersection; diff --git a/src/psl/psl-build.ads b/src/psl/psl-build.ads index c8e15ee22..dcfadb96a 100644 --- a/src/psl/psl-build.ads +++ b/src/psl/psl-build.ads @@ -21,5 +21,6 @@ with PSL.Nodes; use PSL.Nodes; package PSL.Build is Optimize_Final : Boolean := True; + function Build_SERE_FA (N : Node) return NFA; function Build_FA (N : Node) return NFA; end PSL.Build; diff --git a/src/psl/psl-prints.adb b/src/psl/psl-prints.adb index 19d7c3959..dd0755570 100644 --- a/src/psl/psl-prints.adb +++ b/src/psl/psl-prints.adb @@ -67,7 +67,9 @@ package body PSL.Prints is | N_True | N_False | N_EOS - | N_HDL_Expr => + | N_HDL_Expr + | N_Property_Instance + | N_Sequence_Instance => return Prio_HDL; when N_Or_Bool => return Prio_Seq_Or; @@ -184,8 +186,6 @@ package body PSL.Prints is end if; end Print_Expr; - procedure Print_Sequence (Seq : Node; Parent_Prio : Priority); - procedure Print_Count (N : Node) is B : Node; begin @@ -222,7 +222,7 @@ package body PSL.Prints is Put ("]"); end Print_Repeat_Sequence; - procedure Print_Sequence (Seq : Node; Parent_Prio : Priority) + procedure Print_Sequence (Seq : Node; Parent_Prio : Priority := Prio_Lowest) is Prio : constant Priority := Get_Priority (Seq); Add_Paren : constant Boolean := Prio < Parent_Prio @@ -260,6 +260,8 @@ package body PSL.Prints is when N_Booleans | N_Name_Decl => Print_Expr (Seq); + when N_Sequence_Instance => + Put (Image (Get_Identifier (Get_Declaration (Seq)))); when others => Error_Kind ("print_sequence", Seq); end case; @@ -387,6 +389,10 @@ package body PSL.Prints is Print_Expr (Prop); when N_Sequences => Print_Sequence (Prop, Parent_Prio); + when N_Property_Instance => + Put (Image (Get_Identifier (Get_Declaration (Prop)))); + when N_EOS => + Put ("EOS"); when others => Error_Kind ("print_property", Prop); end case; diff --git a/src/psl/psl-prints.ads b/src/psl/psl-prints.ads index 920ca5939..d49a5e093 100644 --- a/src/psl/psl-prints.ads +++ b/src/psl/psl-prints.ads @@ -21,8 +21,10 @@ with PSL.Priorities; use PSL.Priorities; package PSL.Prints is procedure Print_Unit (Unit : Node); - procedure Print_Property (Prop : Node; - Parent_Prio : Priority := Prio_Lowest); + procedure Print_Sequence + (Seq : Node; Parent_Prio : Priority := Prio_Lowest); + procedure Print_Property + (Prop : Node; Parent_Prio : Priority := Prio_Lowest); procedure Print_Expr (N : Node; Parent_Prio : Priority := Prio_Lowest); -- Procedure to display HDL_Expr nodes. diff --git a/src/vhdl/canon.adb b/src/vhdl/canon.adb index c498ba55c..bf4536088 100644 --- a/src/vhdl/canon.adb +++ b/src/vhdl/canon.adb @@ -1636,6 +1636,31 @@ package body Canon is return False; end Psl_Need_Finalizer; + procedure Canon_Psl_Directive (Stmt : Iir) + is + use PSL.Nodes; + Fa : PSL_NFA; + Num : Natural; + List : Iir_List; + begin + Fa := Get_PSL_NFA (Stmt); + + PSL.NFAs.Labelize_States (Fa, Num); + Set_PSL_Nbr_States (Stmt, Int32 (Num)); + + Set_PSL_EOS_Flag (Stmt, Psl_Need_Finalizer (Fa)); + + List := Create_Iir_List; + Canon_PSL.Canon_Extract_Sensitivity (Get_PSL_Clock (Stmt), List); + Set_PSL_Clock_Sensitivity (Stmt, List); + + if Canon_Flag_Expressions then + Canon_PSL_Expression (Get_PSL_Clock (Stmt)); + Canon_Expression (Get_Severity_Expression (Stmt)); + Canon_Expression (Get_Report_Expression (Stmt)); + end if; + end Canon_Psl_Directive; + procedure Canon_Concurrent_Stmts (Top : Iir_Design_Unit; Parent : Iir) is -- Current element in the chain of concurrent statements. @@ -1897,37 +1922,38 @@ package body Canon is Canon_Generate_Statement_Body (Top, Get_Generate_Statement_Body (El)); - when Iir_Kind_Psl_Assert_Statement - | Iir_Kind_Psl_Cover_Statement => + when Iir_Kind_Psl_Assert_Statement => declare use PSL.Nodes; Prop : PSL_Node; Fa : PSL_NFA; - Num : Natural; - List : Iir_List; begin Prop := Get_Psl_Property (El); Prop := PSL.Rewrites.Rewrite_Property (Prop); Set_Psl_Property (El, Prop); + -- Generate the NFA. Fa := PSL.Build.Build_FA (Prop); Set_PSL_NFA (El, Fa); - PSL.NFAs.Labelize_States (Fa, Num); - Set_PSL_Nbr_States (El, Int32 (Num)); + Canon_Psl_Directive (El); + end; - Set_PSL_EOS_Flag (El, Psl_Need_Finalizer (Fa)); + when Iir_Kind_Psl_Cover_Statement => + declare + use PSL.Nodes; + Seq : PSL_Node; + Fa : PSL_NFA; + begin + Seq := Get_Psl_Sequence (El); + Seq := PSL.Rewrites.Rewrite_SERE (Seq); + Set_Psl_Sequence (El, Seq); - List := Create_Iir_List; - Canon_PSL.Canon_Extract_Sensitivity - (Get_PSL_Clock (El), List); - Set_PSL_Clock_Sensitivity (El, List); + -- Generate the NFA. + Fa := PSL.Build.Build_SERE_FA (Seq); + Set_PSL_NFA (El, Fa); - if Canon_Flag_Expressions then - Canon_PSL_Expression (Get_PSL_Clock (El)); - Canon_Expression (Get_Severity_Expression (El)); - Canon_Expression (Get_Report_Expression (El)); - end if; + Canon_Psl_Directive (El); end; when Iir_Kind_Psl_Default_Clock => diff --git a/src/vhdl/disp_vhdl.adb b/src/vhdl/disp_vhdl.adb index 9872ff802..4cccdf576 100644 --- a/src/vhdl/disp_vhdl.adb +++ b/src/vhdl/disp_vhdl.adb @@ -2835,6 +2835,12 @@ package body Disp_Vhdl is PSL.Prints.Print_Property (Expr); end Disp_Psl_Expression; + procedure Disp_Psl_Sequence (Expr : PSL_Node) is + begin + PSL.Prints.HDL_Expr_Printer := Disp_PSL_HDL_Expr'Access; + PSL.Prints.Print_Sequence (Expr); + end Disp_Psl_Sequence; + procedure Disp_Block_Header (Header : Iir_Block_Header; Indent: Count) is Chain : Iir; @@ -2979,6 +2985,29 @@ package body Disp_Vhdl is Put_Line (";"); end Disp_Psl_Default_Clock; + procedure Disp_Psl_Declaration (Stmt : Iir) + is + use PSL.Nodes; + Decl : constant PSL_Node := Get_Psl_Declaration (Stmt); + begin + Put ("--psl "); + case Get_Kind (Decl) is + when N_Property_Declaration => + Put ("property "); + Disp_Ident (Get_Identifier (Decl)); + Put (" is "); + Disp_Psl_Expression (Get_Property (Decl)); + when N_Sequence_Declaration => + Put ("sequence "); + Disp_Ident (Get_Identifier (Decl)); + Put (" is "); + Disp_Psl_Sequence (Get_Sequence (Decl)); + when others => + Error_Kind ("disp_psl_declaration", Decl); + end case; + Put_Line (";"); + end Disp_Psl_Declaration; + procedure Disp_PSL_NFA (N : PSL.Nodes.NFA) is use PSL.NFAs; @@ -2994,6 +3023,12 @@ package body Disp_Vhdl is E : NFA_Edge; begin if N /= No_NFA then + Put ("-- start: "); + Disp_State (Get_Start_State (N)); + Put (", final: "); + Disp_State (Get_Final_State (N)); + New_Line; + S := Get_First_State (N); while S /= No_State loop E := Get_First_Src_Edge (S); @@ -3027,7 +3062,7 @@ package body Disp_Vhdl is Put ("--psl "); Disp_Label (Stmt); Put ("cover "); - Disp_Psl_Expression (Get_Psl_Property (Stmt)); + Disp_Psl_Sequence (Get_Psl_Sequence (Stmt)); Put_Line (";"); Disp_PSL_NFA (Get_PSL_NFA (Stmt)); end Disp_Psl_Cover_Statement; @@ -3070,6 +3105,8 @@ package body Disp_Vhdl is Disp_For_Generate_Statement (Stmt); when Iir_Kind_Psl_Default_Clock => Disp_Psl_Default_Clock (Stmt); + when Iir_Kind_Psl_Declaration => + Disp_Psl_Declaration (Stmt); when Iir_Kind_Psl_Assert_Statement => Disp_Psl_Assert_Statement (Stmt); when Iir_Kind_Psl_Cover_Statement => @@ -3340,6 +3377,8 @@ package body Disp_Vhdl is | Iir_Kind_Indexed_Name | Iir_Kind_Slice_Name => Disp_Expression (An_Iir); + when Iir_Kind_Psl_Cover_Statement => + Disp_Psl_Cover_Statement (An_Iir); when others => Error_Kind ("disp", An_Iir); end case; diff --git a/src/vhdl/disp_vhdl.ads b/src/vhdl/disp_vhdl.ads index 880290efd..9f04129bc 100644 --- a/src/vhdl/disp_vhdl.ads +++ b/src/vhdl/disp_vhdl.ads @@ -24,6 +24,8 @@ package Disp_Vhdl is -- the node. procedure Disp_Vhdl (An_Iir: Iir); + procedure Disp_PSL_NFA (N : PSL_NFA); + procedure Disp_Expression (Expr: Iir); -- Display an expression. diff --git a/src/vhdl/iirs.adb b/src/vhdl/iirs.adb index 00614233c..3b9f32b86 100644 --- a/src/vhdl/iirs.adb +++ b/src/vhdl/iirs.adb @@ -5229,6 +5229,22 @@ package body Iirs is Set_Field1 (Decl, PSL_Node_To_Iir (Prop)); end Set_Psl_Property; + function Get_Psl_Sequence (Decl : Iir) return PSL_Node is + begin + pragma Assert (Decl /= Null_Iir); + pragma Assert (Has_Psl_Sequence (Get_Kind (Decl)), + "no field Psl_Sequence"); + return Iir_To_PSL_Node (Get_Field1 (Decl)); + end Get_Psl_Sequence; + + procedure Set_Psl_Sequence (Decl : Iir; Prop : PSL_Node) is + begin + pragma Assert (Decl /= Null_Iir); + pragma Assert (Has_Psl_Sequence (Get_Kind (Decl)), + "no field Psl_Sequence"); + Set_Field1 (Decl, PSL_Node_To_Iir (Prop)); + end Set_Psl_Sequence; + function Get_Psl_Declaration (Decl : Iir) return PSL_Node is begin pragma Assert (Decl /= Null_Iir); diff --git a/src/vhdl/iirs.ads b/src/vhdl/iirs.ads index 1272e7723..a1fe93ced 100644 --- a/src/vhdl/iirs.ads +++ b/src/vhdl/iirs.ads @@ -2506,8 +2506,12 @@ package Iirs is -- -- Get/Set_Parent (Field0) -- + -- Only for Iir_Kind_Psl_Assert_Statement: -- Get/Set_Psl_Property (Field1) -- + -- Only for Iir_Kind_Psl_Cover_Statement: + -- Get/Set_Psl_Sequence (Field1) + -- -- Get/Set_Chain (Field2) -- -- Get/Set_Label (Field3) @@ -6645,6 +6649,10 @@ package Iirs is function Get_Psl_Property (Decl : Iir) return PSL_Node; procedure Set_Psl_Property (Decl : Iir; Prop : PSL_Node); + -- Field: Field1 (uc) + function Get_Psl_Sequence (Decl : Iir) return PSL_Node; + procedure Set_Psl_Sequence (Decl : Iir; Prop : PSL_Node); + -- Field: Field1 (uc) function Get_Psl_Declaration (Decl : Iir) return PSL_Node; procedure Set_Psl_Declaration (Decl : Iir; Prop : PSL_Node); diff --git a/src/vhdl/nodes_meta.adb b/src/vhdl/nodes_meta.adb index d5a3c62a0..b868751f5 100644 --- a/src/vhdl/nodes_meta.adb +++ b/src/vhdl/nodes_meta.adb @@ -312,6 +312,7 @@ package body Nodes_Meta is Field_Suspend_Flag => Type_Boolean, Field_Is_Ref => Type_Boolean, Field_Psl_Property => Type_PSL_Node, + Field_Psl_Sequence => Type_PSL_Node, Field_Psl_Declaration => Type_PSL_Node, Field_Psl_Expression => Type_PSL_Node, Field_Psl_Boolean => Type_PSL_Node, @@ -916,6 +917,8 @@ package body Nodes_Meta is return "is_ref"; when Field_Psl_Property => return "psl_property"; + when Field_Psl_Sequence => + return "psl_sequence"; when Field_Psl_Declaration => return "psl_declaration"; when Field_Psl_Expression => @@ -2038,6 +2041,8 @@ package body Nodes_Meta is return Attr_None; when Field_Psl_Property => return Attr_None; + when Field_Psl_Sequence => + return Attr_None; when Field_Psl_Declaration => return Attr_None; when Field_Psl_Expression => @@ -3473,7 +3478,7 @@ package body Nodes_Meta is Field_Report_Expression, Field_Parent, -- Iir_Kind_Psl_Cover_Statement - Field_Psl_Property, + Field_Psl_Sequence, Field_Label, Field_PSL_Clock, Field_PSL_NFA, @@ -5960,6 +5965,8 @@ package body Nodes_Meta is case F is when Field_Psl_Property => return Get_Psl_Property (N); + when Field_Psl_Sequence => + return Get_Psl_Sequence (N); when Field_Psl_Declaration => return Get_Psl_Declaration (N); when Field_Psl_Expression => @@ -5980,6 +5987,8 @@ package body Nodes_Meta is case F is when Field_Psl_Property => Set_Psl_Property (N, V); + when Field_Psl_Sequence => + Set_Psl_Sequence (N, V); when Field_Psl_Declaration => Set_Psl_Declaration (N, V); when Field_Psl_Expression => @@ -9762,15 +9771,14 @@ package body Nodes_Meta is function Has_Psl_Property (K : Iir_Kind) return Boolean is begin - case K is - when Iir_Kind_Psl_Assert_Statement - | Iir_Kind_Psl_Cover_Statement => - return True; - when others => - return False; - end case; + return K = Iir_Kind_Psl_Assert_Statement; end Has_Psl_Property; + function Has_Psl_Sequence (K : Iir_Kind) return Boolean is + begin + return K = Iir_Kind_Psl_Cover_Statement; + end Has_Psl_Sequence; + function Has_Psl_Declaration (K : Iir_Kind) return Boolean is begin return K = Iir_Kind_Psl_Declaration; diff --git a/src/vhdl/nodes_meta.ads b/src/vhdl/nodes_meta.ads index d4ae3a060..19b5930a6 100644 --- a/src/vhdl/nodes_meta.ads +++ b/src/vhdl/nodes_meta.ads @@ -352,6 +352,7 @@ package Nodes_Meta is Field_Suspend_Flag, Field_Is_Ref, Field_Psl_Property, + Field_Psl_Sequence, Field_Psl_Declaration, Field_Psl_Expression, Field_Psl_Boolean, @@ -842,6 +843,7 @@ package Nodes_Meta is function Has_Suspend_Flag (K : Iir_Kind) return Boolean; function Has_Is_Ref (K : Iir_Kind) return Boolean; function Has_Psl_Property (K : Iir_Kind) return Boolean; + function Has_Psl_Sequence (K : Iir_Kind) return Boolean; function Has_Psl_Declaration (K : Iir_Kind) return Boolean; function Has_Psl_Expression (K : Iir_Kind) return Boolean; function Has_Psl_Boolean (K : Iir_Kind) return Boolean; diff --git a/src/vhdl/parse.adb b/src/vhdl/parse.adb index ccbf98617..012a54264 100644 --- a/src/vhdl/parse.adb +++ b/src/vhdl/parse.adb @@ -6917,18 +6917,31 @@ package body Parse is return Res; end Parse_Psl_Declaration; + -- Parse end of PSL assert/cover statement. + procedure Parse_Psl_Assert_Report_Severity (Stmt : Iir) is + begin + if Current_Token = Tok_Report then + -- Skip 'report' + Scan; + + Set_Report_Expression (Stmt, Parse_Expression); + end if; + + if Current_Token = Tok_Severity then + -- Skip 'severity' + Scan; + + Set_Severity_Expression (Stmt, Parse_Expression); + end if; + + Expect (Tok_Semi_Colon); + end Parse_Psl_Assert_Report_Severity; + function Parse_Psl_Assert_Statement return Iir is Res : Iir; begin - case Current_Token is - when Tok_Assert => - Res := Create_Iir (Iir_Kind_Psl_Assert_Statement); - when Tok_Psl_Cover => - Res := Create_Iir (Iir_Kind_Psl_Cover_Statement); - when others => - raise Internal_Error; - end case; + Res := Create_Iir (Iir_Kind_Psl_Assert_Statement); -- Skip 'assert' Scan; @@ -6938,24 +6951,31 @@ package body Parse is -- No more PSL tokens after the property. Scanner.Flag_Psl := False; - if Current_Token = Tok_Report then - -- Skip 'report' - Scan; + Parse_Psl_Assert_Report_Severity (Res); - Set_Report_Expression (Res, Parse_Expression); - end if; + Scanner.Flag_Scan_In_Comment := False; + return Res; + end Parse_Psl_Assert_Statement; - if Current_Token = Tok_Severity then - -- Skip 'severity' - Scan; + function Parse_Psl_Cover_Statement return Iir + is + Res : Iir; + begin + Res := Create_Iir (Iir_Kind_Psl_Cover_Statement); - Set_Severity_Expression (Res, Parse_Expression); - end if; + -- Skip 'cover' + Scan; + + Set_Psl_Sequence (Res, Parse_Psl.Parse_Psl_Sequence); + + -- No more PSL tokens after the property. + Scanner.Flag_Psl := False; + + Parse_Psl_Assert_Report_Severity (Res); - Expect (Tok_Semi_Colon); Scanner.Flag_Scan_In_Comment := False; return Res; - end Parse_Psl_Assert_Statement; + end Parse_Psl_Cover_Statement; procedure Parse_Concurrent_Statements (Parent : Iir) is @@ -7103,7 +7123,7 @@ package body Parse is Stmt := Parse_Psl_Declaration; when Tok_Psl_Cover => Postponed_Not_Allowed; - Stmt := Parse_Psl_Assert_Statement; + Stmt := Parse_Psl_Cover_Statement; when others => -- FIXME: improve message: -- instead of 'unexpected token 'signal' in conc stmt list' diff --git a/src/vhdl/parse_psl.adb b/src/vhdl/parse_psl.adb index 506218ade..a356043aa 100644 --- a/src/vhdl/parse_psl.adb +++ b/src/vhdl/parse_psl.adb @@ -77,17 +77,18 @@ package body Parse_Psl is function Vhdl_To_Psl (N : Iirs.Iir) return Node is + use Iirs; Res : Node; begin Res := Create_Node_Loc (N_HDL_Expr); - Set_Location (Res, Iirs.Get_Location (N)); - Set_HDL_Node (Res, Int32 (N)); + if N /= Null_Iir then + Set_Location (Res, Get_Location (N)); + Set_HDL_Node (Res, Int32 (N)); + end if; return Res; end Vhdl_To_Psl; function Parse_FL_Property (Prio : Priority) return Node; - function Parse_Sequence return Node; - function Parse_Parenthesis_Boolean return Node; function Parse_Boolean (Parent_Prio : Priority) return Node; @@ -161,7 +162,7 @@ package body Parse_Psl is Kind : Nkind; Op_Prio : Priority; begin - Left := Parse_Sequence; -- FIXME: allow boolean; + Left := Parse_Psl_Sequence; -- FIXME: allow boolean; loop case Current_Token is when Tok_Semi_Colon => @@ -282,7 +283,7 @@ package body Parse_Psl is end if; end Parse_Bracket_Number; - function Parse_Sequence return Node is + function Parse_Psl_Sequence return Node is Res, N : Node; begin case Current_Token is @@ -331,7 +332,7 @@ package body Parse_Psl is return Res; end case; end loop; - end Parse_Sequence; + end Parse_Psl_Sequence; -- precond: '(' -- postcond: next token @@ -430,7 +431,7 @@ package body Parse_Psl is when Tok_Left_Paren => return Parse_Parenthesis_FL_Property; when Tok_Left_Curly => - Res := Parse_Sequence; + Res := Parse_Psl_Sequence; if Get_Kind (Res) = N_Braced_SERE and then Current_Token = Tok_Left_Paren then @@ -442,7 +443,7 @@ package body Parse_Psl is Res := Tmp; end if; when others => - Res := Parse_Sequence; + Res := Parse_Psl_Sequence; end case; return Res; end Parse_FL_Property_1; @@ -663,7 +664,7 @@ package body Parse_Psl is Set_Property (Res, Parse_Psl_Property); when N_Sequence_Declaration | N_Endpoint_Declaration => - Set_Sequence (Res, Parse_Sequence); + Set_Sequence (Res, Parse_Psl_Sequence); when others => raise Internal_Error; end case; diff --git a/src/vhdl/parse_psl.ads b/src/vhdl/parse_psl.ads index 62869feb8..160df668e 100644 --- a/src/vhdl/parse_psl.ads +++ b/src/vhdl/parse_psl.ads @@ -20,6 +20,7 @@ with Types; use Types; with Tokens; use Tokens; package Parse_Psl is + function Parse_Psl_Sequence return PSL_Node; function Parse_Psl_Property return PSL_Node; function Parse_Psl_Boolean return PSL_Node; function Parse_Psl_Declaration (Tok : Token_Type) return PSL_Node; diff --git a/src/vhdl/sem_psl.adb b/src/vhdl/sem_psl.adb index 503842ce1..98e258359 100644 --- a/src/vhdl/sem_psl.adb +++ b/src/vhdl/sem_psl.adb @@ -150,11 +150,7 @@ package body Sem_Psl is Expr := Finish_Sem_Name (Expr); Set_HDL_Node (N, Expr); - if Get_Kind (Expr) in Iir_Kinds_Denoting_Name then - Name := Get_Named_Entity (Expr); - else - Name := Expr; - end if; + Name := Strip_Denoting_Name (Expr); case Get_Kind (Name) is when Iir_Kind_Error => @@ -290,7 +286,20 @@ package body Sem_Psl is | N_Not_Bool => return Sem_Boolean (Seq); when N_HDL_Expr => - return Sem_Hdl_Expr (Seq); + Res := Sem_Hdl_Expr (Seq); + case Get_Kind (Res) is + when N_Sequence_Instance + | N_Endpoint_Instance + | N_Boolean_Parameter + | N_Booleans => + null; + when N_Property_Instance => + Error_Msg_Sem + ("property instance not allowed in PSL sequence", Res); + when others => + Error_Kind ("psl.sem_sequence.hdl", Res); + end case; + return Res; when others => Error_Kind ("psl.sem_sequence", Seq); end case; @@ -553,14 +562,30 @@ package body Sem_Psl is end case; end Is_Boolean_Assertion; + procedure Sem_Psl_Directive_Clock (Stmt : Iir; Prop : in out Node) + is + Clk : Node; + begin + Extract_Clock (Prop, Clk); + if Clk = Null_Node then + if Current_Psl_Default_Clock = Null_Iir then + Error_Msg_Sem ("no clock for PSL directive", Stmt); + Clk := Null_Node; + else + Clk := Get_Psl_Boolean (Current_Psl_Default_Clock); + end if; + end if; + Set_PSL_Clock (Stmt, Clk); + end Sem_Psl_Directive_Clock; + function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir is Prop : Node; - Clk : Node; Res : Iir; begin -- Sem report and severity expressions. Sem_Report_Statement (Stmt); + Prop := Get_Psl_Property (Stmt); Prop := Sem_Property (Prop, True); Set_Psl_Property (Stmt, Prop); @@ -576,16 +601,7 @@ package body Sem_Psl is end if; -- Properties must be clocked. - Extract_Clock (Prop, Clk); - if Clk = Null_Node then - if Current_Psl_Default_Clock = Null_Iir then - Error_Msg_Sem ("no clock for PSL assert", Stmt); - Clk := Null_Node; - else - Clk := Get_Psl_Boolean (Current_Psl_Default_Clock); - end if; - end if; - Set_PSL_Clock (Stmt, Clk); + Sem_Psl_Directive_Clock (Stmt, Prop); Set_Psl_Property (Stmt, Prop); -- Check simple subset restrictions. @@ -594,6 +610,24 @@ package body Sem_Psl is return Stmt; end Sem_Psl_Assert_Statement; + procedure Sem_Psl_Cover_Statement (Stmt : Iir) + is + Seq : Node; + begin + -- Sem report and severity expressions. + Sem_Report_Statement (Stmt); + + Seq := Get_Psl_Sequence (Stmt); + Seq := Sem_Sequence (Seq); + + -- Properties must be clocked. + Sem_Psl_Directive_Clock (Stmt, Seq); + Set_Psl_Sequence (Stmt, Seq); + + -- Check simple subset restrictions. + PSL.Subsets.Check_Simple (Seq); + end Sem_Psl_Cover_Statement; + procedure Sem_Psl_Default_Clock (Stmt : Iir) is Expr : Node; diff --git a/src/vhdl/sem_psl.ads b/src/vhdl/sem_psl.ads index 25663a244..482380303 100644 --- a/src/vhdl/sem_psl.ads +++ b/src/vhdl/sem_psl.ads @@ -20,7 +20,11 @@ with Iirs; use Iirs; package Sem_Psl is procedure Sem_Psl_Declaration (Stmt : Iir); + + -- May return a non-psl concurrent assertion statement. function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir; + + procedure Sem_Psl_Cover_Statement (Stmt : Iir); procedure Sem_Psl_Default_Clock (Stmt : Iir); function Sem_Psl_Name (Name : Iir) return Iir; end Sem_Psl; diff --git a/src/vhdl/sem_stmts.adb b/src/vhdl/sem_stmts.adb index 5e04cb494..24d0f96e2 100644 --- a/src/vhdl/sem_stmts.adb +++ b/src/vhdl/sem_stmts.adb @@ -1913,9 +1913,10 @@ package body Sem_Stmts is (El, Is_Passive); when Iir_Kind_Psl_Declaration => Sem_Psl.Sem_Psl_Declaration (El); - when Iir_Kind_Psl_Assert_Statement - | Iir_Kind_Psl_Cover_Statement => + when Iir_Kind_Psl_Assert_Statement => New_El := Sem_Psl.Sem_Psl_Assert_Statement (El); + when Iir_Kind_Psl_Cover_Statement => + Sem_Psl.Sem_Psl_Cover_Statement (El); when Iir_Kind_Psl_Default_Clock => Sem_Psl.Sem_Psl_Default_Clock (El); when Iir_Kind_Simple_Simultaneous_Statement => diff --git a/src/vhdl/simulate/debugger.adb b/src/vhdl/simulate/debugger.adb index bbb16e231..47846394a 100644 --- a/src/vhdl/simulate/debugger.adb +++ b/src/vhdl/simulate/debugger.adb @@ -1298,6 +1298,42 @@ package body Debugger is return Walk_Continue; end Cb_Disp_File; + procedure Info_PSL_Proc (Line : String) + is + pragma Unreferenced (Line); + begin + if PSL_Table.Last < PSL_Table.First then + Put_Line ("no PSL directive"); + return; + end if; + + for I in PSL_Table.First .. PSL_Table.Last loop + declare + E : PSL_Entry renames PSL_Table.Table (I); + begin + Disp_Instance_Name (E.Instance); + Put ('.'); + Put (Name_Table.Image (Get_Identifier (E.Stmt))); + New_Line; + Disp_Vhdl.Disp_PSL_NFA (Get_PSL_NFA (E.Stmt)); + Put (" 01234567890123456789012345678901234567890123456789"); + for I in E.States'Range loop + if I mod 50 = 0 then + New_Line; + Put (Int32'Image (I / 10)); + Put (": "); + end if; + if E.States (I) then + Put ('*'); + else + Put ('.'); + end if; + end loop; + New_Line; + end; + end loop; + end Info_PSL_Proc; + procedure Info_Stats_Proc (Line : String) is P : Natural := Line'First; E : Natural; @@ -1324,7 +1360,8 @@ package body Debugger is end if; end Info_Stats_Proc; - procedure Info_Files_Proc (Line : String) is + procedure Info_Files_Proc (Line : String) + is pragma Unreferenced (Line); Status : Walk_Status; begin @@ -1706,10 +1743,16 @@ package body Debugger is end loop; end Cont_Proc; + Menu_Info_Psl : aliased Menu_Entry := + (Kind => Menu_Command, + Name => new String'("psl"), + Next => null, + Proc => Info_PSL_Proc'Access); + Menu_Info_Stats : aliased Menu_Entry := (Kind => Menu_Command, Name => new String'("stats"), - Next => null, + Next => Menu_Info_Psl'Access, Proc => Info_Stats_Proc'Access); Menu_Info_Tree : aliased Menu_Entry := diff --git a/src/vhdl/simulate/simulation.adb b/src/vhdl/simulate/simulation.adb index b02d47dd2..c33997b7d 100644 --- a/src/vhdl/simulate/simulation.adb +++ b/src/vhdl/simulate/simulation.adb @@ -1112,6 +1112,9 @@ package body Simulation is Release (Marker, Expr_Pool); if V then Nvec := (others => False); + if Get_Kind (E.Stmt) = Iir_Kind_Psl_Cover_Statement then + Nvec (0) := True; + end if; -- For each state: if set, evaluate all outgoing edges. NFA := Get_PSL_NFA (E.Stmt); diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb index b2138cd06..36a8ec471 100644 --- a/src/vhdl/translate/trans-chap9.adb +++ b/src/vhdl/translate/trans-chap9.adb @@ -450,6 +450,12 @@ package body Trans.Chap9 is Start_Declare_Stmt; New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type); Init_Var (Var_I); + if Get_Kind (Stmt) = Iir_Kind_Psl_Cover_Statement then + New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var), + New_Obj_Value (Var_I)), + New_Lit (Std_Boolean_True_Node)); + Inc_Var (Var_I); + end if; Start_Loop_Stmt (Label); Gen_Exit_When (Label, @@ -1372,7 +1378,7 @@ package body Trans.Chap9 is Start_Declare_Stmt; New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type); New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var), - New_Lit (Ghdl_Index_0)), + New_Lit (Ghdl_Index_0)), New_Lit (Std_Boolean_True_Node)); New_Assign_Stmt (New_Obj (Var_I), New_Lit (Ghdl_Index_1)); Start_Loop_Stmt (Label); -- cgit v1.2.3