-- Semantic analysis pass for PSL. -- Copyright (C) 2009 Tristan Gingold -- -- GHDL is free software; you can redistribute it and/or modify it under -- the terms of the GNU General Public License as published by the Free -- Software Foundation; either version 2, or (at your option) any later -- version. -- -- GHDL is distributed in the hope that it will be useful, but WITHOUT ANY -- WARRANTY; without even the implied warranty of MERCHANTABILITY or -- FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License -- for more details. -- -- You should have received a copy of the GNU General Public License -- along with GHDL; see the file COPYING. If not, write to the Free -- Software Foundation, 59 Temple Place - Suite 330, Boston, MA -- 02111-1307, USA. with Types; use Types; with Std_Names; with Errorout; use Errorout; with PSL.Types; use PSL.Types; with PSL.Nodes; use PSL.Nodes; with PSL.Subsets; with PSL.Hash; with PSL.Errors; use PSL.Errors; with Vhdl.Sem_Expr; with Vhdl.Sem_Stmts; use Vhdl.Sem_Stmts; with Vhdl.Sem_Scopes; with Vhdl.Sem_Names; with Vhdl.Sem_Lib; with Vhdl.Sem_Decls; with Vhdl.Utils; use Vhdl.Utils; with Vhdl.Evaluation; use Vhdl.Evaluation; with Vhdl.Std_Package; with Vhdl.Ieee.Std_Logic_1164; with Vhdl.Errors; use Vhdl.Errors; with Vhdl.Xrefs; use Vhdl.Xrefs; package body Vhdl.Sem_Psl is procedure Sem_Psl_Directive_Clock (Stmt : Iir; Prop : in out PSL_Node); -- Return TRUE iff Atype is a PSL boolean type. -- See PSL1.1 5.1.2 Boolean expressions function Is_Psl_Bool_Type (Atype : Iir) return Boolean is Btype : Iir; begin if Atype = Null_Iir then return False; end if; Btype := Get_Base_Type (Atype); return Btype = Vhdl.Std_Package.Boolean_Type_Definition or else Btype = Vhdl.Std_Package.Bit_Type_Definition or else Btype = Vhdl.Ieee.Std_Logic_1164.Std_Ulogic_Type; end Is_Psl_Bool_Type; -- Return TRUE if EXPR type is a PSL boolean type. function Is_Psl_Bool_Expr (Expr : Iir) return Boolean is begin return Is_Psl_Bool_Type (Get_Type (Expr)); end Is_Psl_Bool_Expr; -- Convert VHDL and/or/not nodes to PSL nodes. function Convert_Bool (Expr : Iir) return PSL_Node is use Std_Names; Impl : Iir; begin case Get_Kind (Expr) is when Iir_Kinds_Dyadic_Operator => declare Left : Iir; Right : Iir; function Build_Op (Kind : Nkind) return PSL_Node is N : PSL_Node; begin N := Create_Node (Kind); Set_Location (N, Get_Location (Expr)); Set_Left (N, Convert_Bool (Left)); Set_Right (N, Convert_Bool (Right)); Free_Iir (Expr); return N; end Build_Op; begin Impl := Get_Implementation (Expr); Left := Get_Left (Expr); Right := Get_Right (Expr); if Impl /= Null_Iir and then Is_Psl_Bool_Expr (Left) and then Is_Psl_Bool_Expr (Right) then if Get_Identifier (Impl) = Name_And then return Build_Op (N_And_Bool); elsif Get_Identifier (Impl) = Name_Or then return Build_Op (N_Or_Bool); end if; end if; end; when Iir_Kinds_Monadic_Operator => declare Operand : Iir; function Build_Op (Kind : Nkind) return PSL_Node is N : PSL_Node; begin N := Create_Node (Kind); Set_Location (N, Get_Location (Expr)); Set_Boolean (N, Convert_Bool (Operand)); Free_Iir (Expr); return N; end Build_Op; begin Impl := Get_Implementation (Expr); Operand := Get_Operand (Expr); if Impl /= Null_Iir and then Is_Psl_Bool_Expr (Operand) then if Get_Identifier (Impl) = Name_Not then return Build_Op (N_Not_Bool); end if; end if; end; when Iir_Kinds_Name => -- Get the named entity for names in order to hash it. declare Name : Iir; begin Name := Get_Named_Entity (Expr); if Name /= Null_Iir then return PSL.Hash.Get_PSL_Node (HDL_Node (Name)); end if; end; when others => null; end case; return PSL.Hash.Get_PSL_Node (HDL_Node (Expr)); end Convert_Bool; -- Analyze an HDL expression. This may mostly a wrapper except in the -- case when the expression is in fact a PSL expression. function Sem_Hdl_Expr (N : PSL_Node) return PSL_Node is use Sem_Names; Expr : Iir; Name : Iir; Decl : PSL_Node; Res : PSL_Node; begin Expr := Get_HDL_Node (N); if Get_Kind (Expr) in Iir_Kinds_Name then Sem_Name (Expr); Expr := Finish_Sem_Name (Expr); Set_HDL_Node (N, Expr); Name := Strip_Denoting_Name (Expr); case Get_Kind (Name) is when Iir_Kind_Error => return N; when Iir_Kind_Overload_List => -- FIXME: todo. raise Internal_Error; when Iir_Kind_Psl_Declaration => Decl := Get_Psl_Declaration (Name); case Get_Kind (Decl) is when N_Sequence_Declaration => Res := Create_Node (N_Sequence_Instance); when N_Property_Declaration => Res := Create_Node (N_Property_Instance); when N_Boolean_Parameter | N_Sequence_Parameter | N_Const_Parameter | N_Property_Parameter => -- FIXME: create a n_name Free_Node (N); Free_Iir (Expr); return Decl; when others => Error_Kind ("sem_hdl_expr(2)", Decl); end case; Set_Location (Res, Get_Location (N)); Set_Declaration (Res, Decl); if Get_Parameter_List (Decl) /= Null_PSL_Node then Error_Msg_Sem (+Res, "no actual for instantiation"); end if; Free_Node (N); Free_Iir (Expr); return Res; when Iir_Kind_Psl_Expression => -- Remove the two bridge nodes: from PSL to HDL and from -- HDL to PSL. Free_Node (N); Res := Get_Psl_Expression (Name); Free_Iir (Expr); if Name /= Expr then Free_Iir (Name); end if; return Res; when Iir_Kind_Function_Call | Iir_Kind_Indexed_Name | Iir_Kind_Selected_Element | Iir_Kinds_Expression_Attribute => Expr := Name; when others => Expr := Name_To_Expression (Expr, Null_Iir); end case; else Expr := Sem_Expr.Sem_Expression (Expr, Null_Iir); end if; if Expr = Null_Iir then return N; end if; Free_Node (N); if not Is_Psl_Bool_Expr (Expr) then Error_Msg_Sem (+Expr, "type of expression must be boolean"); return PSL.Hash.Get_PSL_Node (HDL_Node (Expr)); else return Convert_Bool (Expr); end if; end Sem_Hdl_Expr; -- Sem a boolean node. function Sem_Boolean (Bool : PSL_Node) return PSL_Node is begin case Get_Kind (Bool) is when N_HDL_Expr => return Sem_Hdl_Expr (Bool); when N_And_Bool | N_Or_Bool => Set_Left (Bool, Sem_Boolean (Get_Left (Bool))); Set_Right (Bool, Sem_Boolean (Get_Right (Bool))); return Bool; when others => Error_Kind ("psl.sem_boolean", Bool); end case; end Sem_Boolean; procedure Sem_Boolean (N : PSL_Node) is Bool : PSL_Node; begin Bool := Get_Boolean (N); Bool := Sem_Boolean (Bool); Set_Boolean (N, Bool); end Sem_Boolean; -- Used by Sem_Property to rewrite a property logical operator to a -- boolean logical operator. function Reduce_Logic_Binary_Node (Prop : PSL_Node; Bool_Kind : Nkind) return PSL_Node is Res : PSL_Node; begin Res := Create_Node (Bool_Kind); Set_Location (Res, Get_Location (Prop)); Set_Left (Res, Get_Left (Prop)); Set_Right (Res, Get_Right (Prop)); Free_Node (Prop); return Res; end Reduce_Logic_Binary_Node; function Reduce_Logic_Unary_Node (Prop : PSL_Node; Bool_Kind : Nkind) return PSL_Node is Res : PSL_Node; begin Res := Create_Node (Bool_Kind); Set_Location (Res, Get_Location (Prop)); Set_Boolean (Res, Get_Property (Prop)); Free_Node (Prop); return Res; end Reduce_Logic_Unary_Node; function Sem_Sequence (Seq : PSL_Node) return PSL_Node is Res : PSL_Node; L, R : PSL_Node; begin case Get_Kind (Seq) is when N_Braced_SERE => Res := Sem_Sequence (Get_SERE (Seq)); Set_SERE (Seq, Res); return Seq; when N_Clocked_SERE => Res := Sem_Sequence (Get_SERE (Seq)); Set_SERE (Seq, Res); Sem_Boolean (Seq); return Seq; when N_Concat_SERE | N_Fusion_SERE | N_Within_SERE | N_Or_Seq | N_And_Seq | N_Match_And_Seq => L := Sem_Sequence (Get_Left (Seq)); Set_Left (Seq, L); R := Sem_Sequence (Get_Right (Seq)); Set_Right (Seq, R); return Seq; when N_Star_Repeat_Seq => Res := Get_Sequence (Seq); if Res /= Null_PSL_Node then Res := Sem_Sequence (Get_Sequence (Seq)); Set_Sequence (Seq, Res); end if; -- FIXME: range. return Seq; when N_Plus_Repeat_Seq => Res := Get_Sequence (Seq); if Res /= Null_PSL_Node then Res := Sem_Sequence (Get_Sequence (Seq)); Set_Sequence (Seq, Res); end if; return Seq; when N_And_Bool | N_Or_Bool | N_Not_Bool => return Sem_Boolean (Seq); when N_HDL_Expr => 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 (+Res, "property instance not allowed in PSL sequence"); when others => Error_Kind ("psl.sem_sequence.hdl", Res); end case; return Res; when others => Error_Kind ("psl.sem_sequence", Seq); end case; end Sem_Sequence; function Sem_Property (Prop : PSL_Node; Top : Boolean := False) return PSL_Node; procedure Sem_Property (N : PSL_Node; Top : Boolean := False) is Prop : PSL_Node; begin Prop := Get_Property (N); Prop := Sem_Property (Prop, Top); Set_Property (N, Prop); end Sem_Property; procedure Sem_Number (N : PSL_Node) is Num : PSL_Node; begin Num := Get_Number (N); -- FIXME: todo null; Set_Number (N, Num); end Sem_Number; function Sem_Property (Prop : PSL_Node; Top : Boolean := False) return PSL_Node is Res : PSL_Node; begin case Get_Kind (Prop) is when N_Braced_SERE => return Sem_Sequence (Prop); when N_Always | N_Never => -- By extension, clock_event is allowed within outermost -- always/never. Sem_Property (Prop, Top); return Prop; when N_Eventually => Sem_Property (Prop); return Prop; when N_Clock_Event => Sem_Property (Prop); Sem_Boolean (Prop); if not Top then Error_Msg_Sem (+Prop, "inner clock event not supported"); end if; return Prop; when N_Abort => Sem_Property (Prop); Sem_Boolean (Prop); return Prop; when N_Until | N_Before => Res := Sem_Property (Get_Left (Prop)); Set_Left (Prop, Res); Res := Sem_Property (Get_Right (Prop)); Set_Right (Prop, Res); return Prop; when N_Log_Imp_Prop | N_And_Prop | N_Or_Prop => declare L, R : PSL_Node; begin L := Sem_Property (Get_Left (Prop)); Set_Left (Prop, L); R := Sem_Property (Get_Right (Prop)); Set_Right (Prop, R); if Get_Psl_Type (L) = Type_Boolean and then Get_Psl_Type (R) = Type_Boolean then case Get_Kind (Prop) is when N_And_Prop => return Reduce_Logic_Binary_Node (Prop, N_And_Bool); when N_Or_Prop => return Reduce_Logic_Binary_Node (Prop, N_Or_Bool); when N_Log_Imp_Prop => return Reduce_Logic_Binary_Node (Prop, N_Imp_Bool); when others => Error_Kind ("psl.sem_property(log)", Prop); end case; else return Prop; end if; end; when N_Overlap_Imp_Seq | N_Imp_Seq => Res := Sem_Sequence (Get_Sequence (Prop)); Set_Sequence (Prop, Res); Sem_Property (Prop); return Prop; when N_Paren_Prop => declare Op : PSL_Node; begin Op := Get_Property (Prop); Op := Sem_Property (Op); Set_Property (Prop, Op); if Get_Psl_Type (Op) = Type_Boolean then return Reduce_Logic_Unary_Node (Prop, N_Paren_Bool); else return Prop; end if; end; when N_Next => Sem_Number (Prop); Sem_Property (Prop); return Prop; when N_Next_A => -- FIXME: range. Sem_Property (Prop); return Prop; when N_Next_Event => Sem_Number (Prop); Sem_Boolean (Prop); Sem_Property (Prop); return Prop; when N_HDL_Expr => Res := Sem_Hdl_Expr (Prop); if not Top and then Get_Kind (Res) = N_Property_Instance then declare Decl : constant PSL_Node := Get_Declaration (Res); begin if Decl /= Null_PSL_Node and then Get_Global_Clock (Decl) /= Null_PSL_Node then Error_Msg_Sem (+Prop, "property instance already has a clock"); end if; end; end if; return Res; when others => Error_Kind ("psl.sem_property", Prop); end case; end Sem_Property; -- Extract the clock from PROP. procedure Extract_Clock (Prop : in out PSL_Node; Clk : out PSL_Node) is Child : PSL_Node; begin Clk := Null_PSL_Node; case Get_Kind (Prop) is when N_Clock_Event => Clk := Get_Boolean (Prop); Prop := Get_Property (Prop); when N_Clocked_SERE => Clk := Get_Boolean (Prop); Prop := Get_SERE (Prop); when N_Always | N_Never => Child := Get_Property (Prop); if Get_Kind (Child) = N_Clock_Event then Set_Property (Prop, Get_Property (Child)); Clk := Get_Boolean (Child); end if; when N_Property_Instance => Child := Get_Declaration (Prop); Clk := Get_Global_Clock (Child); when others => null; end case; end Extract_Clock; -- Sem a property/sequence/endpoint declaration. procedure Sem_Psl_Declaration (Stmt : Iir) is use Sem_Scopes; Decl : constant PSL_Node := Get_Psl_Declaration (Stmt); Prop : PSL_Node; Clk : PSL_Node; Formal : PSL_Node; El : Iir; begin Sem_Scopes.Add_Name (Stmt); Xref_Decl (Stmt); Open_Declarative_Region; -- Make formal parameters visible. Formal := Get_Parameter_List (Decl); while Formal /= Null_PSL_Node loop El := Create_Iir (Iir_Kind_Psl_Declaration); Set_Location (El, Get_Location (Formal)); Set_Identifier (El, Get_Identifier (Formal)); Set_Psl_Declaration (El, Formal); Sem_Scopes.Add_Name (El); Xref_Decl (El); Set_Visible_Flag (El, True); Formal := Get_Chain (Formal); end loop; case Get_Kind (Decl) is when N_Property_Declaration => -- FIXME: sem formal list Prop := Get_Property (Decl); Prop := Sem_Property (Prop, True); Extract_Clock (Prop, Clk); Set_Property (Decl, Prop); Set_Global_Clock (Decl, Clk); -- Check simple subset restrictions. PSL.Subsets.Check_Simple (Prop); when N_Sequence_Declaration | N_Endpoint_Declaration => -- FIXME: sem formal list, do not allow property parameter. Prop := Get_Sequence (Decl); Prop := Sem_Sequence (Prop); Set_Sequence (Decl, Prop); PSL.Subsets.Check_Simple (Prop); when others => Error_Kind ("sem_psl_declaration", Decl); end case; Set_Visible_Flag (Stmt, True); Close_Declarative_Region; end Sem_Psl_Declaration; procedure Sem_Psl_Endpoint_Declaration (Stmt : Iir) is Decl : constant PSL_Node := Get_Psl_Declaration (Stmt); Prop : PSL_Node; begin Sem_Scopes.Add_Name (Stmt); Xref_Decl (Stmt); pragma Assert (Get_Parameter_List (Decl) = Null_PSL_Node); pragma Assert (Get_Kind (Decl) = N_Endpoint_Declaration); Prop := Get_Sequence (Decl); Prop := Sem_Sequence (Prop); Sem_Psl_Directive_Clock (Stmt, Prop); Set_Sequence (Decl, Prop); PSL.Subsets.Check_Simple (Prop); -- Endpoints are considered as an HDL declaration and must have a -- type. Set_Type (Stmt, Vhdl.Std_Package.Boolean_Type_Definition); Set_Expr_Staticness (Stmt, None); Set_Visible_Flag (Stmt, True); end Sem_Psl_Endpoint_Declaration; function Rewrite_As_Boolean_Expression (Prop : PSL_Node) return Iir is function Rewrite_Dyadic_Operator (Expr : PSL_Node; Kind : Iir_Kind) return Iir is Res : Iir; begin Res := Create_Iir (Kind); Set_Location (Res, Get_Location (Expr)); Set_Left (Res, Rewrite_As_Boolean_Expression (Get_Left (Expr))); Set_Right (Res, Rewrite_As_Boolean_Expression (Get_Right (Expr))); return Res; end Rewrite_Dyadic_Operator; function Rewrite_Monadic_Operator (Expr : PSL_Node; Kind : Iir_Kind) return Iir is Res : Iir; begin Res := Create_Iir (Kind); Set_Location (Res, Get_Location (Expr)); Set_Operand (Res, Rewrite_As_Boolean_Expression (Get_Boolean (Expr))); return Res; end Rewrite_Monadic_Operator; begin case Get_Kind (Prop) is when N_HDL_Expr => return Get_HDL_Node (Prop); when N_And_Bool => return Rewrite_Dyadic_Operator (Prop, Iir_Kind_And_Operator); when N_Or_Bool => return Rewrite_Dyadic_Operator (Prop, Iir_Kind_Or_Operator); when N_Not_Bool => return Rewrite_Monadic_Operator (Prop, Iir_Kind_Not_Operator); when N_Paren_Bool => declare Expr : constant PSL_Node := Get_Boolean (Prop); Hexpr : Iir; Res : Iir; begin Res := Create_Iir (Iir_Kind_Parenthesis_Expression); Set_Location (Res, Get_Location (Prop)); if Get_Kind (Expr) = N_HDL_Expr then Hexpr := Get_HDL_Node (Expr); Set_Expression (Res, Hexpr); Set_Type (Res, Get_Type (Hexpr)); else Set_Expression (Res, Rewrite_As_Boolean_Expression (Expr)); end if; return Res; end; when others => Error_Kind ("rewrite_as_boolean_expression", Prop); end case; end Rewrite_As_Boolean_Expression; function Rewrite_As_Concurrent_Assertion (Stmt : Iir) return Iir is Res : Iir; Cond : Iir; begin Res := Create_Iir (Iir_Kind_Concurrent_Assertion_Statement); Set_Location (Res, Get_Location (Stmt)); Cond := Rewrite_As_Boolean_Expression (Get_Psl_Property (Stmt)); if Get_Type (Cond) = Null_Iir then Cond := Sem_Expr.Sem_Condition (Cond); elsif Get_Base_Type (Get_Type (Cond)) /= Vhdl.Std_Package.Boolean_Type_Definition then Cond := Sem_Expr.Insert_Condition_Operator (Cond); end if; Cond := Eval_Expr_If_Static (Cond); Set_Assertion_Condition (Res, Cond); Set_Label (Res, Get_Label (Stmt)); Set_Severity_Expression (Res, Get_Severity_Expression (Stmt)); Set_Report_Expression (Res, Get_Report_Expression (Stmt)); Set_Postponed_Flag (Res, Get_Postponed_Flag (Stmt)); Set_Parent (Res, Get_Parent (Stmt)); Set_Chain (Res, Get_Chain (Stmt)); return Res; end Rewrite_As_Concurrent_Assertion; -- Return True iff EXPR is a boolean expression. function Is_Boolean_Assertion (Expr : PSL_Node) return Boolean is begin case Get_Kind (Expr) is when N_HDL_Expr => return True; when N_And_Bool | N_Or_Bool | N_Not_Bool | N_Paren_Bool => return True; when others => return False; end case; end Is_Boolean_Assertion; procedure Sem_Psl_Directive_Clock (Stmt : Iir; Prop : in out PSL_Node) is Clk : PSL_Node; begin Extract_Clock (Prop, Clk); if Clk = Null_PSL_Node then if Current_Psl_Default_Clock = Null_Iir then Error_Msg_Sem (+Stmt, "no clock for PSL directive"); Clk := Null_PSL_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_Directive (Stmt : Iir; Can_Rewrite : Boolean) return Iir is Prop : PSL_Node; Res : Iir; begin pragma Assert (Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Directive); -- Sem report and severity expressions. Sem_Report_Statement (Stmt); Prop := Get_Psl_Property (Stmt); Prop := Sem_Property (Prop, True); Set_Psl_Property (Stmt, Prop); if Can_Rewrite and then Is_Boolean_Assertion (Prop) then -- This is a simple assertion. Convert to a non-PSL statement, as -- the handling is simpler (and the assertion doesn't need a clock). Res := Rewrite_As_Concurrent_Assertion (Stmt); Free_Iir (Stmt); return Res; end if; if Get_Postponed_Flag (Stmt) then Error_Msg_Sem (+Stmt, "PSL assertions cannot be postponed"); Set_Postponed_Flag (Stmt, False); end if; -- Properties must be clocked. Sem_Psl_Directive_Clock (Stmt, Prop); Set_Psl_Property (Stmt, Prop); -- Check simple subset restrictions. PSL.Subsets.Check_Simple (Prop); return Stmt; end Sem_Psl_Assert_Directive; procedure Sem_Psl_Assume_Directive (Stmt : Iir) is Prop : PSL_Node; begin Prop := Get_Psl_Property (Stmt); Prop := Sem_Property (Prop, True); Set_Psl_Property (Stmt, Prop); -- Properties must be clocked. Sem_Psl_Directive_Clock (Stmt, Prop); Set_Psl_Property (Stmt, Prop); -- Check simple subset restrictions. PSL.Subsets.Check_Simple (Prop); end Sem_Psl_Assume_Directive; procedure Sem_Psl_Sequence (Stmt : Iir) is Seq : PSL_Node; begin Seq := Get_Psl_Sequence (Stmt); Seq := Sem_Sequence (Seq); -- Expect a pure sequence. case Get_Kind (Seq) is when N_Sequence_Instance | N_Star_Repeat_Seq | N_Goto_Repeat_Seq | N_Plus_Repeat_Seq | N_Equal_Repeat_Seq | N_Braced_SERE | N_Clocked_SERE => null; when others => Error_Msg_Sem (+Seq, "sequence expected here"); end case; -- 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_Sequence; procedure Sem_Psl_Cover_Directive (Stmt : Iir) is begin Sem_Report_Expression (Stmt); Sem_Psl_Sequence (Stmt); end Sem_Psl_Cover_Directive; procedure Sem_Psl_Restrict_Directive (Stmt : Iir) is begin Sem_Psl_Sequence (Stmt); end Sem_Psl_Restrict_Directive; procedure Sem_Psl_Default_Clock (Stmt : Iir) is Expr : PSL_Node; begin if Current_Psl_Default_Clock /= Null_Iir and then Get_Parent (Current_Psl_Default_Clock) = Get_Parent (Stmt) then Report_Start_Group; Error_Msg_Sem (+Stmt, "redeclaration of PSL default clock in the same region"); Error_Msg_Sem (+Current_Psl_Default_Clock, " (previous default clock declaration)"); Report_End_Group; end if; Expr := Sem_Boolean (Get_Psl_Boolean (Stmt)); Set_Psl_Boolean (Stmt, Expr); Current_Psl_Default_Clock := Stmt; end Sem_Psl_Default_Clock; function Sem_Psl_Instance_Name (Name : Iir) return Iir is Prefix : constant Iir := Get_Prefix (Name); Ent : constant Iir := Get_Named_Entity (Prefix); Decl : constant PSL_Node := Get_Psl_Declaration (Ent); Formal : PSL_Node; Assoc : Iir; Res : PSL_Node; Last_Assoc : PSL_Node; Assoc2 : PSL_Node; Actual : Iir; Psl_Actual : PSL_Node; Res2 : Iir; begin pragma Assert (Get_Kind (Ent) = Iir_Kind_Psl_Declaration or Get_Kind (Ent) = Iir_Kind_Psl_Endpoint_Declaration); case Get_Kind (Decl) is when N_Property_Declaration => Res := Create_Node (N_Property_Instance); when N_Sequence_Declaration => Res := Create_Node (N_Sequence_Instance); when N_Endpoint_Declaration => Res := Create_Node (N_Endpoint_Instance); when others => Error_Msg_Sem (+Name, "can only instantiate a psl declaration"); return Null_Iir; end case; Set_Declaration (Res, Decl); Set_Location (Res, Get_Location (Name)); Formal := Get_Parameter_List (Decl); Assoc := Get_Association_Chain (Name); Last_Assoc := Null_PSL_Node; while Formal /= Null_PSL_Node loop if Assoc = Null_Iir then Error_Msg_Sem (+Name, "not enough association"); exit; end if; if Get_Kind (Assoc) /= Iir_Kind_Association_Element_By_Expression then Error_Msg_Sem (+Assoc, "open or individual association not allowed"); elsif Get_Formal (Assoc) /= Null_Iir then Error_Msg_Sem (+Assoc, "named association not allowed in psl"); else Actual := Get_Actual (Assoc); -- FIXME: currently only boolean are parsed. Actual := Sem_Expr.Sem_Expression (Actual, Null_Iir); if Get_Kind (Actual) in Iir_Kinds_Name then Actual := Get_Named_Entity (Actual); end if; Psl_Actual := PSL.Hash.Get_PSL_Node (HDL_Node (Actual)); end if; Assoc2 := Create_Node (N_Actual); Set_Location (Assoc2, Get_Location (Assoc)); Set_Formal (Assoc2, Formal); Set_Actual (Assoc2, Psl_Actual); if Last_Assoc = Null_PSL_Node then Set_Association_Chain (Res, Assoc2); else Set_Chain (Last_Assoc, Assoc2); end if; Last_Assoc := Assoc2; Formal := Get_Chain (Formal); Assoc := Get_Chain (Assoc); end loop; if Assoc /= Null_Iir then Error_Msg_Sem (+Name, "too many association"); end if; Res2 := Create_Iir (Iir_Kind_Psl_Expression); Set_Psl_Expression (Res2, Res); Location_Copy (Res2, Name); return Res2; end Sem_Psl_Instance_Name; -- Called by sem_names to analyze a psl name. function Sem_Psl_Name (Name : Iir) return Iir is begin case Get_Kind (Name) is when Iir_Kind_Parenthesis_Name => return Sem_Psl_Instance_Name (Name); when others => Error_Kind ("sem_psl_name", Name); end case; return Null_Iir; end Sem_Psl_Name; procedure Sem_Hierarchical_Name (Hier_Name : Iir; Unit : Iir) is Entity_Name : Iir; Design_Entity : Iir; Lib_Entity : Iir; Arch_Name : Iir; Arch : Iir; Library : Iir_Library_Declaration; begin Entity_Name := Get_Entity_Name (Hier_Name); Library := Get_Library (Get_Design_File (Get_Design_Unit (Unit))); Design_Entity := Sem_Lib.Load_Primary_Unit (Library, Get_Identifier (Entity_Name), Entity_Name); if Design_Entity = Null_Iir then Error_Msg_Sem (+Entity_Name, "entity %n was not analysed", +Entity_Name); return; end if; Lib_Entity := Get_Library_Unit (Design_Entity); if Get_Kind (Lib_Entity) /= Iir_Kind_Entity_Declaration then Error_Msg_Sem (+Entity_Name, "name %i does not denote an entity", +Entity_Name); return; end if; Set_Named_Entity (Entity_Name, Lib_Entity); Xrefs.Xref_Ref (Entity_Name, Lib_Entity); Arch_Name := Get_Architecture (Hier_Name); if Arch_Name /= Null_Iir then Arch := Sem_Lib.Load_Secondary_Unit (Design_Entity, Get_Identifier (Arch_Name), Arch_Name); if Arch /= Null_Iir then Set_Named_Entity (Arch_Name, Get_Library_Unit (Arch)); end if; end if; end Sem_Hierarchical_Name; procedure Sem_Psl_Verification_Unit (Unit : Iir) is Hier_Name : constant Iir := Get_Hierarchical_Name (Unit); Entity : Iir; Arch : Iir; Item : Iir; Prev_Item : Iir; Attr_Spec_Chain : Iir; begin if Hier_Name = Null_Iir then -- Hierarchical name is optional. -- If the unit is not bound, the names are not bound too. return; end if; Sem_Hierarchical_Name (Hier_Name, Unit); -- Import declarations. Entity := Get_Entity_Name (Hier_Name); if Entity = Null_Iir then return; end if; Entity := Get_Named_Entity (Entity); if Entity = Null_Iir then return; end if; Arch := Get_Architecture (Hier_Name); if Arch /= Null_Iir then Arch := Get_Named_Entity (Arch); if Arch = Null_Iir then return; end if; end if; Sem_Scopes.Add_Context_Clauses (Get_Design_Unit (Entity)); Sem_Scopes.Open_Declarative_Region; Set_Is_Within_Flag (Entity, True); Sem_Scopes.Add_Entity_Declarations (Entity); if Arch /= Null_Iir then Sem_Scopes.Open_Scope_Extension; Sem_Scopes.Extend_Scope_Of_Block_Declarations (Arch); end if; Attr_Spec_Chain := Null_Iir; Prev_Item := Null_Iir; Item := Get_Vunit_Item_Chain (Unit); while Item /= Null_Iir loop case Get_Kind (Item) is when Iir_Kind_Psl_Default_Clock => Sem_Psl_Default_Clock (Item); when Iir_Kind_Psl_Assert_Directive => Item := Sem_Psl_Assert_Directive (Item, False); when Iir_Kind_Psl_Assume_Directive => Sem_Psl_Assume_Directive (Item); when Iir_Kind_Psl_Restrict_Directive => Sem_Psl_Restrict_Directive (Item); when Iir_Kind_Psl_Cover_Directive => Sem_Psl_Cover_Directive (Item); when Iir_Kind_Signal_Declaration | Iir_Kind_Function_Declaration | Iir_Kind_Procedure_Declaration | Iir_Kind_Function_Body | Iir_Kind_Procedure_Body | Iir_Kind_Attribute_Declaration | Iir_Kind_Attribute_Specification => Sem_Decls.Sem_Declaration (Item, Prev_Item, False, Attr_Spec_Chain); when Iir_Kind_Concurrent_Simple_Signal_Assignment => Sem_Stmts.Sem_Concurrent_Statement (Item, False); when others => Error_Kind ("sem_psl_verification_unit", Item); end case; if Prev_Item = Null_Iir then Set_Vunit_Item_Chain (Unit, Item); else Set_Chain (Prev_Item, Item); end if; Prev_Item := Item; Item := Get_Chain (Item); end loop; if Arch /= Null_Iir then Sem_Scopes.Close_Scope_Extension; end if; Sem_Scopes.Close_Declarative_Region; Set_Is_Within_Flag (Entity, False); end Sem_Psl_Verification_Unit; end Vhdl.Sem_Psl;