PSL: handle and/or in boolean assertion.

3 files changed, 66 insertions, 19 deletions

diff --git a/src/vhdl/sem_expr.adb b/src/vhdl/sem_expr.adb
index 88150b75d..e41f9322a 100644
--- a/src/vhdl/sem_expr.adb
+++ b/src/vhdl/sem_expr.adb
@@ -4751,15 +4751,6 @@ package body Sem_Expr is
       return Res;
    end Insert_Condition_Operator;
 
-   function Maybe_Insert_Condition_Operator (Expr : Iir) return Iir is
-   begin
-      if Get_Base_Type (Get_Type (Expr)) = Boolean_Type_Definition then
-         return Expr;
-      else
-         return Insert_Condition_Operator (Expr);
-      end if;
-   end Maybe_Insert_Condition_Operator;
-
    function Sem_Condition (Cond : Iir) return Iir
    is
       Res : Iir;
diff --git a/src/vhdl/sem_expr.ads b/src/vhdl/sem_expr.ads
index 40fa06f11..4c4f004a1 100644
--- a/src/vhdl/sem_expr.ads
+++ b/src/vhdl/sem_expr.ads
@@ -69,9 +69,8 @@ package Sem_Expr is
    --  A check is made that COND can be read.
    function Sem_Condition (Cond : Iir) return Iir;
 
-   --  Insert an implicit condition operator for EXPR.  Use only when EXPR
-   --  is fully analyzed, otherwise use Sem_Condition.
-   function Maybe_Insert_Condition_Operator (Expr : Iir) return Iir;
+   --  Insert a call to condition operator.
+   function Insert_Condition_Operator (Cond : Iir) return Iir;
 
    --  Same as Sem_Expression but knowing that the type of EXPR must be a
    --  composite type.  Used for expressions in assignment statement when the
diff --git a/src/vhdl/sem_psl.adb b/src/vhdl/sem_psl.adb
index 0a1bf1c4d..503842ce1 100644
--- a/src/vhdl/sem_psl.adb
+++ b/src/vhdl/sem_psl.adb
@@ -478,6 +478,45 @@ package body Sem_Psl is
       Close_Declarative_Region;
    end Sem_Psl_Declaration;
 
+   function Rewrite_As_Boolean_Expression (Prop : Node) return Iir
+   is
+      function Rewrite_Dyadic_Operator
+        (Expr : 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 : 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 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;
@@ -485,8 +524,14 @@ package body Sem_Psl is
    begin
       Res := Create_Iir (Iir_Kind_Concurrent_Assertion_Statement);
       Set_Location (Res, Get_Location (Stmt));
-      Cond := Get_HDL_Node (Get_Psl_Property (Stmt));
-      Cond := Sem_Expr.Maybe_Insert_Condition_Operator (Cond);
+      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))
+        /= Std_Package.Boolean_Type_Definition
+      then
+         Cond := Sem_Expr.Insert_Condition_Operator (Cond);
+      end if;
       Set_Assertion_Condition (Res, Cond);
       Set_Label (Res, Get_Label (Stmt));
       Set_Severity_Expression (Res, Get_Severity_Expression (Stmt));
@@ -495,21 +540,33 @@ package body Sem_Psl is
       return Res;
    end Rewrite_As_Concurrent_Assertion;
 
+   --  Return True iff EXPR is a boolean expression.
+   function Is_Boolean_Assertion (Expr : Node) return Boolean is
+   begin
+      case Get_Kind (Expr) is
+         when N_HDL_Expr =>
+            return True;
+         when N_And_Bool | N_Or_Bool =>
+            return True;
+         when others =>
+            return False;
+      end case;
+   end Is_Boolean_Assertion;
+
    function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir
    is
       Prop : Node;
       Clk : Node;
       Res : Iir;
    begin
+      --  Sem report and severity expressions.
+      Sem_Report_Statement (Stmt);
       Prop := Get_Psl_Property (Stmt);
       Prop := Sem_Property (Prop, True);
       Set_Psl_Property (Stmt, Prop);
 
-      --  Sem report and severity expressions.
-      Sem_Report_Statement (Stmt);
-
-      if Get_Kind (Prop) = N_HDL_Expr
-        and then Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Statement
+      if Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Statement
+        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).