From ace70f3cc4d5ac8d5fb7e02e96d5b3187319e520 Mon Sep 17 00:00:00 2001
From: Tristan Gingold <tgingold@free.fr>
Date: Sat, 13 Feb 2016 18:00:36 +0100
Subject: psl: cover directive works on a sequence, not on a property.
---
src/psl/psl-build.adb | 2 --
src/psl/psl-build.ads | 1 +
src/psl/psl-prints.adb | 14 +++++---
src/psl/psl-prints.ads | 6 ++--
src/vhdl/canon.adb | 58 +++++++++++++++++++++++---------
src/vhdl/disp_vhdl.adb | 41 ++++++++++++++++++++++-
src/vhdl/disp_vhdl.ads | 2 ++
src/vhdl/iirs.adb | 16 +++++++++
src/vhdl/iirs.ads | 8 +++++
src/vhdl/nodes_meta.adb | 24 +++++++++-----
src/vhdl/nodes_meta.ads | 2 ++
src/vhdl/parse.adb | 62 ++++++++++++++++++++++------------
src/vhdl/parse_psl.adb | 21 ++++++------
src/vhdl/parse_psl.ads | 1 +
src/vhdl/sem_psl.adb | 68 ++++++++++++++++++++++++++++----------
src/vhdl/sem_psl.ads | 4 +++
src/vhdl/sem_stmts.adb | 5 +--
src/vhdl/simulate/debugger.adb | 47 ++++++++++++++++++++++++--
src/vhdl/simulate/simulation.adb | 3 ++
src/vhdl/translate/trans-chap9.adb | 8 ++++-
20 files changed, 307 insertions(+), 86 deletions(-)
diff --git a/src/psl/psl-build.adb b/src/psl/psl-build.adb
index 661d758bf..7a047b6de 100644
--- a/src/psl/psl-build.adb
+++ b/src/psl/psl-build.adb
@@ -29,8 +29,6 @@ with PSL.Prints;
with PSL.NFAs; use PSL.NFAs;
package body PSL.Build is
- function Build_SERE_FA (N : Node) return NFA;
-
package Intersection is
function Build_Inter (L, R : NFA; Match_Len : Boolean) return NFA;
end Intersection;
diff --git a/src/psl/psl-build.ads b/src/psl/psl-build.ads
index c8e15ee22..dcfadb96a 100644
--- a/src/psl/psl-build.ads
+++ b/src/psl/psl-build.ads
@@ -21,5 +21,6 @@ with PSL.Nodes; use PSL.Nodes;
package PSL.Build is
Optimize_Final : Boolean := True;
+ function Build_SERE_FA (N : Node) return NFA;
function Build_FA (N : Node) return NFA;
end PSL.Build;
diff --git a/src/psl/psl-prints.adb b/src/psl/psl-prints.adb
index 19d7c3959..dd0755570 100644
--- a/src/psl/psl-prints.adb
+++ b/src/psl/psl-prints.adb
@@ -67,7 +67,9 @@ package body PSL.Prints is
| N_True
| N_False
| N_EOS
- | N_HDL_Expr =>
+ | N_HDL_Expr
+ | N_Property_Instance
+ | N_Sequence_Instance =>
return Prio_HDL;
when N_Or_Bool =>
return Prio_Seq_Or;
@@ -184,8 +186,6 @@ package body PSL.Prints is
end if;
end Print_Expr;
- procedure Print_Sequence (Seq : Node; Parent_Prio : Priority);
-
procedure Print_Count (N : Node) is
B : Node;
begin
@@ -222,7 +222,7 @@ package body PSL.Prints is
Put ("]");
end Print_Repeat_Sequence;
- procedure Print_Sequence (Seq : Node; Parent_Prio : Priority)
+ procedure Print_Sequence (Seq : Node; Parent_Prio : Priority := Prio_Lowest)
is
Prio : constant Priority := Get_Priority (Seq);
Add_Paren : constant Boolean := Prio < Parent_Prio
@@ -260,6 +260,8 @@ package body PSL.Prints is
when N_Booleans
| N_Name_Decl =>
Print_Expr (Seq);
+ when N_Sequence_Instance =>
+ Put (Image (Get_Identifier (Get_Declaration (Seq))));
when others =>
Error_Kind ("print_sequence", Seq);
end case;
@@ -387,6 +389,10 @@ package body PSL.Prints is
Print_Expr (Prop);
when N_Sequences =>
Print_Sequence (Prop, Parent_Prio);
+ when N_Property_Instance =>
+ Put (Image (Get_Identifier (Get_Declaration (Prop))));
+ when N_EOS =>
+ Put ("EOS");
when others =>
Error_Kind ("print_property", Prop);
end case;
diff --git a/src/psl/psl-prints.ads b/src/psl/psl-prints.ads
index 920ca5939..d49a5e093 100644
--- a/src/psl/psl-prints.ads
+++ b/src/psl/psl-prints.ads
@@ -21,8 +21,10 @@ with PSL.Priorities; use PSL.Priorities;
package PSL.Prints is
procedure Print_Unit (Unit : Node);
- procedure Print_Property (Prop : Node;
- Parent_Prio : Priority := Prio_Lowest);
+ procedure Print_Sequence
+ (Seq : Node; Parent_Prio : Priority := Prio_Lowest);
+ procedure Print_Property
+ (Prop : Node; Parent_Prio : Priority := Prio_Lowest);
procedure Print_Expr (N : Node; Parent_Prio : Priority := Prio_Lowest);
-- Procedure to display HDL_Expr nodes.
diff --git a/src/vhdl/canon.adb b/src/vhdl/canon.adb
index c498ba55c..bf4536088 100644
--- a/src/vhdl/canon.adb
+++ b/src/vhdl/canon.adb
@@ -1636,6 +1636,31 @@ package body Canon is
return False;
end Psl_Need_Finalizer;
+ procedure Canon_Psl_Directive (Stmt : Iir)
+ is
+ use PSL.Nodes;
+ Fa : PSL_NFA;
+ Num : Natural;
+ List : Iir_List;
+ begin
+ Fa := Get_PSL_NFA (Stmt);
+
+ PSL.NFAs.Labelize_States (Fa, Num);
+ Set_PSL_Nbr_States (Stmt, Int32 (Num));
+
+ Set_PSL_EOS_Flag (Stmt, Psl_Need_Finalizer (Fa));
+
+ List := Create_Iir_List;
+ Canon_PSL.Canon_Extract_Sensitivity (Get_PSL_Clock (Stmt), List);
+ Set_PSL_Clock_Sensitivity (Stmt, List);
+
+ if Canon_Flag_Expressions then
+ Canon_PSL_Expression (Get_PSL_Clock (Stmt));
+ Canon_Expression (Get_Severity_Expression (Stmt));
+ Canon_Expression (Get_Report_Expression (Stmt));
+ end if;
+ end Canon_Psl_Directive;
+
procedure Canon_Concurrent_Stmts (Top : Iir_Design_Unit; Parent : Iir)
is
-- Current element in the chain of concurrent statements.
@@ -1897,37 +1922,38 @@ package body Canon is
Canon_Generate_Statement_Body
(Top, Get_Generate_Statement_Body (El));
- when Iir_Kind_Psl_Assert_Statement
- | Iir_Kind_Psl_Cover_Statement =>
+ when Iir_Kind_Psl_Assert_Statement =>
declare
use PSL.Nodes;
Prop : PSL_Node;
Fa : PSL_NFA;
- Num : Natural;
- List : Iir_List;
begin
Prop := Get_Psl_Property (El);
Prop := PSL.Rewrites.Rewrite_Property (Prop);
Set_Psl_Property (El, Prop);
+
-- Generate the NFA.
Fa := PSL.Build.Build_FA (Prop);
Set_PSL_NFA (El, Fa);
- PSL.NFAs.Labelize_States (Fa, Num);
- Set_PSL_Nbr_States (El, Int32 (Num));
+ Canon_Psl_Directive (El);
+ end;
- Set_PSL_EOS_Flag (El, Psl_Need_Finalizer (Fa));
+ when Iir_Kind_Psl_Cover_Statement =>
+ declare
+ use PSL.Nodes;
+ Seq : PSL_Node;
+ Fa : PSL_NFA;
+ begin
+ Seq := Get_Psl_Sequence (El);
+ Seq := PSL.Rewrites.Rewrite_SERE (Seq);
+ Set_Psl_Sequence (El, Seq);
- List := Create_Iir_List;
- Canon_PSL.Canon_Extract_Sensitivity
- (Get_PSL_Clock (El), List);
- Set_PSL_Clock_Sensitivity (El, List);
+ -- Generate the NFA.
+ Fa := PSL.Build.Build_SERE_FA (Seq);
+ Set_PSL_NFA (El, Fa);
- if Canon_Flag_Expressions then
- Canon_PSL_Expression (Get_PSL_Clock (El));
- Canon_Expression (Get_Severity_Expression (El));
- Canon_Expression (Get_Report_Expression (El));
- end if;
+ Canon_Psl_Directive (El);
end;
when Iir_Kind_Psl_Default_Clock =>
diff --git a/src/vhdl/disp_vhdl.adb b/src/vhdl/disp_vhdl.adb
index 9872ff802..4cccdf576 100644
--- a/src/vhdl/disp_vhdl.adb
+++ b/src/vhdl/disp_vhdl.adb
@@ -2835,6 +2835,12 @@ package body Disp_Vhdl is
PSL.Prints.Print_Property (Expr);
end Disp_Psl_Expression;
+ procedure Disp_Psl_Sequence (Expr : PSL_Node) is
+ begin
+ PSL.Prints.HDL_Expr_Printer := Disp_PSL_HDL_Expr'Access;
+ PSL.Prints.Print_Sequence (Expr);
+ end Disp_Psl_Sequence;
+
procedure Disp_Block_Header (Header : Iir_Block_Header; Indent: Count)
is
Chain : Iir;
@@ -2979,6 +2985,29 @@ package body Disp_Vhdl is
Put_Line (";");
end Disp_Psl_Default_Clock;
+ procedure Disp_Psl_Declaration (Stmt : Iir)
+ is
+ use PSL.Nodes;
+ Decl : constant PSL_Node := Get_Psl_Declaration (Stmt);
+ begin
+ Put ("--psl ");
+ case Get_Kind (Decl) is
+ when N_Property_Declaration =>
+ Put ("property ");
+ Disp_Ident (Get_Identifier (Decl));
+ Put (" is ");
+ Disp_Psl_Expression (Get_Property (Decl));
+ when N_Sequence_Declaration =>
+ Put ("sequence ");
+ Disp_Ident (Get_Identifier (Decl));
+ Put (" is ");
+ Disp_Psl_Sequence (Get_Sequence (Decl));
+ when others =>
+ Error_Kind ("disp_psl_declaration", Decl);
+ end case;
+ Put_Line (";");
+ end Disp_Psl_Declaration;
+
procedure Disp_PSL_NFA (N : PSL.Nodes.NFA)
is
use PSL.NFAs;
@@ -2994,6 +3023,12 @@ package body Disp_Vhdl is
E : NFA_Edge;
begin
if N /= No_NFA then
+ Put ("-- start: ");
+ Disp_State (Get_Start_State (N));
+ Put (", final: ");
+ Disp_State (Get_Final_State (N));
+ New_Line;
+
S := Get_First_State (N);
while S /= No_State loop
E := Get_First_Src_Edge (S);
@@ -3027,7 +3062,7 @@ package body Disp_Vhdl is
Put ("--psl ");
Disp_Label (Stmt);
Put ("cover ");
- Disp_Psl_Expression (Get_Psl_Property (Stmt));
+ Disp_Psl_Sequence (Get_Psl_Sequence (Stmt));
Put_Line (";");
Disp_PSL_NFA (Get_PSL_NFA (Stmt));
end Disp_Psl_Cover_Statement;
@@ -3070,6 +3105,8 @@ package body Disp_Vhdl is
Disp_For_Generate_Statement (Stmt);
when Iir_Kind_Psl_Default_Clock =>
Disp_Psl_Default_Clock (Stmt);
+ when Iir_Kind_Psl_Declaration =>
+ Disp_Psl_Declaration (Stmt);
when Iir_Kind_Psl_Assert_Statement =>
Disp_Psl_Assert_Statement (Stmt);
when Iir_Kind_Psl_Cover_Statement =>
@@ -3340,6 +3377,8 @@ package body Disp_Vhdl is
| Iir_Kind_Indexed_Name
| Iir_Kind_Slice_Name =>
Disp_Expression (An_Iir);
+ when Iir_Kind_Psl_Cover_Statement =>
+ Disp_Psl_Cover_Statement (An_Iir);
when others =>
Error_Kind ("disp", An_Iir);
end case;
diff --git a/src/vhdl/disp_vhdl.ads b/src/vhdl/disp_vhdl.ads
index 880290efd..9f04129bc 100644
--- a/src/vhdl/disp_vhdl.ads
+++ b/src/vhdl/disp_vhdl.ads
@@ -24,6 +24,8 @@ package Disp_Vhdl is
-- the node.
procedure Disp_Vhdl (An_Iir: Iir);
+ procedure Disp_PSL_NFA (N : PSL_NFA);
+
procedure Disp_Expression (Expr: Iir);
-- Display an expression.
diff --git a/src/vhdl/iirs.adb b/src/vhdl/iirs.adb
index 00614233c..3b9f32b86 100644
--- a/src/vhdl/iirs.adb
+++ b/src/vhdl/iirs.adb
@@ -5229,6 +5229,22 @@ package body Iirs is
Set_Field1 (Decl, PSL_Node_To_Iir (Prop));
end Set_Psl_Property;
+ function Get_Psl_Sequence (Decl : Iir) return PSL_Node is
+ begin
+ pragma Assert (Decl /= Null_Iir);
+ pragma Assert (Has_Psl_Sequence (Get_Kind (Decl)),
+ "no field Psl_Sequence");
+ return Iir_To_PSL_Node (Get_Field1 (Decl));
+ end Get_Psl_Sequence;
+
+ procedure Set_Psl_Sequence (Decl : Iir; Prop : PSL_Node) is
+ begin
+ pragma Assert (Decl /= Null_Iir);
+ pragma Assert (Has_Psl_Sequence (Get_Kind (Decl)),
+ "no field Psl_Sequence");
+ Set_Field1 (Decl, PSL_Node_To_Iir (Prop));
+ end Set_Psl_Sequence;
+
function Get_Psl_Declaration (Decl : Iir) return PSL_Node is
begin
pragma Assert (Decl /= Null_Iir);
diff --git a/src/vhdl/iirs.ads b/src/vhdl/iirs.ads
index 1272e7723..a1fe93ced 100644
--- a/src/vhdl/iirs.ads
+++ b/src/vhdl/iirs.ads
@@ -2506,8 +2506,12 @@ package Iirs is
--
-- Get/Set_Parent (Field0)
--
+ -- Only for Iir_Kind_Psl_Assert_Statement:
-- Get/Set_Psl_Property (Field1)
--
+ -- Only for Iir_Kind_Psl_Cover_Statement:
+ -- Get/Set_Psl_Sequence (Field1)
+ --
-- Get/Set_Chain (Field2)
--
-- Get/Set_Label (Field3)
@@ -6645,6 +6649,10 @@ package Iirs is
function Get_Psl_Property (Decl : Iir) return PSL_Node;
procedure Set_Psl_Property (Decl : Iir; Prop : PSL_Node);
+ -- Field: Field1 (uc)
+ function Get_Psl_Sequence (Decl : Iir) return PSL_Node;
+ procedure Set_Psl_Sequence (Decl : Iir; Prop : PSL_Node);
+
-- Field: Field1 (uc)
function Get_Psl_Declaration (Decl : Iir) return PSL_Node;
procedure Set_Psl_Declaration (Decl : Iir; Prop : PSL_Node);
diff --git a/src/vhdl/nodes_meta.adb b/src/vhdl/nodes_meta.adb
index d5a3c62a0..b868751f5 100644
--- a/src/vhdl/nodes_meta.adb
+++ b/src/vhdl/nodes_meta.adb
@@ -312,6 +312,7 @@ package body Nodes_Meta is
Field_Suspend_Flag => Type_Boolean,
Field_Is_Ref => Type_Boolean,
Field_Psl_Property => Type_PSL_Node,
+ Field_Psl_Sequence => Type_PSL_Node,
Field_Psl_Declaration => Type_PSL_Node,
Field_Psl_Expression => Type_PSL_Node,
Field_Psl_Boolean => Type_PSL_Node,
@@ -916,6 +917,8 @@ package body Nodes_Meta is
return "is_ref";
when Field_Psl_Property =>
return "psl_property";
+ when Field_Psl_Sequence =>
+ return "psl_sequence";
when Field_Psl_Declaration =>
return "psl_declaration";
when Field_Psl_Expression =>
@@ -2038,6 +2041,8 @@ package body Nodes_Meta is
return Attr_None;
when Field_Psl_Property =>
return Attr_None;
+ when Field_Psl_Sequence =>
+ return Attr_None;
when Field_Psl_Declaration =>
return Attr_None;
when Field_Psl_Expression =>
@@ -3473,7 +3478,7 @@ package body Nodes_Meta is
Field_Report_Expression,
Field_Parent,
-- Iir_Kind_Psl_Cover_Statement
- Field_Psl_Property,
+ Field_Psl_Sequence,
Field_Label,
Field_PSL_Clock,
Field_PSL_NFA,
@@ -5960,6 +5965,8 @@ package body Nodes_Meta is
case F is
when Field_Psl_Property =>
return Get_Psl_Property (N);
+ when Field_Psl_Sequence =>
+ return Get_Psl_Sequence (N);
when Field_Psl_Declaration =>
return Get_Psl_Declaration (N);
when Field_Psl_Expression =>
@@ -5980,6 +5987,8 @@ package body Nodes_Meta is
case F is
when Field_Psl_Property =>
Set_Psl_Property (N, V);
+ when Field_Psl_Sequence =>
+ Set_Psl_Sequence (N, V);
when Field_Psl_Declaration =>
Set_Psl_Declaration (N, V);
when Field_Psl_Expression =>
@@ -9762,15 +9771,14 @@ package body Nodes_Meta is
function Has_Psl_Property (K : Iir_Kind) return Boolean is
begin
- case K is
- when Iir_Kind_Psl_Assert_Statement
- | Iir_Kind_Psl_Cover_Statement =>
- return True;
- when others =>
- return False;
- end case;
+ return K = Iir_Kind_Psl_Assert_Statement;
end Has_Psl_Property;
+ function Has_Psl_Sequence (K : Iir_Kind) return Boolean is
+ begin
+ return K = Iir_Kind_Psl_Cover_Statement;
+ end Has_Psl_Sequence;
+
function Has_Psl_Declaration (K : Iir_Kind) return Boolean is
begin
return K = Iir_Kind_Psl_Declaration;
diff --git a/src/vhdl/nodes_meta.ads b/src/vhdl/nodes_meta.ads
index d4ae3a060..19b5930a6 100644
--- a/src/vhdl/nodes_meta.ads
+++ b/src/vhdl/nodes_meta.ads
@@ -352,6 +352,7 @@ package Nodes_Meta is
Field_Suspend_Flag,
Field_Is_Ref,
Field_Psl_Property,
+ Field_Psl_Sequence,
Field_Psl_Declaration,
Field_Psl_Expression,
Field_Psl_Boolean,
@@ -842,6 +843,7 @@ package Nodes_Meta is
function Has_Suspend_Flag (K : Iir_Kind) return Boolean;
function Has_Is_Ref (K : Iir_Kind) return Boolean;
function Has_Psl_Property (K : Iir_Kind) return Boolean;
+ function Has_Psl_Sequence (K : Iir_Kind) return Boolean;
function Has_Psl_Declaration (K : Iir_Kind) return Boolean;
function Has_Psl_Expression (K : Iir_Kind) return Boolean;
function Has_Psl_Boolean (K : Iir_Kind) return Boolean;
diff --git a/src/vhdl/parse.adb b/src/vhdl/parse.adb
index ccbf98617..012a54264 100644
--- a/src/vhdl/parse.adb
+++ b/src/vhdl/parse.adb
@@ -6917,18 +6917,31 @@ package body Parse is
return Res;
end Parse_Psl_Declaration;
+ -- Parse end of PSL assert/cover statement.
+ procedure Parse_Psl_Assert_Report_Severity (Stmt : Iir) is
+ begin
+ if Current_Token = Tok_Report then
+ -- Skip 'report'
+ Scan;
+
+ Set_Report_Expression (Stmt, Parse_Expression);
+ end if;
+
+ if Current_Token = Tok_Severity then
+ -- Skip 'severity'
+ Scan;
+
+ Set_Severity_Expression (Stmt, Parse_Expression);
+ end if;
+
+ Expect (Tok_Semi_Colon);
+ end Parse_Psl_Assert_Report_Severity;
+
function Parse_Psl_Assert_Statement return Iir
is
Res : Iir;
begin
- case Current_Token is
- when Tok_Assert =>
- Res := Create_Iir (Iir_Kind_Psl_Assert_Statement);
- when Tok_Psl_Cover =>
- Res := Create_Iir (Iir_Kind_Psl_Cover_Statement);
- when others =>
- raise Internal_Error;
- end case;
+ Res := Create_Iir (Iir_Kind_Psl_Assert_Statement);
-- Skip 'assert'
Scan;
@@ -6938,24 +6951,31 @@ package body Parse is
-- No more PSL tokens after the property.
Scanner.Flag_Psl := False;
- if Current_Token = Tok_Report then
- -- Skip 'report'
- Scan;
+ Parse_Psl_Assert_Report_Severity (Res);
- Set_Report_Expression (Res, Parse_Expression);
- end if;
+ Scanner.Flag_Scan_In_Comment := False;
+ return Res;
+ end Parse_Psl_Assert_Statement;
- if Current_Token = Tok_Severity then
- -- Skip 'severity'
- Scan;
+ function Parse_Psl_Cover_Statement return Iir
+ is
+ Res : Iir;
+ begin
+ Res := Create_Iir (Iir_Kind_Psl_Cover_Statement);
- Set_Severity_Expression (Res, Parse_Expression);
- end if;
+ -- Skip 'cover'
+ Scan;
+
+ Set_Psl_Sequence (Res, Parse_Psl.Parse_Psl_Sequence);
+
+ -- No more PSL tokens after the property.
+ Scanner.Flag_Psl := False;
+
+ Parse_Psl_Assert_Report_Severity (Res);
- Expect (Tok_Semi_Colon);
Scanner.Flag_Scan_In_Comment := False;
return Res;
- end Parse_Psl_Assert_Statement;
+ end Parse_Psl_Cover_Statement;
procedure Parse_Concurrent_Statements (Parent : Iir)
is
@@ -7103,7 +7123,7 @@ package body Parse is
Stmt := Parse_Psl_Declaration;
when Tok_Psl_Cover =>
Postponed_Not_Allowed;
- Stmt := Parse_Psl_Assert_Statement;
+ Stmt := Parse_Psl_Cover_Statement;
when others =>
-- FIXME: improve message:
-- instead of 'unexpected token 'signal' in conc stmt list'
diff --git a/src/vhdl/parse_psl.adb b/src/vhdl/parse_psl.adb
index 506218ade..a356043aa 100644
--- a/src/vhdl/parse_psl.adb
+++ b/src/vhdl/parse_psl.adb
@@ -77,17 +77,18 @@ package body Parse_Psl is
function Vhdl_To_Psl (N : Iirs.Iir) return Node
is
+ use Iirs;
Res : Node;
begin
Res := Create_Node_Loc (N_HDL_Expr);
- Set_Location (Res, Iirs.Get_Location (N));
- Set_HDL_Node (Res, Int32 (N));
+ if N /= Null_Iir then
+ Set_Location (Res, Get_Location (N));
+ Set_HDL_Node (Res, Int32 (N));
+ end if;
return Res;
end Vhdl_To_Psl;
function Parse_FL_Property (Prio : Priority) return Node;
- function Parse_Sequence return Node;
-
function Parse_Parenthesis_Boolean return Node;
function Parse_Boolean (Parent_Prio : Priority) return Node;
@@ -161,7 +162,7 @@ package body Parse_Psl is
Kind : Nkind;
Op_Prio : Priority;
begin
- Left := Parse_Sequence; -- FIXME: allow boolean;
+ Left := Parse_Psl_Sequence; -- FIXME: allow boolean;
loop
case Current_Token is
when Tok_Semi_Colon =>
@@ -282,7 +283,7 @@ package body Parse_Psl is
end if;
end Parse_Bracket_Number;
- function Parse_Sequence return Node is
+ function Parse_Psl_Sequence return Node is
Res, N : Node;
begin
case Current_Token is
@@ -331,7 +332,7 @@ package body Parse_Psl is
return Res;
end case;
end loop;
- end Parse_Sequence;
+ end Parse_Psl_Sequence;
-- precond: '('
-- postcond: next token
@@ -430,7 +431,7 @@ package body Parse_Psl is
when Tok_Left_Paren =>
return Parse_Parenthesis_FL_Property;
when Tok_Left_Curly =>
- Res := Parse_Sequence;
+ Res := Parse_Psl_Sequence;
if Get_Kind (Res) = N_Braced_SERE
and then Current_Token = Tok_Left_Paren
then
@@ -442,7 +443,7 @@ package body Parse_Psl is
Res := Tmp;
end if;
when others =>
- Res := Parse_Sequence;
+ Res := Parse_Psl_Sequence;
end case;
return Res;
end Parse_FL_Property_1;
@@ -663,7 +664,7 @@ package body Parse_Psl is
Set_Property (Res, Parse_Psl_Property);
when N_Sequence_Declaration
| N_Endpoint_Declaration =>
- Set_Sequence (Res, Parse_Sequence);
+ Set_Sequence (Res, Parse_Psl_Sequence);
when others =>
raise Internal_Error;
end case;
diff --git a/src/vhdl/parse_psl.ads b/src/vhdl/parse_psl.ads
index 62869feb8..160df668e 100644
--- a/src/vhdl/parse_psl.ads
+++ b/src/vhdl/parse_psl.ads
@@ -20,6 +20,7 @@ with Types; use Types;
with Tokens; use Tokens;
package Parse_Psl is
+ function Parse_Psl_Sequence return PSL_Node;
function Parse_Psl_Property return PSL_Node;
function Parse_Psl_Boolean return PSL_Node;
function Parse_Psl_Declaration (Tok : Token_Type) return PSL_Node;
diff --git a/src/vhdl/sem_psl.adb b/src/vhdl/sem_psl.adb
index 503842ce1..98e258359 100644
--- a/src/vhdl/sem_psl.adb
+++ b/src/vhdl/sem_psl.adb
@@ -150,11 +150,7 @@ package body Sem_Psl is
Expr := Finish_Sem_Name (Expr);
Set_HDL_Node (N, Expr);
- if Get_Kind (Expr) in Iir_Kinds_Denoting_Name then
- Name := Get_Named_Entity (Expr);
- else
- Name := Expr;
- end if;
+ Name := Strip_Denoting_Name (Expr);
case Get_Kind (Name) is
when Iir_Kind_Error =>
@@ -290,7 +286,20 @@ package body Sem_Psl is
| N_Not_Bool =>
return Sem_Boolean (Seq);
when N_HDL_Expr =>
- return Sem_Hdl_Expr (Seq);
+ 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
+ ("property instance not allowed in PSL sequence", Res);
+ when others =>
+ Error_Kind ("psl.sem_sequence.hdl", Res);
+ end case;
+ return Res;
when others =>
Error_Kind ("psl.sem_sequence", Seq);
end case;
@@ -553,14 +562,30 @@ package body Sem_Psl is
end case;
end Is_Boolean_Assertion;
+ procedure Sem_Psl_Directive_Clock (Stmt : Iir; Prop : in out Node)
+ is
+ Clk : Node;
+ begin
+ Extract_Clock (Prop, Clk);
+ if Clk = Null_Node then
+ if Current_Psl_Default_Clock = Null_Iir then
+ Error_Msg_Sem ("no clock for PSL directive", Stmt);
+ Clk := Null_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_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);
@@ -576,16 +601,7 @@ package body Sem_Psl is
end if;
-- Properties must be clocked.
- Extract_Clock (Prop, Clk);
- if Clk = Null_Node then
- if Current_Psl_Default_Clock = Null_Iir then
- Error_Msg_Sem ("no clock for PSL assert", Stmt);
- Clk := Null_Node;
- else
- Clk := Get_Psl_Boolean (Current_Psl_Default_Clock);
- end if;
- end if;
- Set_PSL_Clock (Stmt, Clk);
+ Sem_Psl_Directive_Clock (Stmt, Prop);
Set_Psl_Property (Stmt, Prop);
-- Check simple subset restrictions.
@@ -594,6 +610,24 @@ package body Sem_Psl is
return Stmt;
end Sem_Psl_Assert_Statement;
+ procedure Sem_Psl_Cover_Statement (Stmt : Iir)
+ is
+ Seq : Node;
+ begin
+ -- Sem report and severity expressions.
+ Sem_Report_Statement (Stmt);
+
+ Seq := Get_Psl_Sequence (Stmt);
+ Seq := Sem_Sequence (Seq);
+
+ -- 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_Cover_Statement;
+
procedure Sem_Psl_Default_Clock (Stmt : Iir)
is
Expr : Node;
diff --git a/src/vhdl/sem_psl.ads b/src/vhdl/sem_psl.ads
index 25663a244..482380303 100644
--- a/src/vhdl/sem_psl.ads
+++ b/src/vhdl/sem_psl.ads
@@ -20,7 +20,11 @@ with Iirs; use Iirs;
package Sem_Psl is
procedure Sem_Psl_Declaration (Stmt : Iir);
+
+ -- May return a non-psl concurrent assertion statement.
function Sem_Psl_Assert_Statement (Stmt : Iir) return Iir;
+
+ procedure Sem_Psl_Cover_Statement (Stmt : Iir);
procedure Sem_Psl_Default_Clock (Stmt : Iir);
function Sem_Psl_Name (Name : Iir) return Iir;
end Sem_Psl;
diff --git a/src/vhdl/sem_stmts.adb b/src/vhdl/sem_stmts.adb
index 5e04cb494..24d0f96e2 100644
--- a/src/vhdl/sem_stmts.adb
+++ b/src/vhdl/sem_stmts.adb
@@ -1913,9 +1913,10 @@ package body Sem_Stmts is
(El, Is_Passive);
when Iir_Kind_Psl_Declaration =>
Sem_Psl.Sem_Psl_Declaration (El);
- when Iir_Kind_Psl_Assert_Statement
- | Iir_Kind_Psl_Cover_Statement =>
+ when Iir_Kind_Psl_Assert_Statement =>
New_El := Sem_Psl.Sem_Psl_Assert_Statement (El);
+ when Iir_Kind_Psl_Cover_Statement =>
+ Sem_Psl.Sem_Psl_Cover_Statement (El);
when Iir_Kind_Psl_Default_Clock =>
Sem_Psl.Sem_Psl_Default_Clock (El);
when Iir_Kind_Simple_Simultaneous_Statement =>
diff --git a/src/vhdl/simulate/debugger.adb b/src/vhdl/simulate/debugger.adb
index bbb16e231..47846394a 100644
--- a/src/vhdl/simulate/debugger.adb
+++ b/src/vhdl/simulate/debugger.adb
@@ -1298,6 +1298,42 @@ package body Debugger is
return Walk_Continue;
end Cb_Disp_File;
+ procedure Info_PSL_Proc (Line : String)
+ is
+ pragma Unreferenced (Line);
+ begin
+ if PSL_Table.Last < PSL_Table.First then
+ Put_Line ("no PSL directive");
+ return;
+ end if;
+
+ for I in PSL_Table.First .. PSL_Table.Last loop
+ declare
+ E : PSL_Entry renames PSL_Table.Table (I);
+ begin
+ Disp_Instance_Name (E.Instance);
+ Put ('.');
+ Put (Name_Table.Image (Get_Identifier (E.Stmt)));
+ New_Line;
+ Disp_Vhdl.Disp_PSL_NFA (Get_PSL_NFA (E.Stmt));
+ Put (" 01234567890123456789012345678901234567890123456789");
+ for I in E.States'Range loop
+ if I mod 50 = 0 then
+ New_Line;
+ Put (Int32'Image (I / 10));
+ Put (": ");
+ end if;
+ if E.States (I) then
+ Put ('*');
+ else
+ Put ('.');
+ end if;
+ end loop;
+ New_Line;
+ end;
+ end loop;
+ end Info_PSL_Proc;
+
procedure Info_Stats_Proc (Line : String) is
P : Natural := Line'First;
E : Natural;
@@ -1324,7 +1360,8 @@ package body Debugger is
end if;
end Info_Stats_Proc;
- procedure Info_Files_Proc (Line : String) is
+ procedure Info_Files_Proc (Line : String)
+ is
pragma Unreferenced (Line);
Status : Walk_Status;
begin
@@ -1706,10 +1743,16 @@ package body Debugger is
end loop;
end Cont_Proc;
+ Menu_Info_Psl : aliased Menu_Entry :=
+ (Kind => Menu_Command,
+ Name => new String'("psl"),
+ Next => null,
+ Proc => Info_PSL_Proc'Access);
+
Menu_Info_Stats : aliased Menu_Entry :=
(Kind => Menu_Command,
Name => new String'("stats"),
- Next => null,
+ Next => Menu_Info_Psl'Access,
Proc => Info_Stats_Proc'Access);
Menu_Info_Tree : aliased Menu_Entry :=
diff --git a/src/vhdl/simulate/simulation.adb b/src/vhdl/simulate/simulation.adb
index b02d47dd2..c33997b7d 100644
--- a/src/vhdl/simulate/simulation.adb
+++ b/src/vhdl/simulate/simulation.adb
@@ -1112,6 +1112,9 @@ package body Simulation is
Release (Marker, Expr_Pool);
if V then
Nvec := (others => False);
+ if Get_Kind (E.Stmt) = Iir_Kind_Psl_Cover_Statement then
+ Nvec (0) := True;
+ end if;
-- For each state: if set, evaluate all outgoing edges.
NFA := Get_PSL_NFA (E.Stmt);
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index b2138cd06..36a8ec471 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -450,6 +450,12 @@ package body Trans.Chap9 is
Start_Declare_Stmt;
New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
Init_Var (Var_I);
+ if Get_Kind (Stmt) = Iir_Kind_Psl_Cover_Statement then
+ New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var),
+ New_Obj_Value (Var_I)),
+ New_Lit (Std_Boolean_True_Node));
+ Inc_Var (Var_I);
+ end if;
Start_Loop_Stmt (Label);
Gen_Exit_When
(Label,
@@ -1372,7 +1378,7 @@ package body Trans.Chap9 is
Start_Declare_Stmt;
New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
New_Assign_Stmt (New_Indexed_Element (Get_Var (Info.Psl_Vect_Var),
- New_Lit (Ghdl_Index_0)),
+ New_Lit (Ghdl_Index_0)),
New_Lit (Std_Boolean_True_Node));
New_Assign_Stmt (New_Obj (Var_I), New_Lit (Ghdl_Index_1));
Start_Loop_Stmt (Label);
--
cgit v1.2.3