From 32bcb07c7d7a809fc94fc438835e5e3109ace30a Mon Sep 17 00:00:00 2001
From: Ondrej Ille <ondrej.ille@gmail.com>
Date: Wed, 7 Apr 2021 09:55:16 +0200
Subject: src: Introduce two separate PSL counters (Finish and Start).
Finish counter corresponds to legacy count.
Start counter corresponds to number of times start
state is left (assertion is triggered).
---
src/grt/grt-psl.adb | 21 ++++++++++++-------
src/vhdl/translate/trans-chap7.adb | 2 +-
src/vhdl/translate/trans-chap9.adb | 42 ++++++++++++++++++++++++++++++--------
src/vhdl/translate/trans.ads | 10 +++++++--
src/vhdl/translate/translation.adb | 1 +
5 files changed, 57 insertions(+), 19 deletions(-)
(limited to 'src')
diff --git a/src/grt/grt-psl.adb b/src/grt/grt-psl.adb
index ff736c951..b6362509c 100644
--- a/src/grt/grt-psl.adb
+++ b/src/grt/grt-psl.adb
@@ -75,7 +75,8 @@ package body Grt.Psl is
F : constant FILEs := Report_Stream;
Psl_Dir : Ghdl_Rtin_Psl_Directive_Acc;
Addr : System.Address;
- Val : Ghdl_Index_Type;
+ Finished_Count : Ghdl_Index_Type;
+ Started_Count : Ghdl_Index_Type;
begin
case Rti.Kind is
when Ghdl_Rtiks_Psl =>
@@ -116,16 +117,22 @@ package body Grt.Psl is
Put_U32 (F, Get_Linecol_Line (Psl_Dir.Linecol));
Put_Line (F, ",");
- Put (F, " ""count"": ");
+ Put (F, " ""finished-count"": ");
Addr := Loc_To_Addr (Psl_Dir.Common.Depth, Psl_Dir.Loc, Ctxt);
- Val := To_Ghdl_Index_Ptr (Addr).all;
- Put_U32 (F, Ghdl_U32 (Val));
+ Finished_Count := To_Ghdl_Index_Ptr (Addr).all;
+ Put_U32 (F, Ghdl_U32 (Finished_Count));
+ Put_Line (F, ",");
+
+ Put (F, " ""started-count"": ");
+ Addr := Loc_To_Addr (Psl_Dir.Common.Depth, Psl_Dir.Loc + 4, Ctxt);
+ Started_Count := To_Ghdl_Index_Ptr (Addr).all;
+ Put_U32 (F, Ghdl_U32 (Started_Count));
Put_Line (F, ",");
Put (F, " ""status"": """);
case Rti.Kind is
when Ghdl_Rtik_Psl_Assert =>
- if Val = 0 then
+ if Finished_Count = 0 then
Put (F, "passed");
Inc (Nbr_Assert_Passed);
else
@@ -133,7 +140,7 @@ package body Grt.Psl is
Inc (Nbr_Assert_Failed);
end if;
when Ghdl_Rtik_Psl_Assume =>
- if Val = 0 then
+ if Finished_Count = 0 then
Put (F, "passed");
Inc (Nbr_Assume_Passed);
else
@@ -141,7 +148,7 @@ package body Grt.Psl is
Inc (Nbr_Assume_Failed);
end if;
when Ghdl_Rtik_Psl_Cover =>
- if Val = 0 then
+ if Finished_Count = 0 then
Put (F, "not covered");
Inc (Nbr_Cover_Failed);
else
diff --git a/src/vhdl/translate/trans-chap7.adb b/src/vhdl/translate/trans-chap7.adb
index 369e7564d..618ca996d 100644
--- a/src/vhdl/translate/trans-chap7.adb
+++ b/src/vhdl/translate/trans-chap7.adb
@@ -4527,7 +4527,7 @@ package body Trans.Chap7 is
declare
Info : constant Psl_Info_Acc := Get_Info (Expr);
begin
- return New_Value (Get_Var (Info.Psl_Count_Var));
+ return New_Value (Get_Var (Info.Psl_Finish_Count_Var));
end;
when others =>
diff --git a/src/vhdl/translate/trans-chap9.adb b/src/vhdl/translate/trans-chap9.adb
index 4acb0c01f..f9d8f5054 100644
--- a/src/vhdl/translate/trans-chap9.adb
+++ b/src/vhdl/translate/trans-chap9.adb
@@ -342,17 +342,19 @@ package body Trans.Chap9 is
New_Index_Lit (Unsigned_64 (Get_PSL_Nbr_States (Stmt))));
New_Type_Decl (Create_Identifier ("VECTTYPE"), Info.Psl_Vect_Type);
- -- Create the variables.
+ -- Create count variables
if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then
-- FIXME: endpoint is a variable (and not a signal). This is required
-- to have the right value for the current cycle, but as a
-- consequence, this process must be evaluated before using the
-- endpoint.
- Info.Psl_Count_Var := Create_Var
+ Info.Psl_Finish_Count_Var := Create_Var
(Create_Var_Identifier ("ENDPOINT"), Std_Boolean_Type_Node);
else
- Info.Psl_Count_Var := Create_Var
- (Create_Var_Identifier ("COUNT"), Ghdl_Index_Type);
+ Info.Psl_Finish_Count_Var := Create_Var
+ (Create_Var_Identifier ("FINISH_COUNT"), Ghdl_Index_Type);
+ Info.Psl_Start_Count_Var := Create_Var
+ (Create_Var_Identifier ("START_COUNT"), Ghdl_Index_Type);
end if;
Info.Psl_State_Var := Create_Var
@@ -530,6 +532,7 @@ package body Trans.Chap9 is
Instance : O_Dnode;
Var_I : O_Dnode;
Var_Nvec : O_Dnode;
+ Var_SFlag : O_Dnode;
Report_Proc : O_Dnode;
Label : O_Snode;
Clk_Blk : O_If_Block;
@@ -595,6 +598,8 @@ package body Trans.Chap9 is
New_Lit (Std_Boolean_False_Node));
Inc_Var (Var_I);
Finish_Loop_Stmt (Label);
+ -- Flag for active edge from start state (assertion "started" flag)
+ New_Var_Decl (Var_SFlag, Wki_Flag, O_Storage_Local, Ghdl_Bool_Type);
Finish_Declare_Stmt;
-- Global 'if' statement for the clock.
@@ -602,6 +607,9 @@ package body Trans.Chap9 is
Start_If_Stmt (Clk_Blk,
Translate_Psl_Expr (Get_PSL_Clock (Stmt), False));
+ -- Default "started" flag is not set
+ New_Assign_Stmt (New_Obj (Var_SFlag), New_Lit (Ghdl_Bool_False_Node));
+
-- Default simplified state -> Inactive
New_Assign_Stmt (Get_Var (Info.Psl_State_Var),
New_Lit (Trans.Rtis.Ghdl_Rti_Psl_State_Inactive));
@@ -641,10 +649,17 @@ package body Trans.Chap9 is
New_Lit (D_Lit))));
Cond := New_Dyadic_Op
(ON_And, Cond, Translate_Psl_Expr (Get_Edge_Expr (E), False));
+
+ -- If NFA edge expression is valid -> Fire-up destination state.
Start_If_Stmt (E_Blk, Cond);
New_Assign_Stmt
(New_Indexed_Element (New_Obj (Var_Nvec), New_Lit (D_Lit)),
New_Lit (Std_Boolean_True_Node));
+ -- If we fire from start state -> set "started" flag.
+ if S = Get_First_State (NFA) then
+ New_Assign_Stmt (New_Obj (Var_SFlag),
+ New_Lit (Ghdl_Bool_True_Node));
+ end if;
Finish_If_Stmt (E_Blk);
Close_Temp;
@@ -667,7 +682,7 @@ package body Trans.Chap9 is
(Unsigned_64 (S_Num)))));
if Get_Kind (Stmt) = Iir_Kind_Psl_Endpoint_Declaration then
- New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), Cond);
+ New_Assign_Stmt (Get_Var (Info.Psl_Finish_Count_Var), Cond);
else
Start_If_Stmt (S_Blk, Cond);
Open_Temp;
@@ -697,14 +712,23 @@ package body Trans.Chap9 is
Error_Kind ("Translate_Psl_Directive_Statement", Stmt);
end case;
New_Assign_Stmt
- (Get_Var (Info.Psl_Count_Var),
+ (Get_Var (Info.Psl_Finish_Count_Var),
New_Dyadic_Op (ON_Add_Ov,
- New_Value (Get_Var (Info.Psl_Count_Var)),
+ New_Value (Get_Var (Info.Psl_Finish_Count_Var)),
New_Lit (Ghdl_Index_1)));
Close_Temp;
Finish_If_Stmt (S_Blk);
end if;
+ -- Check "started" flag, increment started count if set
+ Start_If_Stmt (S_Blk, New_Value (New_Obj (Var_SFlag)));
+ New_Assign_Stmt
+ (Get_Var (Info.Psl_Start_Count_Var),
+ New_Dyadic_Op (ON_Add_Ov,
+ New_Value (Get_Var (Info.Psl_Start_Count_Var)),
+ New_Lit (Ghdl_Index_1)));
+ Finish_If_Stmt (S_Blk);
+
-- Assign state vector.
Start_Declare_Stmt;
New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type);
@@ -797,7 +821,7 @@ package body Trans.Chap9 is
Start_If_Stmt
(S_Blk,
New_Compare_Op (ON_Eq,
- New_Value (Get_Var (Info.Psl_Count_Var)),
+ New_Value (Get_Var (Info.Psl_Finish_Count_Var)),
New_Lit (Ghdl_Index_0),
Ghdl_Bool_Type));
Start_Association (Assocs, Report_Proc);
@@ -1900,7 +1924,7 @@ package body Trans.Chap9 is
else
Init := Ghdl_Index_0;
end if;
- New_Assign_Stmt (Get_Var (Info.Psl_Count_Var), New_Lit (Init));
+ New_Assign_Stmt (Get_Var (Info.Psl_Finish_Count_Var), New_Lit (Init));
end Elab_Psl_Directive;
procedure Elab_Implicit_Guard_Signal
diff --git a/src/vhdl/translate/trans.ads b/src/vhdl/translate/trans.ads
index 4e0b9b959..ecfc79203 100644
--- a/src/vhdl/translate/trans.ads
+++ b/src/vhdl/translate/trans.ads
@@ -172,6 +172,7 @@ package Trans is
Wki_Base : O_Ident;
Wki_Bounds : O_Ident;
Wki_Locvars : O_Ident;
+ Wki_Flag : O_Ident;
-- ALLOCATION_KIND defines the type of memory storage.
-- ALLOC_STACK means the object is allocated on the local stack and
@@ -1946,8 +1947,13 @@ package Trans is
-- Simplified Assertion state (for dumping)
Psl_State_Var : Var_Type;
- -- Counter variable (nbr of failures or coverage)
- Psl_Count_Var : Var_Type;
+ -- Number of times assertion finished
+ -- For cover points: Number of coveres
+ -- For assertions: Number of failures
+ Psl_Finish_Count_Var : Var_Type;
+
+ -- Number of times assertion was started
+ Psl_Start_Count_Var : Var_Type;
-- RTI for the process.
Psl_Rti_Const : O_Dnode := O_Dnode_Null;
diff --git a/src/vhdl/translate/translation.adb b/src/vhdl/translate/translation.adb
index b8d19e6ce..c02326ea8 100644
--- a/src/vhdl/translate/translation.adb
+++ b/src/vhdl/translate/translation.adb
@@ -416,6 +416,7 @@ package body Translation is
Wki_Base := Get_Identifier ("BASE");
Wki_Bounds := Get_Identifier ("BOUNDS");
Wki_Locvars := Get_Identifier ("LOCVARS");
+ Wki_Flag := Get_Identifier ("FLAG");
Sizetype := New_Unsigned_Type (32);
New_Type_Decl (Get_Identifier ("__ghdl_size_type"), Sizetype);
--
cgit v1.2.3