--  Semantic analysis pass for PSL.
--  Copyright (C) 2009 Tristan Gingold
--
--  This program 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 of the License, or
--  (at your option) any later version.
--
--  This program 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 this program.  If not, see <gnu.org/licenses>.

with Types; use Types;
with Errorout; use Errorout;

with PSL.Types; use PSL.Types;
with PSL.Nodes; use PSL.Nodes;
with PSL.Subsets;
with PSL.Hash;
with PSL.Rewrites;
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_Boolean_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_Boolean_Type;

   --  Return TRUE if EXPR type is a PSL boolean type.
   function Is_Psl_Boolean_Expr (Expr : Iir) return Boolean is
   begin
      return Is_Psl_Boolean_Type (Get_Type (Expr));
   end Is_Psl_Boolean_Expr;

   function Is_Psl_Bit_Type (Atype : Iir) return Boolean
   is
      Btype : constant Iir := Get_Base_Type (Atype);
   begin
      return Btype = Vhdl.Std_Package.Bit_Type_Definition
        or else Btype = Vhdl.Ieee.Std_Logic_1164.Std_Ulogic_Type;
   end Is_Psl_Bit_Type;

   function Is_Psl_Bitvector_Type (Atype : Iir) return Boolean is
   begin
      if not Is_One_Dimensional_Array_Type (Atype) then
         return False;
      end if;
      return Is_Psl_Bit_Type (Get_Element_Subtype (Atype));
   end Is_Psl_Bitvector_Type;

   function Sem_Prev_Builtin (Call : Iir; Atype : Iir) return Iir
   is
      use Vhdl.Sem_Expr;
      use Vhdl.Std_Package;
      Expr  : Iir;
      Count : Iir;
      Clock : Iir;
      First : Boolean;
   begin
      Expr := Get_Expression (Call);
      First := Is_Expr_Not_Analyzed (Expr);
      Expr := Sem_Expression_Ov (Expr, Atype);
      if Expr /= Null_Iir then
         Set_Expression (Call, Expr);
         Set_Type (Call, Get_Type (Expr));
         Set_Expr_Staticness (Call, None);
      end if;

      if First then
         --  Analyze count and clock only once.
         Count := Get_Count_Expression (Call);
         if Count /= Null_Iir then
            Count := Sem_Expression_Wildcard
              (Count, Wildcard_Any_Integer_Type);
            Count := Eval_Expr (Count);
            Set_Count_Expression (Call, Count);
         end if;

         Clock := Get_Clock_Expression (Call);
         if Clock /= Null_Iir then
            Clock := Sem_Expression_Wildcard (Clock, Wildcard_Psl_Bit_Type);
            Set_Clock_Expression (Call, Clock);
         else
            if Current_Psl_Default_Clock = Null_Iir then
               Error_Msg_Sem (+Call, "no clock for PSL prev builtin");
            else
               Set_Default_Clock (Call, Current_Psl_Default_Clock);
            end if;
         end if;
      end if;

      return Call;
   end Sem_Prev_Builtin;

   function Sem_Clock_Builtin (Call : Iir) return Iir
   is
      use Vhdl.Sem_Expr;
      use Vhdl.Std_Package;
      Expr  : Iir;
      Clock : Iir;
      First : Boolean;
   begin
      Expr := Get_Expression (Call);
      First := Is_Expr_Not_Analyzed (Expr);
      Expr := Sem_Expression (Expr, Null_Iir);
      if Expr /= Null_Iir then
         Set_Expression (Call, Expr);
         Set_Type (Call, Vhdl.Std_Package.Boolean_Type_Definition);
         Set_Expr_Staticness (Call, None);
      end if;

      if First then
         --  Analyze clock only once.
         Clock := Get_Clock_Expression (Call);
         if Clock /= Null_Iir then
            Clock := Sem_Expression_Wildcard (Clock, Wildcard_Psl_Bit_Type);
            Set_Clock_Expression (Call, Clock);
         else
            if Current_Psl_Default_Clock = Null_Iir then
               Error_Msg_Sem (+Call, "no clock for %n", +Call);
            else
               Set_Default_Clock (Call, Current_Psl_Default_Clock);
            end if;
         end if;
      end if;

      return Call;
   end Sem_Clock_Builtin;

   function Sem_Onehot_Builtin (Call : Iir) return Iir
   is
      use Vhdl.Sem_Expr;
      use Vhdl.Std_Package;
      Expr : Iir;
   begin
      Expr := Get_Expression (Call);
      Expr := Sem_Expression (Expr, Null_Iir);
      if Expr /= Null_Iir then
         Set_Expression (Call, Expr);
         Set_Type (Call, Vhdl.Std_Package.Boolean_Type_Definition);
         Set_Expr_Staticness (Call, None);
         if not Is_Psl_Bitvector_Type (Get_Type (Expr)) then
            Error_Msg_Sem (+Call, "type of parameter must be bitvector");
         end if;
      end if;
      return Call;
   end Sem_Onehot_Builtin;

   --  Convert VHDL and/or/not nodes to PSL nodes.
   function Convert_Bool (Expr : Iir) return PSL_Node;

   function Convert_Bool_Dyadic_Operator (Expr : Iir; Kind : PSL.Nodes.Nkind)
                                         return PSL_Node
   is
      Left  : constant Iir := Get_Left (Expr);
      Right : constant Iir := Get_Right (Expr);
      N : PSL_Node;
   begin
      if Is_Psl_Boolean_Expr (Left)
        and then Is_Psl_Boolean_Expr (Right)
      then
         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;
      else
         return Null_PSL_Node;
      end if;
   end Convert_Bool_Dyadic_Operator;

   function Convert_Bool_Monadic_Operator (Expr : Iir; Kind : PSL.Nodes.Nkind)
                                          return PSL_Node
   is
      Operand : constant Iir := Get_Operand (Expr);
      N : PSL_Node;
   begin
      if Is_Psl_Boolean_Expr (Operand) then
         N := Create_Node (Kind);
         Set_Location (N, Get_Location (Expr));
         Set_Boolean (N, Convert_Bool (Operand));
         Free_Iir (Expr);
         return N;
      else
         return Null_PSL_Node;
      end if;
   end Convert_Bool_Monadic_Operator;

   --  Convert VHDL and/or/not nodes to PSL nodes.
   function Convert_Bool (Expr : Iir) return PSL_Node
   is
      Res : PSL_Node;
   begin
      case Get_Kind (Expr) is
         when Iir_Kind_And_Operator =>
            Res := Convert_Bool_Dyadic_Operator (Expr, N_And_Bool);
            if Res /= Null_PSL_Node then
               return Res;
            end if;
         when Iir_Kind_Or_Operator =>
            Res := Convert_Bool_Dyadic_Operator (Expr, N_Or_Bool);
            if Res /= Null_PSL_Node then
               return Res;
            end if;
         when Iir_Kind_Not_Operator =>
            Res := Convert_Bool_Monadic_Operator (Expr, N_Not_Bool);
            if Res /= Null_PSL_Node then
               return Res;
            end if;
         when Iir_Kinds_Name =>
            --  Get the named entity for names in order to hash it.
            declare
               Name : Iir;
               Hnode : PSL_Node;
               N : PSL_Node;
            begin
               Name := Get_Named_Entity (Expr);
               if Name /= Null_Iir then
                  Hnode := PSL.Hash.Get_PSL_Node
                    (HDL_Node (Name), Get_Location (Name));
                  N := Create_Node (N_HDL_Expr);
                  Set_Location (N, Get_Location (Expr));
                  Set_HDL_Node (N, HDL_Node (Expr));
                  Set_HDL_Hash (N, Hnode);
                  return N;
               end if;
            end;
         when others =>
            null;
      end case;

      --  Default.
      return PSL.Hash.Get_PSL_Node (HDL_Node (Expr), Get_Location (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;
      Expr_Type : 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_Wildcard
           (Expr, Std_Package.Wildcard_Psl_Boolean_Type);
      end if;

      if Expr = Null_Iir then
         return N;
      end if;
      Expr_Type := Get_Type (Expr);
      if Expr_Type = Null_Iir then
         return N;
      end if;
      Free_Node (N);
      if not Is_Overload_List (Expr_Type)
        and then not Is_Psl_Boolean_Type (Expr_Type)
      then
         Error_Msg_Sem (+Expr, "type of expression must be boolean");
         return PSL.Hash.Get_PSL_Node (HDL_Node (Expr), Get_Location (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
            | N_Plus_Repeat_Seq =>
            Res := Get_Sequence (Seq);
            if Res /= Null_PSL_Node then
               Res := Sem_Sequence (Res);
               Set_Sequence (Seq, Res);
            end if;
            return Seq;
         when N_Equal_Repeat_Seq
            | N_Goto_Repeat_Seq =>
            Res := Get_Boolean (Seq);
            if Res /= Null_PSL_Node then
               Res := Sem_Boolean (Res);
               Set_Boolean (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
            | N_Clocked_SERE =>
            return Sem_Sequence (Prop);
         when N_Star_Repeat_Seq
            | N_Plus_Repeat_Seq =>
            declare
               Seq : PSL_Node;
            begin
               Seq := Get_Sequence (Prop);
               if Seq /= Null_PSL_Node then
                  Seq := Sem_Sequence (Seq);
                  Set_Sequence (Prop, Seq);
               end if;
               return Prop;
            end;
         when N_Equal_Repeat_Seq
            | N_Goto_Repeat_Seq =>
            declare
               B : PSL_Node;
            begin
               B := Get_Boolean (Prop);
               B := Sem_Boolean (B);
               Set_Boolean (Prop, B);
               return Prop;
            end;
         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
            | N_Async_Abort
            | N_Sync_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_Log_Equiv_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 N_Log_Equiv_Prop =>
                        return Reduce_Logic_Binary_Node (Prop, N_Equiv_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 | N_Next_E =>
            --  FIXME: range.
            Sem_Property (Prop);
            return Prop;
         when N_Next_Event =>
            Sem_Number (Prop);
            Sem_Boolean (Prop);
            Sem_Property (Prop);
            return Prop;
         when N_Next_Event_A | N_Next_Event_E =>
            --  FIXME: range.
            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);
            elsif Get_Kind (Child) = N_Clocked_SERE then
               Clk := Get_Boolean (Child);
               Set_Property (Prop, Get_SERE (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
           | N_HDL_Bool =>
            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));
               case Get_Kind (Expr) is
                  when N_HDL_Expr
                    | N_HDL_Bool =>
                     Hexpr := Get_HDL_Node (Expr);
                     Set_Expression (Res, Hexpr);
                     Set_Type (Res, Get_Type (Hexpr));
                  when others =>
                     Hexpr := Rewrite_As_Boolean_Expression (Expr);
                     Set_Expression (Res, Hexpr);
               end case;
               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);
      else
         Cond := Sem_Expr.Sem_Condition_Pass2 (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
           | N_HDL_Bool =>
            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));
      Expr := PSL.Rewrites.Rewrite_Boolean (Expr);
      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), Get_Location (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_Psl_Declaration =>
               Sem_Psl_Declaration (Item);
            when Iir_Kind_Signal_Declaration
               | Iir_Kind_Constant_Declaration
               | Iir_Kind_Type_Declaration
               | Iir_Kind_Subtype_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
               | Iir_Kind_Object_Alias_Declaration
               | Iir_Kind_Non_Object_Alias_Declaration =>
               Sem_Decls.Sem_Declaration
                 (Item, Prev_Item, False, Attr_Spec_Chain);
            when Iir_Kinds_Concurrent_Signal_Assignment
               | Iir_Kinds_Process_Statement
               | Iir_Kinds_Generate_Statement
               | Iir_Kind_Block_Statement
               | Iir_Kind_Concurrent_Procedure_Call_Statement
               | Iir_Kind_Component_Instantiation_Statement =>
               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;