aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--python/libghdl/thin/vhdl/nodes.py180
-rw-r--r--python/libghdl/thin/vhdl/tokens.py47
-rw-r--r--src/ghdldrv/ghdlprint.adb1
-rw-r--r--src/ghdldrv/ghdlrun.adb2
-rw-r--r--src/grt/grt-disp_rti.adb3
-rw-r--r--src/grt/grt-lib.adb6
-rw-r--r--src/grt/grt-lib.ads6
-rw-r--r--src/grt/grt-psl.adb22
-rw-r--r--src/grt/grt-rtis.ads1
-rw-r--r--src/vhdl/simulate/simul-elaboration.adb3
-rw-r--r--src/vhdl/simulate/simul-simulation-main.adb11
-rw-r--r--src/vhdl/translate/trans-chap9.adb29
-rw-r--r--src/vhdl/translate/trans-rtis.adb16
-rw-r--r--src/vhdl/translate/trans-rtis.ads1
-rw-r--r--src/vhdl/translate/trans_decls.ads1
-rw-r--r--src/vhdl/translate/translation.adb2
-rw-r--r--src/vhdl/vhdl-annotations.adb3
-rw-r--r--src/vhdl/vhdl-canon.adb3
-rw-r--r--src/vhdl/vhdl-elocations.adb3
-rw-r--r--src/vhdl/vhdl-elocations.ads3
-rw-r--r--src/vhdl/vhdl-errors.adb4
-rw-r--r--src/vhdl/vhdl-nodes.adb3
-rw-r--r--src/vhdl/vhdl-nodes.ads17
-rw-r--r--src/vhdl/vhdl-nodes_meta.adb238
-rw-r--r--src/vhdl/vhdl-parse.adb30
-rw-r--r--src/vhdl/vhdl-prints.adb28
-rw-r--r--src/vhdl/vhdl-scanner.adb2
-rw-r--r--src/vhdl/vhdl-sem_psl.adb25
-rw-r--r--src/vhdl/vhdl-sem_psl.ads3
-rw-r--r--src/vhdl/vhdl-sem_stmts.adb6
-rw-r--r--src/vhdl/vhdl-tokens.adb2
-rw-r--r--src/vhdl/vhdl-tokens.ads1
-rw-r--r--testsuite/gna/issue880/psl.ref30
-rw-r--r--testsuite/gna/issue880/psl.vhdl30
-rwxr-xr-xtestsuite/gna/issue880/testsuite.sh41
-rw-r--r--testsuite/gna/ticket24/psl.ref3
36 files changed, 555 insertions, 251 deletions
diff --git a/python/libghdl/thin/vhdl/nodes.py b/python/libghdl/thin/vhdl/nodes.py
index 26b1a6f86..05782b97f 100644
--- a/python/libghdl/thin/vhdl/nodes.py
+++ b/python/libghdl/thin/vhdl/nodes.py
@@ -198,91 +198,92 @@ class Iir_Kind:
Concurrent_Selected_Signal_Assignment = 183
Concurrent_Assertion_Statement = 184
Concurrent_Procedure_Call_Statement = 185
- Psl_Assert_Statement = 186
- Psl_Cover_Directive = 187
- Psl_Restrict_Directive = 188
- Block_Statement = 189
- If_Generate_Statement = 190
- Case_Generate_Statement = 191
- For_Generate_Statement = 192
- Component_Instantiation_Statement = 193
- Psl_Default_Clock = 194
- Simple_Simultaneous_Statement = 195
- Generate_Statement_Body = 196
- If_Generate_Else_Clause = 197
- Simple_Signal_Assignment_Statement = 198
- Conditional_Signal_Assignment_Statement = 199
- Selected_Waveform_Assignment_Statement = 200
- Null_Statement = 201
- Assertion_Statement = 202
- Report_Statement = 203
- Wait_Statement = 204
- Variable_Assignment_Statement = 205
- Conditional_Variable_Assignment_Statement = 206
- Return_Statement = 207
- For_Loop_Statement = 208
- While_Loop_Statement = 209
- Next_Statement = 210
- Exit_Statement = 211
- Case_Statement = 212
- Procedure_Call_Statement = 213
- If_Statement = 214
- Elsif = 215
- Character_Literal = 216
- Simple_Name = 217
- Selected_Name = 218
- Operator_Symbol = 219
- Reference_Name = 220
- External_Constant_Name = 221
- External_Signal_Name = 222
- External_Variable_Name = 223
- Selected_By_All_Name = 224
- Parenthesis_Name = 225
- Package_Pathname = 226
- Absolute_Pathname = 227
- Relative_Pathname = 228
- Pathname_Element = 229
- Base_Attribute = 230
- Subtype_Attribute = 231
- Element_Attribute = 232
- Left_Type_Attribute = 233
- Right_Type_Attribute = 234
- High_Type_Attribute = 235
- Low_Type_Attribute = 236
- Ascending_Type_Attribute = 237
- Image_Attribute = 238
- Value_Attribute = 239
- Pos_Attribute = 240
- Val_Attribute = 241
- Succ_Attribute = 242
- Pred_Attribute = 243
- Leftof_Attribute = 244
- Rightof_Attribute = 245
- Delayed_Attribute = 246
- Stable_Attribute = 247
- Quiet_Attribute = 248
- Transaction_Attribute = 249
- Event_Attribute = 250
- Active_Attribute = 251
- Last_Event_Attribute = 252
- Last_Active_Attribute = 253
- Last_Value_Attribute = 254
- Driving_Attribute = 255
- Driving_Value_Attribute = 256
- Behavior_Attribute = 257
- Structure_Attribute = 258
- Simple_Name_Attribute = 259
- Instance_Name_Attribute = 260
- Path_Name_Attribute = 261
- Left_Array_Attribute = 262
- Right_Array_Attribute = 263
- High_Array_Attribute = 264
- Low_Array_Attribute = 265
- Length_Array_Attribute = 266
- Ascending_Array_Attribute = 267
- Range_Array_Attribute = 268
- Reverse_Range_Array_Attribute = 269
- Attribute_Name = 270
+ Psl_Assert_Directive = 186
+ Psl_Assume_Directive = 187
+ Psl_Cover_Directive = 188
+ Psl_Restrict_Directive = 189
+ Block_Statement = 190
+ If_Generate_Statement = 191
+ Case_Generate_Statement = 192
+ For_Generate_Statement = 193
+ Component_Instantiation_Statement = 194
+ Psl_Default_Clock = 195
+ Simple_Simultaneous_Statement = 196
+ Generate_Statement_Body = 197
+ If_Generate_Else_Clause = 198
+ Simple_Signal_Assignment_Statement = 199
+ Conditional_Signal_Assignment_Statement = 200
+ Selected_Waveform_Assignment_Statement = 201
+ Null_Statement = 202
+ Assertion_Statement = 203
+ Report_Statement = 204
+ Wait_Statement = 205
+ Variable_Assignment_Statement = 206
+ Conditional_Variable_Assignment_Statement = 207
+ Return_Statement = 208
+ For_Loop_Statement = 209
+ While_Loop_Statement = 210
+ Next_Statement = 211
+ Exit_Statement = 212
+ Case_Statement = 213
+ Procedure_Call_Statement = 214
+ If_Statement = 215
+ Elsif = 216
+ Character_Literal = 217
+ Simple_Name = 218
+ Selected_Name = 219
+ Operator_Symbol = 220
+ Reference_Name = 221
+ External_Constant_Name = 222
+ External_Signal_Name = 223
+ External_Variable_Name = 224
+ Selected_By_All_Name = 225
+ Parenthesis_Name = 226
+ Package_Pathname = 227
+ Absolute_Pathname = 228
+ Relative_Pathname = 229
+ Pathname_Element = 230
+ Base_Attribute = 231
+ Subtype_Attribute = 232
+ Element_Attribute = 233
+ Left_Type_Attribute = 234
+ Right_Type_Attribute = 235
+ High_Type_Attribute = 236
+ Low_Type_Attribute = 237
+ Ascending_Type_Attribute = 238
+ Image_Attribute = 239
+ Value_Attribute = 240
+ Pos_Attribute = 241
+ Val_Attribute = 242
+ Succ_Attribute = 243
+ Pred_Attribute = 244
+ Leftof_Attribute = 245
+ Rightof_Attribute = 246
+ Delayed_Attribute = 247
+ Stable_Attribute = 248
+ Quiet_Attribute = 249
+ Transaction_Attribute = 250
+ Event_Attribute = 251
+ Active_Attribute = 252
+ Last_Event_Attribute = 253
+ Last_Active_Attribute = 254
+ Last_Value_Attribute = 255
+ Driving_Attribute = 256
+ Driving_Value_Attribute = 257
+ Behavior_Attribute = 258
+ Structure_Attribute = 259
+ Simple_Name_Attribute = 260
+ Instance_Name_Attribute = 261
+ Path_Name_Attribute = 262
+ Left_Array_Attribute = 263
+ Right_Array_Attribute = 264
+ High_Array_Attribute = 265
+ Low_Array_Attribute = 266
+ Length_Array_Attribute = 267
+ Ascending_Array_Attribute = 268
+ Range_Array_Attribute = 269
+ Reverse_Range_Array_Attribute = 270
+ Attribute_Name = 271
class Iir_Kinds:
@@ -457,7 +458,8 @@ class Iir_Kinds:
Iir_Kind.Concurrent_Selected_Signal_Assignment,
Iir_Kind.Concurrent_Assertion_Statement,
Iir_Kind.Concurrent_Procedure_Call_Statement,
- Iir_Kind.Psl_Assert_Statement,
+ Iir_Kind.Psl_Assert_Directive,
+ Iir_Kind.Psl_Assume_Directive,
Iir_Kind.Psl_Cover_Directive,
Iir_Kind.Psl_Restrict_Directive]
@@ -649,7 +651,8 @@ class Iir_Kinds:
Iir_Kind.Concurrent_Selected_Signal_Assignment,
Iir_Kind.Concurrent_Assertion_Statement,
Iir_Kind.Concurrent_Procedure_Call_Statement,
- Iir_Kind.Psl_Assert_Statement,
+ Iir_Kind.Psl_Assert_Directive,
+ Iir_Kind.Psl_Assume_Directive,
Iir_Kind.Psl_Cover_Directive,
Iir_Kind.Psl_Restrict_Directive,
Iir_Kind.Block_Statement,
@@ -1129,6 +1132,9 @@ class Iir_Predefined:
Ieee_Std_Logic_Unsigned_Eq_Slv_Slv = 265
Ieee_Std_Logic_Unsigned_Eq_Slv_Int = 266
Ieee_Std_Logic_Unsigned_Eq_Int_Slv = 267
+ Ieee_Std_Logic_Unsigned_Ne_Slv_Slv = 268
+ Ieee_Std_Logic_Unsigned_Ne_Slv_Int = 269
+ Ieee_Std_Logic_Unsigned_Ne_Int_Slv = 270
Get_Kind = libghdl.vhdl__nodes__get_kind
Get_Location = libghdl.vhdl__nodes__get_location
diff --git a/python/libghdl/thin/vhdl/tokens.py b/python/libghdl/thin/vhdl/tokens.py
index 20cf3b7dd..2d5655001 100644
--- a/python/libghdl/thin/vhdl/tokens.py
+++ b/python/libghdl/thin/vhdl/tokens.py
@@ -180,26 +180,27 @@ class Tok:
Psl_Property = 176
Psl_Sequence = 177
Psl_Endpoint = 178
- Psl_Cover = 179
- Psl_Restrict = 180
- Psl_Restrict_Guarantee = 181
- Psl_Const = 182
- Psl_Boolean = 183
- Inf = 184
- Within = 185
- Abort = 186
- Before = 187
- Before_Em = 188
- Before_Un = 189
- Before_Em_Un = 190
- Until_Em = 191
- Until_Un = 192
- Until_Em_Un = 193
- Always = 194
- Never = 195
- Eventually = 196
- Next_A = 197
- Next_E = 198
- Next_Event = 199
- Next_Event_A = 200
- Next_Event_E = 201
+ Psl_Assume = 179
+ Psl_Cover = 180
+ Psl_Restrict = 181
+ Psl_Restrict_Guarantee = 182
+ Psl_Const = 183
+ Psl_Boolean = 184
+ Inf = 185
+ Within = 186
+ Abort = 187
+ Before = 188
+ Before_Em = 189
+ Before_Un = 190
+ Before_Em_Un = 191
+ Until_Em = 192
+ Until_Un = 193
+ Until_Em_Un = 194
+ Always = 195
+ Never = 196
+ Eventually = 197
+ Next_A = 198
+ Next_E = 199
+ Next_Event = 200
+ Next_Event_A = 201
+ Next_Event_E = 202
diff --git a/src/ghdldrv/ghdlprint.adb b/src/ghdldrv/ghdlprint.adb
index 6c5cd5873..a611f07e7 100644
--- a/src/ghdldrv/ghdlprint.adb
+++ b/src/ghdldrv/ghdlprint.adb
@@ -395,6 +395,7 @@ package body Ghdlprint is
| Tok_Psl_Property
| Tok_Psl_Sequence
| Tok_Psl_Endpoint
+ | Tok_Psl_Assume
| Tok_Psl_Cover
| Tok_Psl_Restrict
| Tok_Psl_Restrict_Guarantee
diff --git a/src/ghdldrv/ghdlrun.adb b/src/ghdldrv/ghdlrun.adb
index f82de30e0..46445b135 100644
--- a/src/ghdldrv/ghdlrun.adb
+++ b/src/ghdldrv/ghdlrun.adb
@@ -341,6 +341,8 @@ package body Ghdlrun is
Grt.Lib.Ghdl_Ieee_Assert_Failed'Address);
Def (Trans_Decls.Ghdl_Psl_Assert_Failed,
Grt.Lib.Ghdl_Psl_Assert_Failed'Address);
+ Def (Trans_Decls.Ghdl_Psl_Assume_Failed,
+ Grt.Lib.Ghdl_Psl_Assume_Failed'Address);
Def (Trans_Decls.Ghdl_Psl_Cover,
Grt.Lib.Ghdl_Psl_Cover'Address);
Def (Trans_Decls.Ghdl_Psl_Cover_Failed,
diff --git a/src/grt/grt-disp_rti.adb b/src/grt/grt-disp_rti.adb
index b3b595668..b908a3c3b 100644
--- a/src/grt/grt-disp_rti.adb
+++ b/src/grt/grt-disp_rti.adb
@@ -470,6 +470,8 @@ package body Grt.Disp_Rti is
when Ghdl_Rtik_Psl_Assert =>
Put ("ghdl_rtik_psl_assert");
+ when Ghdl_Rtik_Psl_Assume =>
+ Put ("ghdl_rtik_psl_assume");
when Ghdl_Rtik_Psl_Cover =>
Put ("ghdl_rtik_psl_cover");
when Ghdl_Rtik_Psl_Endpoint =>
@@ -1310,6 +1312,7 @@ package body Grt.Disp_Rti is
Disp_Type_Protected
(To_Ghdl_Rtin_Type_Scalar_Acc (Rti), Ctxt, Indent);
when Ghdl_Rtik_Psl_Cover
+ | Ghdl_Rtik_Psl_Assume
| Ghdl_Rtik_Psl_Assert =>
Disp_Psl_Directive (To_Ghdl_Rtin_Object_Acc (Rti), Ctxt, Indent);
when Ghdl_Rtik_Psl_Endpoint =>
diff --git a/src/grt/grt-lib.adb b/src/grt/grt-lib.adb
index 26491a7ad..149f218eb 100644
--- a/src/grt/grt-lib.adb
+++ b/src/grt/grt-lib.adb
@@ -116,6 +116,12 @@ package body Grt.Lib is
Do_Report ("psl assertion", Str, "Assertion violation", Severity, Loc);
end Ghdl_Psl_Assert_Failed;
+ procedure Ghdl_Psl_Assume_Failed
+ (Str : Std_String_Ptr; Severity : Integer; Loc : Ghdl_Location_Ptr) is
+ begin
+ Do_Report ("psl assumption", Str, "Assumption violation", Severity, Loc);
+ end Ghdl_Psl_Assume_Failed;
+
procedure Ghdl_Psl_Cover
(Str : Std_String_Ptr; Severity : Integer; Loc : Ghdl_Location_Ptr) is
begin
diff --git a/src/grt/grt-lib.ads b/src/grt/grt-lib.ads
index 167ea98e5..1f5e020d4 100644
--- a/src/grt/grt-lib.ads
+++ b/src/grt/grt-lib.ads
@@ -40,6 +40,11 @@ package Grt.Lib is
Severity : Integer;
Loc : Ghdl_Location_Ptr);
+ procedure Ghdl_Psl_Assume_Failed
+ (Str : Std_String_Ptr;
+ Severity : Integer;
+ Loc : Ghdl_Location_Ptr);
+
-- Called when a sequence is covered (in a cover directive)
procedure Ghdl_Psl_Cover
(Str : Std_String_Ptr; Severity : Integer; Loc : Ghdl_Location_Ptr);
@@ -116,6 +121,7 @@ private
pragma Export (C, Ghdl_Assert_Failed, "__ghdl_assert_failed");
pragma Export (C, Ghdl_Ieee_Assert_Failed, "__ghdl_ieee_assert_failed");
+ pragma Export (C, Ghdl_Psl_Assume_Failed, "__ghdl_psl_assume_failed");
pragma Export (C, Ghdl_Psl_Assert_Failed, "__ghdl_psl_assert_failed");
pragma Export (C, Ghdl_Psl_Cover, "__ghdl_psl_cover");
pragma Export (C, Ghdl_Psl_Cover_Failed, "__ghdl_psl_cover_failed");
diff --git a/src/grt/grt-psl.adb b/src/grt/grt-psl.adb
index cf603a097..1fd3ad94f 100644
--- a/src/grt/grt-psl.adb
+++ b/src/grt/grt-psl.adb
@@ -40,6 +40,8 @@ package body Grt.Psl is
Is_First : Boolean := True;
Nbr_Assert_Failed : Ghdl_U32 := 0;
Nbr_Assert_Passed : Ghdl_U32 := 0;
+ Nbr_Assume_Failed : Ghdl_U32 := 0;
+ Nbr_Assume_Passed : Ghdl_U32 := 0;
Nbr_Cover_Failed : Ghdl_U32 := 0;
Nbr_Cover_Passed : Ghdl_U32 := 0;
@@ -96,6 +98,8 @@ package body Grt.Psl is
case Ghdl_Rtiks_Psl (Rti.Kind) is
when Ghdl_Rtik_Psl_Assert =>
Put (F, """assertion""");
+ when Ghdl_Rtik_Psl_Assume =>
+ Put (F, """assumption""");
when Ghdl_Rtik_Psl_Cover =>
Put (F, """cover""");
end case;
@@ -130,6 +134,14 @@ package body Grt.Psl is
Put (F, "failed");
Inc (Nbr_Assert_Failed);
end if;
+ when Ghdl_Rtik_Psl_Assume =>
+ if Val = 0 then
+ Put (F, "passed");
+ Inc (Nbr_Assume_Passed);
+ else
+ Put (F, "failed");
+ Inc (Nbr_Assume_Failed);
+ end if;
when Ghdl_Rtik_Psl_Cover =>
if Val = 0 then
Put (F, "not covered");
@@ -186,6 +198,16 @@ package body Grt.Psl is
Put_U32 (F, Nbr_Assert_Passed);
Put_Line (F, ",");
+ Put (F, " ""assume"": ");
+ Put_U32 (F, Nbr_Assume_Failed + Nbr_Assume_Passed);
+ Put_Line (F, ",");
+ Put (F, " ""assume-failure"": ");
+ Put_U32 (F, Nbr_Assume_Failed);
+ Put_Line (F, ",");
+ Put (F, " ""assume-pass"": ");
+ Put_U32 (F, Nbr_Assume_Passed);
+ Put_Line (F, ",");
+
Put (F, " ""cover"": ");
Put_U32 (F, Nbr_Cover_Failed + Nbr_Cover_Passed);
Put_Line (F, ",");
diff --git a/src/grt/grt-rtis.ads b/src/grt/grt-rtis.ads
index 030cd7e04..d4664492f 100644
--- a/src/grt/grt-rtis.ads
+++ b/src/grt/grt-rtis.ads
@@ -94,6 +94,7 @@ package Grt.Rtis is
Ghdl_Rtik_Attribute_Stable,
Ghdl_Rtik_Psl_Assert,
+ Ghdl_Rtik_Psl_Assume,
Ghdl_Rtik_Psl_Cover,
Ghdl_Rtik_Psl_Endpoint,
diff --git a/src/vhdl/simulate/simul-elaboration.adb b/src/vhdl/simulate/simul-elaboration.adb
index 61048392b..f165662c2 100644
--- a/src/vhdl/simulate/simul-elaboration.adb
+++ b/src/vhdl/simulate/simul-elaboration.adb
@@ -1897,7 +1897,8 @@ package body Simul.Elaboration is
null;
when Iir_Kind_Psl_Cover_Directive
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Endpoint_Declaration =>
Elaborate_Psl_Directive (Instance, Stmt);
diff --git a/src/vhdl/simulate/simul-simulation-main.adb b/src/vhdl/simulate/simul-simulation-main.adb
index 5af8acb55..d6c6ba0ff 100644
--- a/src/vhdl/simulate/simul-simulation-main.adb
+++ b/src/vhdl/simulate/simul-simulation-main.adb
@@ -477,12 +477,18 @@ package body Simul.Simulation.Main is
S_Num := Get_State_Label (S);
pragma Assert (S_Num = Get_PSL_Nbr_States (E.Stmt) - 1);
case Get_Kind (E.Stmt) is
- when Iir_Kind_Psl_Assert_Statement =>
+ when Iir_Kind_Psl_Assume_Directive =>
if Nvec (S_Num) then
Execute_Failed_Assertion
(E.Instance, "psl assertion", E.Stmt,
"assertion violation", 2);
end if;
+ when Iir_Kind_Psl_Assume_Directive =>
+ if Nvec (S_Num) then
+ Execute_Failed_Assertion
+ (E.Instance, "psl assumption", E.Stmt,
+ "assumption violation", 2);
+ end if;
when Iir_Kind_Psl_Cover_Directive =>
if Nvec (S_Num) then
if Get_Report_Expression (E.Stmt) /= Null_Iir then
@@ -563,7 +569,8 @@ package body Simul.Simulation.Main is
(E.Instance, Get_PSL_Clock_Sensitivity (E.Stmt));
case Get_Kind (E.Stmt) is
- when Iir_Kind_Psl_Assert_Statement =>
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive =>
if Get_PSL_EOS_Flag (E.Stmt) then
Grt.Processes.Ghdl_Finalize_Register
(To_Instance_Acc (E'Address),
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index b70a673a5..7a2033624 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -644,9 +644,12 @@ package body Trans.Chap9 is
Start_If_Stmt (S_Blk, Cond);
Open_Temp;
case Get_Kind (Stmt) is
- when Iir_Kind_Psl_Assert_Statement =>
+ when Iir_Kind_Psl_Assert_Directive =>
Chap8.Translate_Report
(Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error);
+ when Iir_Kind_Psl_Assume_Directive =>
+ Chap8.Translate_Report
+ (Stmt, Ghdl_Psl_Assume_Failed, Severity_Level_Error);
when Iir_Kind_Psl_Cover_Directive =>
if Get_Report_Expression (Stmt) /= Null_Iir then
Start_Association (Assocs, Report_Proc);
@@ -697,7 +700,8 @@ package body Trans.Chap9 is
-- The finalizer.
case Get_Kind (Stmt) is
- when Iir_Kind_Psl_Assert_Statement =>
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive =>
if Get_PSL_EOS_Flag (Stmt) then
Create_Psl_Final_Proc (Stmt, Base, Instance);
@@ -724,8 +728,13 @@ package body Trans.Chap9 is
(ON_And, Cond,
Translate_Psl_Expr (Get_Edge_Expr (E), True));
Start_If_Stmt (E_Blk, Cond);
- Chap8.Translate_Report
- (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error);
+ if Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Directive then
+ Chap8.Translate_Report
+ (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error);
+ else
+ Chap8.Translate_Report
+ (Stmt, Ghdl_Psl_Assume_Failed, Severity_Level_Error);
+ end if;
New_Return_Stmt;
Finish_If_Stmt (E_Blk);
@@ -974,7 +983,8 @@ package body Trans.Chap9 is
null;
when Iir_Kind_Psl_Declaration =>
null;
- when Iir_Kind_Psl_Assert_Statement
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Endpoint_Declaration =>
Translate_Psl_Directive_Declarations (El);
@@ -1122,7 +1132,8 @@ package body Trans.Chap9 is
null;
when Iir_Kind_Psl_Declaration =>
null;
- when Iir_Kind_Psl_Assert_Statement
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Endpoint_Declaration =>
Translate_Psl_Directive_Statement (Stmt, Base_Info);
@@ -2721,7 +2732,8 @@ package body Trans.Chap9 is
when Iir_Kind_Psl_Declaration
| Iir_Kind_Psl_Endpoint_Declaration =>
null;
- when Iir_Kind_Psl_Assert_Statement
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive =>
null;
when Iir_Kind_Component_Instantiation_Statement =>
@@ -2783,7 +2795,8 @@ package body Trans.Chap9 is
null;
when Iir_Kind_Psl_Declaration =>
null;
- when Iir_Kind_Psl_Assert_Statement
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Endpoint_Declaration =>
Elab_Psl_Directive (Stmt, Base_Info);
diff --git a/src/vhdl/translate/trans-rtis.adb b/src/vhdl/translate/trans-rtis.adb
index 96aacb8b0..e618aeb9b 100644
--- a/src/vhdl/translate/trans-rtis.adb
+++ b/src/vhdl/translate/trans-rtis.adb
@@ -322,6 +322,9 @@ package body Trans.Rtis is
(Constr, Get_Identifier ("__ghdl_rtik_psl_assert"),
Ghdl_Rtik_Psl_Assert);
New_Enum_Literal
+ (Constr, Get_Identifier ("__ghdl_rtik_psl_assume"),
+ Ghdl_Rtik_Psl_Assume);
+ New_Enum_Literal
(Constr, Get_Identifier ("__ghdl_rtik_psl_cover"),
Ghdl_Rtik_Psl_Cover);
New_Enum_Literal
@@ -2042,8 +2045,10 @@ package body Trans.Rtis is
case Get_Kind (Decl) is
when Iir_Kind_Psl_Cover_Directive =>
Kind := Ghdl_Rtik_Psl_Cover;
- when Iir_Kind_Psl_Assert_Statement =>
+ when Iir_Kind_Psl_Assert_Directive =>
Kind := Ghdl_Rtik_Psl_Assert;
+ when Iir_Kind_Psl_Assume_Directive =>
+ Kind := Ghdl_Rtik_Psl_Assume;
when Iir_Kind_Psl_Endpoint_Declaration =>
Kind := Ghdl_Rtik_Psl_Endpoint;
when others =>
@@ -2422,7 +2427,8 @@ package body Trans.Rtis is
null;
when Iir_Kind_Psl_Declaration =>
null;
- when Iir_Kind_Psl_Assert_Statement
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Endpoint_Declaration =>
Generate_Psl_Directive (Stmt);
@@ -2994,7 +3000,8 @@ package body Trans.Rtis is
when Iir_Kind_Process_Statement
| Iir_Kind_Sensitized_Process_Statement =>
return Node_Info.Process_Rti_Const;
- when Iir_Kind_Psl_Assert_Statement
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Endpoint_Declaration =>
return Node_Info.Psl_Rti_Const;
@@ -3035,7 +3042,8 @@ package body Trans.Rtis is
when Iir_Kind_Process_Statement
| Iir_Kind_Sensitized_Process_Statement =>
Ref := Get_Instance_Ref (Node_Info.Process_Scope);
- when Iir_Kind_Psl_Assert_Statement
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Endpoint_Declaration =>
Ref := Get_Instance_Ref (Node_Info.Psl_Scope);
diff --git a/src/vhdl/translate/trans-rtis.ads b/src/vhdl/translate/trans-rtis.ads
index e3c8c188e..1e4dd36ef 100644
--- a/src/vhdl/translate/trans-rtis.ads
+++ b/src/vhdl/translate/trans-rtis.ads
@@ -70,6 +70,7 @@ package Trans.Rtis is
Ghdl_Rtik_Attribute_Quiet : O_Cnode;
Ghdl_Rtik_Attribute_Stable : O_Cnode;
Ghdl_Rtik_Psl_Assert : O_Cnode;
+ Ghdl_Rtik_Psl_Assume : O_Cnode;
Ghdl_Rtik_Psl_Cover : O_Cnode;
Ghdl_Rtik_Psl_Endpoint : O_Cnode;
Ghdl_Rtik_Error : O_Cnode;
diff --git a/src/vhdl/translate/trans_decls.ads b/src/vhdl/translate/trans_decls.ads
index 38d3be7e7..d76b1b896 100644
--- a/src/vhdl/translate/trans_decls.ads
+++ b/src/vhdl/translate/trans_decls.ads
@@ -25,6 +25,7 @@ package Trans_Decls is
Ghdl_Check_Stack_Allocation : O_Dnode;
+ Ghdl_Psl_Assume_Failed : O_Dnode;
Ghdl_Psl_Cover : O_Dnode;
Ghdl_Psl_Cover_Failed : O_Dnode;
-- Procedure for report statement.
diff --git a/src/vhdl/translate/translation.adb b/src/vhdl/translate/translation.adb
index de83ba132..863acd37d 100644
--- a/src/vhdl/translate/translation.adb
+++ b/src/vhdl/translate/translation.adb
@@ -1077,6 +1077,8 @@ package body Translation is
("__ghdl_ieee_assert_failed", Ghdl_Ieee_Assert_Failed);
Create_Report_Subprg ("__ghdl_psl_assert_failed",
Ghdl_Psl_Assert_Failed);
+ Create_Report_Subprg ("__ghdl_psl_assume_failed",
+ Ghdl_Psl_Assume_Failed);
Create_Report_Subprg ("__ghdl_psl_cover", Ghdl_Psl_Cover);
Create_Report_Subprg ("__ghdl_psl_cover_failed",
Ghdl_Psl_Cover_Failed);
diff --git a/src/vhdl/vhdl-annotations.adb b/src/vhdl/vhdl-annotations.adb
index cb44f98f0..7e2d19a58 100644
--- a/src/vhdl/vhdl-annotations.adb
+++ b/src/vhdl/vhdl-annotations.adb
@@ -1083,7 +1083,8 @@ package body Vhdl.Annotations is
null;
when Iir_Kind_Psl_Cover_Directive
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Restrict_Directive =>
null;
when Iir_Kind_Psl_Endpoint_Declaration =>
diff --git a/src/vhdl/vhdl-canon.adb b/src/vhdl/vhdl-canon.adb
index 4dbb03c4c..6dd40560b 100644
--- a/src/vhdl/vhdl-canon.adb
+++ b/src/vhdl/vhdl-canon.adb
@@ -2125,7 +2125,8 @@ package body Vhdl.Canon is
(Top, Get_Generate_Statement_Body (El));
end;
- when Iir_Kind_Psl_Assert_Statement =>
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive=>
declare
Prop : PSL_Node;
Fa : PSL_NFA;
diff --git a/src/vhdl/vhdl-elocations.adb b/src/vhdl/vhdl-elocations.adb
index c4dd2f1b6..6965457d6 100644
--- a/src/vhdl/vhdl-elocations.adb
+++ b/src/vhdl/vhdl-elocations.adb
@@ -342,7 +342,8 @@ package body Vhdl.Elocations is
| Iir_Kind_Psl_Expression
| Iir_Kind_Concurrent_Assertion_Statement
| Iir_Kind_Concurrent_Procedure_Call_Statement
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive
| Iir_Kind_Case_Generate_Statement
diff --git a/src/vhdl/vhdl-elocations.ads b/src/vhdl/vhdl-elocations.ads
index 286ba751c..84be78e93 100644
--- a/src/vhdl/vhdl-elocations.ads
+++ b/src/vhdl/vhdl-elocations.ads
@@ -404,7 +404,8 @@ package Vhdl.Elocations is
-- Iir_Kind_Psl_Default_Clock (None)
- -- Iir_Kind_Psl_Assert_Statement (None)
+ -- Iir_Kind_Psl_Assert_Directive (None)
+ -- Iir_Kind_Psl_Assume_Directive (None)
-- Iir_Kind_Psl_Cover_Directive (None)
-- Iir_Kind_Psl_Restrict_Directive (None)
diff --git a/src/vhdl/vhdl-errors.adb b/src/vhdl/vhdl-errors.adb
index 57be65311..ada8258af 100644
--- a/src/vhdl/vhdl-errors.adb
+++ b/src/vhdl/vhdl-errors.adb
@@ -687,8 +687,10 @@ package body Vhdl.Errors is
(Node, "concurrent selected signal assignment");
when Iir_Kind_Concurrent_Assertion_Statement =>
return Disp_Label (Node, "concurrent assertion");
- when Iir_Kind_Psl_Assert_Statement =>
+ when Iir_Kind_Psl_Assert_Directive =>
return Disp_Label (Node, "PSL assertion");
+ when Iir_Kind_Psl_Assume_Directive =>
+ return Disp_Label (Node, "PSL assumption");
when Iir_Kind_Psl_Cover_Directive =>
return Disp_Label (Node, "PSL cover");
when Iir_Kind_Psl_Restrict_Directive =>
diff --git a/src/vhdl/vhdl-nodes.adb b/src/vhdl/vhdl-nodes.adb
index dfb9629af..780f13b5b 100644
--- a/src/vhdl/vhdl-nodes.adb
+++ b/src/vhdl/vhdl-nodes.adb
@@ -1235,7 +1235,8 @@ package body Vhdl.Nodes is
| Iir_Kind_Concurrent_Simple_Signal_Assignment
| Iir_Kind_Concurrent_Conditional_Signal_Assignment
| Iir_Kind_Concurrent_Selected_Signal_Assignment
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive
| Iir_Kind_Block_Statement
diff --git a/src/vhdl/vhdl-nodes.ads b/src/vhdl/vhdl-nodes.ads
index a884f7b9d..58dce712a 100644
--- a/src/vhdl/vhdl-nodes.ads
+++ b/src/vhdl/vhdl-nodes.ads
@@ -2902,12 +2902,16 @@ package Vhdl.Nodes is
-- Get/Set_Label (Field3)
-- Get/Set_Identifier (Alias Field3)
- -- Iir_Kind_Psl_Assert_Statement (Medium)
+ -- Iir_Kind_Psl_Assert_Directive (Medium)
+ -- Iir_Kind_Psl_Assume_Directive (Medium)
-- Iir_Kind_Psl_Cover_Directive (Medium)
--
-- Get/Set_Parent (Field0)
--
- -- Only for Iir_Kind_Psl_Assert_Statement:
+ -- Only for Iir_Kind_Psl_Assert_Directive:
+ -- Get/Set_Psl_Property (Field1)
+ --
+ -- Only for Iir_Kind_Psl_Assume_Directive:
-- Get/Set_Psl_Property (Field1)
--
-- Only for Iir_Kind_Psl_Cover_Directive:
@@ -4377,7 +4381,8 @@ package Vhdl.Nodes is
Iir_Kind_Concurrent_Selected_Signal_Assignment,
Iir_Kind_Concurrent_Assertion_Statement,
Iir_Kind_Concurrent_Procedure_Call_Statement,
- Iir_Kind_Psl_Assert_Statement,
+ Iir_Kind_Psl_Assert_Directive,
+ Iir_Kind_Psl_Assume_Directive,
Iir_Kind_Psl_Cover_Directive,
Iir_Kind_Psl_Restrict_Directive,
Iir_Kind_Block_Statement,
@@ -5569,7 +5574,8 @@ package Vhdl.Nodes is
--Iir_Kind_Concurrent_Selected_Signal_Assignment
--Iir_Kind_Concurrent_Assertion_Statement
--Iir_Kind_Concurrent_Procedure_Call_Statement
- --Iir_Kind_Psl_Assert_Statement
+ --Iir_Kind_Psl_Assert_Directive
+ --Iir_Kind_Psl_Assume_Directive
--Iir_Kind_Psl_Cover_Directive
--Iir_Kind_Psl_Restrict_Directive
--Iir_Kind_Block_Statement
@@ -5587,7 +5593,8 @@ package Vhdl.Nodes is
--Iir_Kind_Concurrent_Selected_Signal_Assignment
--Iir_Kind_Concurrent_Assertion_Statement
--Iir_Kind_Concurrent_Procedure_Call_Statement
- --Iir_Kind_Psl_Assert_Statement
+ --Iir_Kind_Psl_Assert_Directive
+ --Iir_Kind_Psl_Assume_Directive
--Iir_Kind_Psl_Cover_Directive
Iir_Kind_Psl_Restrict_Directive;
diff --git a/src/vhdl/vhdl-nodes_meta.adb b/src/vhdl/vhdl-nodes_meta.adb
index 2e3512028..4b4c6b632 100644
--- a/src/vhdl/vhdl-nodes_meta.adb
+++ b/src/vhdl/vhdl-nodes_meta.adb
@@ -1388,8 +1388,10 @@ package body Vhdl.Nodes_Meta is
return "concurrent_assertion_statement";
when Iir_Kind_Concurrent_Procedure_Call_Statement =>
return "concurrent_procedure_call_statement";
- when Iir_Kind_Psl_Assert_Statement =>
+ when Iir_Kind_Psl_Assert_Directive =>
return "psl_assert_statement";
+ when Iir_Kind_Psl_Assume_Directive =>
+ return "psl_assume_statement";
when Iir_Kind_Psl_Cover_Directive =>
return "psl_cover_directive";
when Iir_Kind_Psl_Restrict_Directive =>
@@ -3795,7 +3797,21 @@ package body Vhdl.Nodes_Meta is
Field_Parent,
Field_Procedure_Call,
Field_Chain,
- -- Iir_Kind_Psl_Assert_Statement
+ -- Iir_Kind_Psl_Assert_Directive
+ Field_Psl_Property,
+ Field_Label,
+ Field_PSL_Clock,
+ Field_PSL_NFA,
+ Field_PSL_Nbr_States,
+ Field_PSL_EOS_Flag,
+ Field_Postponed_Flag,
+ Field_Visible_Flag,
+ Field_Parent,
+ Field_Chain,
+ Field_Severity_Expression,
+ Field_Report_Expression,
+ Field_PSL_Clock_Sensitivity,
+ -- Iir_Kind_Psl_Assume_Directive
Field_Psl_Property,
Field_Label,
Field_PSL_Clock,
@@ -4640,91 +4656,92 @@ package body Vhdl.Nodes_Meta is
Iir_Kind_Concurrent_Selected_Signal_Assignment => 1370,
Iir_Kind_Concurrent_Assertion_Statement => 1378,
Iir_Kind_Concurrent_Procedure_Call_Statement => 1385,
- Iir_Kind_Psl_Assert_Statement => 1398,
- Iir_Kind_Psl_Cover_Directive => 1411,
- Iir_Kind_Psl_Restrict_Directive => 1422,
- Iir_Kind_Block_Statement => 1436,
- Iir_Kind_If_Generate_Statement => 1447,
- Iir_Kind_Case_Generate_Statement => 1456,
- Iir_Kind_For_Generate_Statement => 1465,
- Iir_Kind_Component_Instantiation_Statement => 1476,
- Iir_Kind_Psl_Default_Clock => 1480,
- Iir_Kind_Simple_Simultaneous_Statement => 1487,
- Iir_Kind_Generate_Statement_Body => 1498,
- Iir_Kind_If_Generate_Else_Clause => 1504,
- Iir_Kind_Simple_Signal_Assignment_Statement => 1514,
- Iir_Kind_Conditional_Signal_Assignment_Statement => 1524,
- Iir_Kind_Selected_Waveform_Assignment_Statement => 1535,
- Iir_Kind_Null_Statement => 1539,
- Iir_Kind_Assertion_Statement => 1546,
- Iir_Kind_Report_Statement => 1552,
- Iir_Kind_Wait_Statement => 1560,
- Iir_Kind_Variable_Assignment_Statement => 1567,
- Iir_Kind_Conditional_Variable_Assignment_Statement => 1574,
- Iir_Kind_Return_Statement => 1580,
- Iir_Kind_For_Loop_Statement => 1589,
- Iir_Kind_While_Loop_Statement => 1598,
- Iir_Kind_Next_Statement => 1605,
- Iir_Kind_Exit_Statement => 1612,
- Iir_Kind_Case_Statement => 1620,
- Iir_Kind_Procedure_Call_Statement => 1626,
- Iir_Kind_If_Statement => 1636,
- Iir_Kind_Elsif => 1642,
- Iir_Kind_Character_Literal => 1650,
- Iir_Kind_Simple_Name => 1658,
- Iir_Kind_Selected_Name => 1667,
- Iir_Kind_Operator_Symbol => 1673,
- Iir_Kind_Reference_Name => 1677,
- Iir_Kind_External_Constant_Name => 1685,
- Iir_Kind_External_Signal_Name => 1693,
- Iir_Kind_External_Variable_Name => 1702,
- Iir_Kind_Selected_By_All_Name => 1708,
- Iir_Kind_Parenthesis_Name => 1713,
- Iir_Kind_Package_Pathname => 1717,
- Iir_Kind_Absolute_Pathname => 1718,
- Iir_Kind_Relative_Pathname => 1719,
- Iir_Kind_Pathname_Element => 1724,
- Iir_Kind_Base_Attribute => 1726,
- Iir_Kind_Subtype_Attribute => 1731,
- Iir_Kind_Element_Attribute => 1736,
- Iir_Kind_Left_Type_Attribute => 1741,
- Iir_Kind_Right_Type_Attribute => 1746,
- Iir_Kind_High_Type_Attribute => 1751,
- Iir_Kind_Low_Type_Attribute => 1756,
- Iir_Kind_Ascending_Type_Attribute => 1761,
- Iir_Kind_Image_Attribute => 1767,
- Iir_Kind_Value_Attribute => 1773,
- Iir_Kind_Pos_Attribute => 1779,
- Iir_Kind_Val_Attribute => 1785,
- Iir_Kind_Succ_Attribute => 1791,
- Iir_Kind_Pred_Attribute => 1797,
- Iir_Kind_Leftof_Attribute => 1803,
- Iir_Kind_Rightof_Attribute => 1809,
- Iir_Kind_Delayed_Attribute => 1818,
- Iir_Kind_Stable_Attribute => 1827,
- Iir_Kind_Quiet_Attribute => 1836,
- Iir_Kind_Transaction_Attribute => 1845,
- Iir_Kind_Event_Attribute => 1849,
- Iir_Kind_Active_Attribute => 1853,
- Iir_Kind_Last_Event_Attribute => 1857,
- Iir_Kind_Last_Active_Attribute => 1861,
- Iir_Kind_Last_Value_Attribute => 1865,
- Iir_Kind_Driving_Attribute => 1869,
- Iir_Kind_Driving_Value_Attribute => 1873,
- Iir_Kind_Behavior_Attribute => 1873,
- Iir_Kind_Structure_Attribute => 1873,
- Iir_Kind_Simple_Name_Attribute => 1880,
- Iir_Kind_Instance_Name_Attribute => 1885,
- Iir_Kind_Path_Name_Attribute => 1890,
- Iir_Kind_Left_Array_Attribute => 1897,
- Iir_Kind_Right_Array_Attribute => 1904,
- Iir_Kind_High_Array_Attribute => 1911,
- Iir_Kind_Low_Array_Attribute => 1918,
- Iir_Kind_Length_Array_Attribute => 1925,
- Iir_Kind_Ascending_Array_Attribute => 1932,
- Iir_Kind_Range_Array_Attribute => 1939,
- Iir_Kind_Reverse_Range_Array_Attribute => 1946,
- Iir_Kind_Attribute_Name => 1955
+ Iir_Kind_Psl_Assert_Directive => 1398,
+ Iir_Kind_Psl_Assume_Directive => 1411,
+ Iir_Kind_Psl_Cover_Directive => 1424,
+ Iir_Kind_Psl_Restrict_Directive => 1435,
+ Iir_Kind_Block_Statement => 1449,
+ Iir_Kind_If_Generate_Statement => 1460,
+ Iir_Kind_Case_Generate_Statement => 1469,
+ Iir_Kind_For_Generate_Statement => 1478,
+ Iir_Kind_Component_Instantiation_Statement => 1489,
+ Iir_Kind_Psl_Default_Clock => 1493,
+ Iir_Kind_Simple_Simultaneous_Statement => 1500,
+ Iir_Kind_Generate_Statement_Body => 1511,
+ Iir_Kind_If_Generate_Else_Clause => 1517,
+ Iir_Kind_Simple_Signal_Assignment_Statement => 1527,
+ Iir_Kind_Conditional_Signal_Assignment_Statement => 1537,
+ Iir_Kind_Selected_Waveform_Assignment_Statement => 1548,
+ Iir_Kind_Null_Statement => 1552,
+ Iir_Kind_Assertion_Statement => 1559,
+ Iir_Kind_Report_Statement => 1565,
+ Iir_Kind_Wait_Statement => 1573,
+ Iir_Kind_Variable_Assignment_Statement => 1580,
+ Iir_Kind_Conditional_Variable_Assignment_Statement => 1587,
+ Iir_Kind_Return_Statement => 1593,
+ Iir_Kind_For_Loop_Statement => 1602,
+ Iir_Kind_While_Loop_Statement => 1611,
+ Iir_Kind_Next_Statement => 1618,
+ Iir_Kind_Exit_Statement => 1625,
+ Iir_Kind_Case_Statement => 1633,
+ Iir_Kind_Procedure_Call_Statement => 1639,
+ Iir_Kind_If_Statement => 1649,
+ Iir_Kind_Elsif => 1655,
+ Iir_Kind_Character_Literal => 1663,
+ Iir_Kind_Simple_Name => 1671,
+ Iir_Kind_Selected_Name => 1680,
+ Iir_Kind_Operator_Symbol => 1686,
+ Iir_Kind_Reference_Name => 1690,
+ Iir_Kind_External_Constant_Name => 1698,
+ Iir_Kind_External_Signal_Name => 1706,
+ Iir_Kind_External_Variable_Name => 1715,
+ Iir_Kind_Selected_By_All_Name => 1721,
+ Iir_Kind_Parenthesis_Name => 1726,
+ Iir_Kind_Package_Pathname => 1730,
+ Iir_Kind_Absolute_Pathname => 1731,
+ Iir_Kind_Relative_Pathname => 1732,
+ Iir_Kind_Pathname_Element => 1737,
+ Iir_Kind_Base_Attribute => 1739,
+ Iir_Kind_Subtype_Attribute => 1744,
+ Iir_Kind_Element_Attribute => 1749,
+ Iir_Kind_Left_Type_Attribute => 1754,
+ Iir_Kind_Right_Type_Attribute => 1759,
+ Iir_Kind_High_Type_Attribute => 1764,
+ Iir_Kind_Low_Type_Attribute => 1769,
+ Iir_Kind_Ascending_Type_Attribute => 1774,
+ Iir_Kind_Image_Attribute => 1780,
+ Iir_Kind_Value_Attribute => 1786,
+ Iir_Kind_Pos_Attribute => 1792,
+ Iir_Kind_Val_Attribute => 1798,
+ Iir_Kind_Succ_Attribute => 1804,
+ Iir_Kind_Pred_Attribute => 1810,
+ Iir_Kind_Leftof_Attribute => 1816,
+ Iir_Kind_Rightof_Attribute => 1822,
+ Iir_Kind_Delayed_Attribute => 1831,
+ Iir_Kind_Stable_Attribute => 1840,
+ Iir_Kind_Quiet_Attribute => 1849,
+ Iir_Kind_Transaction_Attribute => 1858,
+ Iir_Kind_Event_Attribute => 1862,
+ Iir_Kind_Active_Attribute => 1866,
+ Iir_Kind_Last_Event_Attribute => 1870,
+ Iir_Kind_Last_Active_Attribute => 1874,
+ Iir_Kind_Last_Value_Attribute => 1878,
+ Iir_Kind_Driving_Attribute => 1882,
+ Iir_Kind_Driving_Value_Attribute => 1886,
+ Iir_Kind_Behavior_Attribute => 1886,
+ Iir_Kind_Structure_Attribute => 1886,
+ Iir_Kind_Simple_Name_Attribute => 1893,
+ Iir_Kind_Instance_Name_Attribute => 1898,
+ Iir_Kind_Path_Name_Attribute => 1903,
+ Iir_Kind_Left_Array_Attribute => 1910,
+ Iir_Kind_Right_Array_Attribute => 1917,
+ Iir_Kind_High_Array_Attribute => 1924,
+ Iir_Kind_Low_Array_Attribute => 1931,
+ Iir_Kind_Length_Array_Attribute => 1938,
+ Iir_Kind_Ascending_Array_Attribute => 1945,
+ Iir_Kind_Range_Array_Attribute => 1952,
+ Iir_Kind_Reverse_Range_Array_Attribute => 1959,
+ Iir_Kind_Attribute_Name => 1968
);
function Get_Fields_First (K : Iir_Kind) return Fields_Index is
@@ -7393,7 +7410,8 @@ package body Vhdl.Nodes_Meta is
| Iir_Kind_Concurrent_Selected_Signal_Assignment
| Iir_Kind_Concurrent_Assertion_Statement
| Iir_Kind_Concurrent_Procedure_Call_Statement
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive
| Iir_Kind_Block_Statement
@@ -8172,7 +8190,8 @@ package body Vhdl.Nodes_Meta is
| Iir_Kind_Concurrent_Selected_Signal_Assignment
| Iir_Kind_Concurrent_Assertion_Statement
| Iir_Kind_Concurrent_Procedure_Call_Statement
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive
| Iir_Kind_Block_Statement
@@ -8223,7 +8242,8 @@ package body Vhdl.Nodes_Meta is
| Iir_Kind_Concurrent_Selected_Signal_Assignment
| Iir_Kind_Concurrent_Assertion_Statement
| Iir_Kind_Concurrent_Procedure_Call_Statement
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive
| Iir_Kind_Block_Statement
@@ -8309,7 +8329,8 @@ package body Vhdl.Nodes_Meta is
| Iir_Kind_Concurrent_Selected_Signal_Assignment
| Iir_Kind_Concurrent_Assertion_Statement
| Iir_Kind_Concurrent_Procedure_Call_Statement
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive
| Iir_Kind_Block_Statement
@@ -8777,7 +8798,8 @@ package body Vhdl.Nodes_Meta is
| Iir_Kind_Concurrent_Selected_Signal_Assignment
| Iir_Kind_Concurrent_Assertion_Statement
| Iir_Kind_Concurrent_Procedure_Call_Statement
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive =>
return True;
@@ -9035,7 +9057,8 @@ package body Vhdl.Nodes_Meta is
begin
case K is
when Iir_Kind_Concurrent_Assertion_Statement
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Assertion_Statement
| Iir_Kind_Report_Statement =>
@@ -9049,7 +9072,8 @@ package body Vhdl.Nodes_Meta is
begin
case K is
when Iir_Kind_Concurrent_Assertion_Statement
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Assertion_Statement
| Iir_Kind_Report_Statement =>
@@ -9393,7 +9417,8 @@ package body Vhdl.Nodes_Meta is
| Iir_Kind_Concurrent_Selected_Signal_Assignment
| Iir_Kind_Concurrent_Assertion_Statement
| Iir_Kind_Concurrent_Procedure_Call_Statement
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive
| Iir_Kind_Block_Statement
@@ -10759,7 +10784,13 @@ package body Vhdl.Nodes_Meta is
function Has_Psl_Property (K : Iir_Kind) return Boolean is
begin
- return K = Iir_Kind_Psl_Assert_Statement;
+ case K is
+ when Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive =>
+ return True;
+ when others =>
+ return False;
+ end case;
end Has_Psl_Property;
function Has_Psl_Sequence (K : Iir_Kind) return Boolean is
@@ -10799,7 +10830,8 @@ package body Vhdl.Nodes_Meta is
case K is
when Iir_Kind_Psl_Declaration
| Iir_Kind_Psl_Endpoint_Declaration
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive =>
return True;
@@ -10813,7 +10845,8 @@ package body Vhdl.Nodes_Meta is
case K is
when Iir_Kind_Psl_Declaration
| Iir_Kind_Psl_Endpoint_Declaration
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive =>
return True;
@@ -10826,7 +10859,8 @@ package body Vhdl.Nodes_Meta is
begin
case K is
when Iir_Kind_Psl_Endpoint_Declaration
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive =>
return True;
@@ -10839,7 +10873,8 @@ package body Vhdl.Nodes_Meta is
begin
case K is
when Iir_Kind_Psl_Endpoint_Declaration
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive =>
return True;
@@ -10852,7 +10887,8 @@ package body Vhdl.Nodes_Meta is
begin
case K is
when Iir_Kind_Psl_Endpoint_Declaration
- | Iir_Kind_Psl_Assert_Statement
+ | Iir_Kind_Psl_Assert_Directive
+ | Iir_Kind_Psl_Assume_Directive
| Iir_Kind_Psl_Cover_Directive
| Iir_Kind_Psl_Restrict_Directive =>
return True;
diff --git a/src/vhdl/vhdl-parse.adb b/src/vhdl/vhdl-parse.adb
index e182821ae..491d14b85 100644
--- a/src/vhdl/vhdl-parse.adb
+++ b/src/vhdl/vhdl-parse.adb
@@ -8586,11 +8586,11 @@ package body Vhdl.Parse is
Expect_Scan (Tok_Semi_Colon);
end Parse_Psl_Assert_Report_Severity;
- function Parse_Psl_Assert_Statement return Iir
+ function Parse_Psl_Assert_Directive return Iir
is
Res : Iir;
begin
- Res := Create_Iir (Iir_Kind_Psl_Assert_Statement);
+ Res := Create_Iir (Iir_Kind_Psl_Assert_Directive);
-- Accept PSL tokens
if Flags.Vhdl_Std >= Vhdl_08 then
@@ -8605,7 +8605,26 @@ package body Vhdl.Parse is
Parse_Psl_Assert_Report_Severity (Res);
return Res;
- end Parse_Psl_Assert_Statement;
+ end Parse_Psl_Assert_Directive;
+
+ function Parse_Psl_Assume_Directive return Iir
+ is
+ Res : Iir;
+ begin
+ Res := Create_Iir (Iir_Kind_Psl_Assume_Directive);
+
+ -- Skip 'assume'
+ Scan;
+
+ Set_Psl_Property (Res, Parse_Psl.Parse_Psl_Property);
+
+ Vhdl.Scanner.Flag_Psl := False;
+ Vhdl.Scanner.Flag_Scan_In_Comment := False;
+
+ Expect_Scan (Tok_Semi_Colon);
+
+ return Res;
+ end Parse_Psl_Assume_Directive;
function Parse_Psl_Cover_Directive return Iir
is
@@ -8758,7 +8777,7 @@ package body Vhdl.Parse is
if Vhdl_Std >= Vhdl_08
or else (Flag_Psl_Comment and then Flag_Scan_In_Comment)
then
- Stmt := Parse_Psl_Assert_Statement;
+ Stmt := Parse_Psl_Assert_Directive;
else
Stmt := Create_Iir (Iir_Kind_Concurrent_Assertion_Statement);
Parse_Assertion (Stmt);
@@ -8804,6 +8823,9 @@ package body Vhdl.Parse is
Postponed_Not_Allowed;
Label_Not_Allowed;
Stmt := Parse_Psl_Declaration;
+ when Tok_Psl_Assume =>
+ Postponed_Not_Allowed;
+ Stmt := Parse_Psl_Assume_Directive;
when Tok_Psl_Cover =>
Postponed_Not_Allowed;
Stmt := Parse_Psl_Cover_Directive;
diff --git a/src/vhdl/vhdl-prints.adb b/src/vhdl/vhdl-prints.adb
index 16f9e0e37..7c87b3df5 100644
--- a/src/vhdl/vhdl-prints.adb
+++ b/src/vhdl/vhdl-prints.adb
@@ -3893,7 +3893,7 @@ package body Vhdl.Prints is
end if;
end Disp_PSL_NFA;
- procedure Disp_Psl_Assert_Statement
+ procedure Disp_Psl_Assert_Directive
(Ctxt : in out Ctxt_Class; Stmt : Iir) is
begin
Start_Hbox (Ctxt);
@@ -3909,7 +3909,25 @@ package body Vhdl.Prints is
Disp_Token (Ctxt, Tok_Semi_Colon);
Close_Hbox (Ctxt);
Disp_PSL_NFA (Get_PSL_NFA (Stmt));
- end Disp_Psl_Assert_Statement;
+ end Disp_Psl_Assert_Directive;
+
+ procedure Disp_Psl_Assume_Directive
+ (Ctxt : in out Ctxt_Class; Stmt : Iir) is
+ begin
+ Start_Hbox (Ctxt);
+ if Vhdl_Std < Vhdl_08 then
+ OOB.Put ("--psl ");
+ end if;
+ Disp_Label (Ctxt, Stmt);
+ Disp_Postponed (Ctxt, Stmt);
+ Disp_Token (Ctxt, Tok_Psl_Assume);
+ Disp_Psl_Expression (Ctxt, Get_Psl_Property (Stmt));
+ Disp_Report_Expression (Ctxt, Stmt);
+ Disp_Severity_Expression (Ctxt, Stmt);
+ Disp_Token (Ctxt, Tok_Semi_Colon);
+ Close_Hbox (Ctxt);
+ Disp_PSL_NFA (Get_PSL_NFA (Stmt));
+ end Disp_Psl_Assume_Directive;
procedure Disp_Psl_Cover_Directive
(Ctxt : in out Ctxt_Class; Stmt : Iir) is
@@ -3984,8 +4002,10 @@ package body Vhdl.Prints is
when Iir_Kind_Psl_Declaration
| Iir_Kind_Psl_Endpoint_Declaration =>
Disp_Psl_Declaration (Ctxt, Stmt);
- when Iir_Kind_Psl_Assert_Statement =>
- Disp_Psl_Assert_Statement (Ctxt, Stmt);
+ when Iir_Kind_Psl_Assert_Directive =>
+ Disp_Psl_Assert_Directive (Ctxt, Stmt);
+ when Iir_Kind_Psl_Assume_Directive =>
+ Disp_Psl_Assume_Directive (Ctxt, Stmt);
when Iir_Kind_Psl_Cover_Directive =>
Disp_Psl_Cover_Directive (Ctxt, Stmt);
when Iir_Kind_Psl_Restrict_Directive =>
diff --git a/src/vhdl/vhdl-scanner.adb b/src/vhdl/vhdl-scanner.adb
index 740617ba4..2f08ffbab 100644
--- a/src/vhdl/vhdl-scanner.adb
+++ b/src/vhdl/vhdl-scanner.adb
@@ -1307,6 +1307,8 @@ package body Vhdl.Scanner is
Current_Token := Tok_Psl_Property;
when Std_Names.Name_Endpoint =>
Current_Token := Tok_Psl_Endpoint;
+ when Std_Names.Name_Assume =>
+ Current_Token := Tok_Psl_Assume;
when Std_Names.Name_Cover =>
Current_Token := Tok_Psl_Cover;
when Std_Names.Name_Default =>
diff --git a/src/vhdl/vhdl-sem_psl.adb b/src/vhdl/vhdl-sem_psl.adb
index b4e949aac..671c59c27 100644
--- a/src/vhdl/vhdl-sem_psl.adb
+++ b/src/vhdl/vhdl-sem_psl.adb
@@ -695,12 +695,12 @@ package body Vhdl.Sem_Psl is
Set_PSL_Clock (Stmt, Clk);
end Sem_Psl_Directive_Clock;
- function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir
+ function Sem_Psl_Assert_Directive (Stmt : Iir) return Iir
is
Prop : PSL_Node;
Res : Iir;
begin
- pragma Assert (Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Statement);
+ pragma Assert (Get_Kind (Stmt) = Iir_Kind_Psl_Assert_Directive);
-- Sem report and severity expressions.
Sem_Report_Statement (Stmt);
@@ -730,7 +730,26 @@ package body Vhdl.Sem_Psl is
PSL.Subsets.Check_Simple (Prop);
return Stmt;
- end Sem_Psl_Assert_Statement;
+ end Sem_Psl_Assert_Directive;
+
+ procedure Sem_Psl_Assume_Directive (Stmt : Iir)
+ is
+ Prop : PSL_Node;
+ 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);
+
+ -- 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_Cover_Directive (Stmt : Iir)
is
diff --git a/src/vhdl/vhdl-sem_psl.ads b/src/vhdl/vhdl-sem_psl.ads
index 433555b20..1cd02796e 100644
--- a/src/vhdl/vhdl-sem_psl.ads
+++ b/src/vhdl/vhdl-sem_psl.ads
@@ -23,8 +23,9 @@ package Vhdl.Sem_Psl is
procedure Sem_Psl_Endpoint_Declaration (Stmt : Iir);
-- May return a non-psl concurrent assertion statement.
- function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir;
+ function Sem_Psl_Assert_Directive (Stmt : Iir) return Iir;
+ procedure Sem_Psl_Assume_Directive (Stmt : Iir);
procedure Sem_Psl_Cover_Directive (Stmt : Iir);
procedure Sem_Psl_Restrict_Directive (Stmt : Iir);
procedure Sem_Psl_Default_Clock (Stmt : Iir);
diff --git a/src/vhdl/vhdl-sem_stmts.adb b/src/vhdl/vhdl-sem_stmts.adb
index 4b8c5880c..545a543c7 100644
--- a/src/vhdl/vhdl-sem_stmts.adb
+++ b/src/vhdl/vhdl-sem_stmts.adb
@@ -2020,8 +2020,10 @@ package body Vhdl.Sem_Stmts is
Sem_Psl.Sem_Psl_Declaration (El);
when Iir_Kind_Psl_Endpoint_Declaration =>
Sem_Psl.Sem_Psl_Endpoint_Declaration (El);
- when Iir_Kind_Psl_Assert_Statement =>
- New_El := Sem_Psl.Sem_Psl_Assert_Statement (El);
+ when Iir_Kind_Psl_Assert_Directive =>
+ New_El := Sem_Psl.Sem_Psl_Assert_Directive (El);
+ when Iir_Kind_Psl_Assume_Directive =>
+ Sem_Psl.Sem_Psl_Assume_Directive (El);
when Iir_Kind_Psl_Cover_Directive =>
Sem_Psl.Sem_Psl_Cover_Directive (El);
when Iir_Kind_Psl_Restrict_Directive =>
diff --git a/src/vhdl/vhdl-tokens.adb b/src/vhdl/vhdl-tokens.adb
index 8ad0e4081..1f17c5092 100644
--- a/src/vhdl/vhdl-tokens.adb
+++ b/src/vhdl/vhdl-tokens.adb
@@ -422,6 +422,8 @@ package body Vhdl.Tokens is
return "sequence";
when Tok_Psl_Endpoint =>
return "endpoint";
+ when Tok_Psl_Assume =>
+ return "assume";
when Tok_Psl_Cover =>
return "cover";
when Tok_Psl_Restrict =>
diff --git a/src/vhdl/vhdl-tokens.ads b/src/vhdl/vhdl-tokens.ads
index e8daf0bce..f8e2dd14e 100644
--- a/src/vhdl/vhdl-tokens.ads
+++ b/src/vhdl/vhdl-tokens.ads
@@ -261,6 +261,7 @@ package Vhdl.Tokens is
Tok_Psl_Property,
Tok_Psl_Sequence,
Tok_Psl_Endpoint,
+ Tok_Psl_Assume,
Tok_Psl_Cover,
Tok_Psl_Restrict,
Tok_Psl_Restrict_Guarantee,
diff --git a/testsuite/gna/issue880/psl.ref b/testsuite/gna/issue880/psl.ref
new file mode 100644
index 000000000..5fd471f5d
--- /dev/null
+++ b/testsuite/gna/issue880/psl.ref
@@ -0,0 +1,30 @@
+{ "details" : [
+ { "directive": "assumption",
+ "name": ".psl(behav).a1",
+ "file": "psl.vhdl",
+ "line": 27,
+ "count": 0,
+ "status": "passed"},
+ { "directive": "assumption",
+ "name": ".psl(behav).a2",
+ "file": "psl.vhdl",
+ "line": 28,
+ "count": 0,
+ "status": "passed"},
+ { "directive": "cover",
+ "name": ".psl(behav).c1",
+ "file": "psl.vhdl",
+ "line": 29,
+ "count": 3,
+ "status": "covered"}],
+ "summary" : {
+ "assert": 0,
+ "assert-failure": 0,
+ "assert-pass": 0,
+ "assume": 2,
+ "assume-failure": 0,
+ "assume-pass": 2,
+ "cover": 1,
+ "cover-failure": 0,
+ "cover-pass": 1}
+}
diff --git a/testsuite/gna/issue880/psl.vhdl b/testsuite/gna/issue880/psl.vhdl
new file mode 100644
index 000000000..a1e203f5f
--- /dev/null
+++ b/testsuite/gna/issue880/psl.vhdl
@@ -0,0 +1,30 @@
+entity psl is
+end;
+
+architecture behav of psl is
+ signal a, b, c : bit;
+ signal clk : bit;
+ subtype wf_type is bit_vector (0 to 7);
+ constant wave_a : wf_type := "10010100";
+ constant wave_b : wf_type := "01001010";
+ constant wave_c : wf_type := "00100101";
+begin
+ process
+ begin
+ for i in wf_type'range loop
+ clk <= '0';
+ wait for 1 ns;
+ a <= wave_a (i);
+ b <= wave_b (i);
+ c <= wave_c (i);
+ clk <= '1';
+ wait for 1 ns;
+ end loop;
+ wait;
+ end process;
+
+ -- psl default clock is (clk'event and clk = '1');
+ -- psl a1: assume always a |=> b;
+ -- psl a2: assume always a -> eventually! c;
+ -- psl c1: cover {a;b;c};
+end behav;
diff --git a/testsuite/gna/issue880/testsuite.sh b/testsuite/gna/issue880/testsuite.sh
new file mode 100755
index 000000000..136317e17
--- /dev/null
+++ b/testsuite/gna/issue880/testsuite.sh
@@ -0,0 +1,41 @@
+#! /bin/sh
+
+. ../../testenv.sh
+
+GHDL_STD_FLAGS="-fpsl"
+analyze psl.vhdl
+elab psl
+if ghdl_has_feature psl psl; then
+ simulate psl --psl-report=psl.out
+
+ if ! diff --strip-trailing-cr psl.out psl.ref > /dev/null; then
+ echo "report mismatch"
+ exit 1
+ fi
+
+ rm -f psl.out
+fi
+clean
+
+# Using vhdl 08
+GHDL_STD_FLAGS="-fpsl --std=08"
+analyze psl.vhdl
+elab -fpsl psl
+if ghdl_has_feature psl psl; then
+ simulate psl --psl-report=psl.out
+
+ diff --strip-trailing-cr -q psl.out psl.ref
+
+ rm -f psl.out
+fi
+clean
+
+# Usage example (python 2.7):
+#
+# import json
+# d=json.load(open("psl.out"))
+# print d['summary']
+# {u'assert-pass': 2, u'cover': 1, ... }
+# print d['summary']['assert']
+
+echo "Test successful"
diff --git a/testsuite/gna/ticket24/psl.ref b/testsuite/gna/ticket24/psl.ref
index 6a5588a3a..9cd8cdb35 100644
--- a/testsuite/gna/ticket24/psl.ref
+++ b/testsuite/gna/ticket24/psl.ref
@@ -21,6 +21,9 @@
"assert": 2,
"assert-failure": 0,
"assert-pass": 2,
+ "assume": 0,
+ "assume-failure": 0,
+ "assume-pass": 0,
"cover": 1,
"cover-failure": 0,
"cover-pass": 1}