docs/hazmat/primitives/padding.rst


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84

.. hazmat::

Padding
=======

.. module:: cryptography.hazmat.primitives.padding

Padding is a way to take data that may or may not be a multiple of the block
size for a cipher and extend it out so that it is. This is required for many
block cipher modes as they require the data to be encrypted to be an exact
multiple of the block size.


.. class:: PKCS7(block_size)

    PKCS7 padding is a generalization of PKCS5 padding (also known as standard
    padding). PKCS7 padding works by appending ``N`` bytes with the value of
    ``chr(N)``, where ``N`` is the number of bytes required to make the final
    block of data the same size as the block size. A simple example of padding
    is:

    .. doctest::

        >>> from cryptography.hazmat.primitives import padding
        >>> padder = padding.PKCS7(128).padder()
        >>> padded_data = padder.update(b"11111111111111112222222222")
        >>> padded_data
        '1111111111111111'
        >>> padded_data += padder.finalize()
        >>> padded_data
        '11111111111111112222222222\x06\x06\x06\x06\x06\x06'
        >>> unpadder = padding.PKCS7(128).unpadder()
        >>> data = unpadder.update(padded_data)
        >>> data
        '1111111111111111'
        >>> data + unpadder.finalize()
        '11111111111111112222222222'

    :param block_size: The size of the block in bits that the data is being
                       padded to.
    :raises ValueError: Raised if block size is not a multiple of 8 or is not
        between 0 and 256.

    .. method:: padder()

        :returns: A padding
            :class:`~cryptography.hazmat.primitives.padding.PaddingContext`
            provider.

    .. method:: unpadder()

        :returns: An unpadding
            :class:`~cryptography.hazmat.primitives.padding.PaddingContext`
            provider.


.. class:: PaddingContext

    When calling ``padder()`` or ``unpadder()`` the result will conform to the
    ``PaddingContext`` interface. You can then call ``update(data)`` with data
    until you have fed everything into the context. Once that is done call
    ``finalize()`` to finish the operation and obtain the remainder of the
    data.

    .. method:: update(data)

        :param bytes data: The data you wish to pass into the context.
        :return bytes: Returns the data that was padded or unpadded.
        :raises TypeError: Raised if data is not bytes.
        :raises cryptography.exceptions.AlreadyFinalized: See :meth:`finalize`.
        :raises TypeError: This exception is raised if ``data`` is not ``bytes``.

    .. method:: finalize()

        Finalize the current context and return the rest of the data.

        After ``finalize`` has been called this object can no longer be used;
        :meth:`update` and :meth:`finalize` will raise an
        :class:`~cryptography.exceptions.AlreadyFinalized` exception.

        :return bytes: Returns the remainder of the data.
        :raises TypeError: Raised if data is not bytes.
        :raises ValueError: When trying to remove padding from incorrectly
                            padded data.
--  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 Libraries;

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
      Etype : constant Iir := Get_Type (Expr);
   begin
      --  In case of overload, consider the expression not as a PSL boolean.
      --  It couldn't be resolved, so there will be an error, unless the whole
      --  property is used in an assertion and the assertion is not considered
      --  as a PSL assertion.
      if Sem_Names.Is_Overload_List (Etype) then
         return False;
      end if;

      return Is_Psl_Boolean_Type (Etype);
   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
              | Iir_Kind_Psl_Boolean_Parameter =>
               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
            | N_Strong =>
            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
         if Get_Kind (Formal) = N_Boolean_Parameter then
            El := Create_Iir (Iir_Kind_Psl_Boolean_Parameter);
            Set_Type (El, Std_Package.Boolean_Type_Definition);
         else
            El := Create_Iir (Iir_Kind_Psl_Declaration);
         end if;
         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;

   procedure Sem_Psl_Inherit_Spec (Item : Iir)
   is
      Name : Iir;
      Unit : Iir;
   begin
      --  Resolve name
      Name := Get_Name (Item);
      if Get_Kind (Name) = Iir_Kind_Simple_Name then
         Unit := Sem_Lib.Load_Primary_Unit
           (Libraries.Work_Library, Get_Identifier (Name), Item);
         if Unit = Null_Iir then
            Error_Msg_Sem (+Name, "unit %n was not analyzed", +Name);
            return;
         end if;
         Unit := Get_Library_Unit (Unit);
         Set_Named_Entity (Name, Unit);
      else
         Name := Sem_Names.Sem_Denoting_Name (Name);
         Unit := Get_Named_Entity (Name);
      end if;

      if Get_Kind (Unit) not in Iir_Kinds_Verification_Unit then
         Error_Msg_Sem (+Name, "%n must denote a verification unit", +Name);
         Set_Named_Entity (Name, Null_Iir);
         return;
      end if;

      --  Add items.
      Sem_Scopes.Add_Inherit_Spec (Item);
   end Sem_Psl_Inherit_Spec;

   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.
         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));
      else
         Entity := Null_Iir;
         Arch := Null_Iir;
      end if;

      Sem_Scopes.Open_Declarative_Region;

      if Entity /= Null_Iir then
         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;
      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_Inherit_Spec =>
               Sem_Psl_Inherit_Spec (Item);
            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_Anonymous_Type_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;
      if Entity /= Null_Iir then
         Set_Is_Within_Flag (Entity, False);
      end if;
   end Sem_Psl_Verification_Unit;

end Vhdl.Sem_Psl;