diff options
| -rw-r--r-- | canon.adb | 6 | ||||
| -rw-r--r-- | configuration.adb | 1 | ||||
| -rw-r--r-- | disp_tree.adb | 9 | ||||
| -rw-r--r-- | disp_vhdl.adb | 27 | ||||
| -rw-r--r-- | errorout.adb | 2 | ||||
| -rw-r--r-- | iirs.adb | 18 | ||||
| -rw-r--r-- | iirs.ads | 3 | ||||
| -rw-r--r-- | parse.adb | 14 | ||||
| -rw-r--r-- | psl/psl-prints.adb | 7 | ||||
| -rw-r--r-- | scanner.adb | 8 | ||||
| -rw-r--r-- | sem_stmts.adb | 3 | ||||
| -rw-r--r-- | testsuite/gna/ticket19/Makefile | 12 | ||||
| -rw-r--r-- | testsuite/gna/ticket19/psl_test_cover.vhd | 53 | ||||
| -rw-r--r-- | testsuite/gna/ticket19/psl_test_cover2.vhd | 60 | ||||
| -rw-r--r-- | testsuite/gna/ticket19/psl_test_cover3.vhd | 53 | ||||
| -rwxr-xr-x | testsuite/gna/ticket19/testsuite.sh | 16 | ||||
| -rw-r--r-- | tokens.adb | 2 | ||||
| -rw-r--r-- | tokens.ads | 1 | ||||
| -rw-r--r-- | translate/ghdldrv/ghdlprint.adb | 1 | ||||
| -rw-r--r-- | translate/ghdldrv/ghdlrun.adb | 6 | ||||
| -rw-r--r-- | translate/grt/grt-lib.adb | 36 | ||||
| -rw-r--r-- | translate/grt/grt-lib.ads | 31 | ||||
| -rw-r--r-- | translate/trans_decls.ads | 3 | ||||
| -rw-r--r-- | translate/translation.adb | 263 |
24 files changed, 503 insertions, 132 deletions
@@ -1642,7 +1642,8 @@ package body Canon is Canon_Concurrent_Stmts (Top, El); end; - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => declare use PSL.Nodes; Prop : PSL_Node; @@ -1654,6 +1655,8 @@ package body Canon is -- Generate the NFA. Fa := PSL.Build.Build_FA (Prop); Set_PSL_NFA (El, Fa); + + -- FIXME: report/severity. end; when Iir_Kind_Psl_Default_Clock => @@ -2525,6 +2528,7 @@ package body Canon is when Iir_Kind_Sensitized_Process_Statement | Iir_Kind_Process_Statement | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Psl_Default_Clock | Iir_Kind_Psl_Declaration | Iir_Kind_Simple_Simultaneous_Statement => diff --git a/configuration.adb b/configuration.adb index 43dbafd7b..ab03bca3b 100644 --- a/configuration.adb +++ b/configuration.adb @@ -220,6 +220,7 @@ package body Configuration is when Iir_Kind_Process_Statement | Iir_Kind_Sensitized_Process_Statement | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Psl_Default_Clock | Iir_Kind_Psl_Declaration | Iir_Kind_Simple_Simultaneous_Statement => diff --git a/disp_tree.adb b/disp_tree.adb index 1747280a5..40a949cff 100644 --- a/disp_tree.adb +++ b/disp_tree.adb @@ -1504,10 +1504,15 @@ package body Disp_Tree is Disp_Tree (Get_Severity_Expression (Tree), Ntab); Header ("attribute_value_chain:"); Disp_Tree_Flat_Chain (Get_Attribute_Value_Chain (Tree), Ntab); - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => + PSL.Dump_Tree.Dump_Tree (Get_Psl_Property (Tree), True); + Header ("report expression:"); + Disp_Tree (Get_Report_Expression (Tree), Ntab); + Header ("severity expression:"); + Disp_Tree (Get_Severity_Expression (Tree), Ntab); Header ("attribute_value_chain:"); Disp_Tree_Flat_Chain (Get_Attribute_Value_Chain (Tree), Ntab); - PSL.Dump_Tree.Dump_Tree (Get_Psl_Property (Tree), True); when Iir_Kind_Psl_Default_Clock => null; diff --git a/disp_vhdl.adb b/disp_vhdl.adb index 792dc6fe3..fd75ea0dc 100644 --- a/disp_vhdl.adb +++ b/disp_vhdl.adb @@ -2274,7 +2274,7 @@ package body Disp_Vhdl is Put_Line (";"); end Disp_Psl_Default_Clock; - procedure Disp_Psl_Assert_Statement (Stmt : Iir) + procedure Disp_PSL_NFA (N : PSL.Nodes.NFA) is use PSL.NFAs; use PSL.Nodes; @@ -2285,15 +2285,10 @@ package body Disp_Vhdl is Put (Str (2 .. Str'Last)); end Disp_State; - N : NFA; S : NFA_State; E : NFA_Edge; begin - Put ("--psl assert "); - Disp_Psl_Expression (Get_Psl_Property (Stmt)); - Put_Line (";"); - N := Get_PSL_NFA (Stmt); - if True and then N /= No_NFA then + if N /= No_NFA then S := Get_First_State (N); while S /= No_State loop E := Get_First_Src_Edge (S); @@ -2310,8 +2305,24 @@ package body Disp_Vhdl is S := Get_Next_State (S); end loop; end if; + end Disp_PSL_NFA; + + procedure Disp_Psl_Assert_Statement (Stmt : Iir) is + begin + Put ("--psl assert "); + Disp_Psl_Expression (Get_Psl_Property (Stmt)); + Put_Line (";"); + Disp_PSL_NFA (Get_PSL_NFA (Stmt)); end Disp_Psl_Assert_Statement; + procedure Disp_Psl_Cover_Statement (Stmt : Iir) is + begin + Put ("--psl cover "); + Disp_Psl_Expression (Get_Psl_Property (Stmt)); + Put_Line (";"); + Disp_PSL_NFA (Get_PSL_NFA (Stmt)); + end Disp_Psl_Cover_Statement; + procedure Disp_Simple_Simultaneous_Statement (Stmt : Iir) is begin @@ -2346,6 +2357,8 @@ package body Disp_Vhdl is Disp_Psl_Default_Clock (Stmt); when Iir_Kind_Psl_Assert_Statement => Disp_Psl_Assert_Statement (Stmt); + when Iir_Kind_Psl_Cover_Statement => + Disp_Psl_Cover_Statement (Stmt); when Iir_Kind_Simple_Simultaneous_Statement => Disp_Simple_Simultaneous_Statement (Stmt); when others => diff --git a/errorout.adb b/errorout.adb index 51611f510..d0d9aba8d 100644 --- a/errorout.adb +++ b/errorout.adb @@ -770,6 +770,8 @@ package body Errorout is return Disp_Label (Node, "concurrent assertion"); when Iir_Kind_Psl_Assert_Statement => return Disp_Label (Node, "PSL assertion"); + when Iir_Kind_Psl_Cover_Statement => + return Disp_Label (Node, "PSL cover"); when Iir_Kind_Psl_Default_Clock => return "PSL default clock"; @@ -544,6 +544,7 @@ package body Iirs is | Iir_Kind_Concurrent_Selected_Signal_Assignment | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Block_Statement | Iir_Kind_Generate_Statement | Iir_Kind_Component_Instantiation_Statement @@ -1885,6 +1886,7 @@ package body Iirs is | Iir_Kind_Concurrent_Selected_Signal_Assignment | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement | Iir_Kind_Block_Statement | Iir_Kind_Generate_Statement @@ -2170,6 +2172,7 @@ package body Iirs is | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Psl_Default_Clock | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement | Iir_Kind_Block_Statement | Iir_Kind_Generate_Statement @@ -3463,6 +3466,7 @@ package body Iirs is | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Psl_Default_Clock | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement | Iir_Kind_Block_Statement | Iir_Kind_Generate_Statement @@ -3511,6 +3515,7 @@ package body Iirs is | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Psl_Default_Clock | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement | Iir_Kind_Block_Statement | Iir_Kind_Generate_Statement @@ -3592,6 +3597,7 @@ package body Iirs is | Iir_Kind_Concurrent_Selected_Signal_Assignment | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement | Iir_Kind_Block_Statement | Iir_Kind_Generate_Statement @@ -4861,6 +4867,7 @@ package body Iirs is case Get_Kind (Target) is when Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Assertion_Statement | Iir_Kind_Report_Statement => null; @@ -4886,6 +4893,7 @@ package body Iirs is case Get_Kind (Target) is when Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Assertion_Statement | Iir_Kind_Report_Statement => null; @@ -5483,6 +5491,7 @@ package body Iirs is | Iir_Kind_Concurrent_Assertion_Statement | Iir_Kind_Psl_Default_Clock | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement | Iir_Kind_Concurrent_Procedure_Call_Statement | Iir_Kind_Block_Statement | Iir_Kind_Generate_Statement @@ -7229,7 +7238,8 @@ package body Iirs is procedure Check_Kind_For_Psl_Property (Target : Iir) is begin case Get_Kind (Target) is - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => null; when others => Failed ("Psl_Property", Target); @@ -7318,7 +7328,8 @@ package body Iirs is begin case Get_Kind (Target) is when Iir_Kind_Psl_Declaration - | Iir_Kind_Psl_Assert_Statement => + | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => null; when others => Failed ("PSL_Clock", Target); @@ -7341,7 +7352,8 @@ package body Iirs is begin case Get_Kind (Target) is when Iir_Kind_Psl_Declaration - | Iir_Kind_Psl_Assert_Statement => + | Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => null; when others => Failed ("PSL_NFA", Target); @@ -1928,6 +1928,7 @@ package Iirs is -- Get/Set_Identifier (Alias Field3) -- Iir_Kind_Psl_Assert_Statement (Medium) + -- Iir_Kind_Psl_Cover_Statement (Medium) -- -- Get/Set_Parent (Field0) -- @@ -2916,6 +2917,7 @@ package Iirs is Iir_Kind_Concurrent_Assertion_Statement, Iir_Kind_Psl_Default_Clock, Iir_Kind_Psl_Assert_Statement, + Iir_Kind_Psl_Cover_Statement, Iir_Kind_Concurrent_Procedure_Call_Statement, Iir_Kind_Block_Statement, Iir_Kind_Generate_Statement, @@ -3679,6 +3681,7 @@ package Iirs is --Iir_Kind_Concurrent_Assertion_Statement --Iir_Kind_Psl_Default_Clock --Iir_Kind_Psl_Assert_Statement + --Iir_Kind_Psl_Cover_Statement --Iir_Kind_Concurrent_Procedure_Call_Statement --Iir_Kind_Block_Statement --Iir_Kind_Generate_Statement @@ -5640,7 +5640,16 @@ package body Parse is is Res : Iir; begin - Res := Create_Iir (Iir_Kind_Psl_Assert_Statement); + case Current_Token is + when Tok_Psl_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; + + -- Scan extended PSL tokens. Scanner.Flag_Psl := True; -- Skip 'assert' @@ -5791,7 +5800,8 @@ package body Parse is | Tok_Psl_Endpoint => Postponed_Not_Allowed; Stmt := Parse_Psl_Declaration; - when Tok_Psl_Assert => + when Tok_Psl_Assert + | Tok_Psl_Cover => Postponed_Not_Allowed; Stmt := Parse_Psl_Assert_Statement; when others => diff --git a/psl/psl-prints.adb b/psl/psl-prints.adb index 6e4f37022..80da47dab 100644 --- a/psl/psl-prints.adb +++ b/psl/psl-prints.adb @@ -41,7 +41,8 @@ package body PSL.Prints is return Prio_Seq_And; when N_Imp_Seq | N_Overlap_Imp_Seq - | N_Log_Imp_Prop => + | N_Log_Imp_Prop + | N_Imp_Bool => return Prio_Bool_Imp; when N_Name_Decl | N_Number @@ -153,6 +154,10 @@ package body PSL.Prints is Print_Expr (Get_Left (N), Prio); Put (" || "); Print_Expr (Get_Right (N), Prio); + when N_Imp_Bool => + Print_Expr (Get_Left (N), Prio); + Put (" -> "); + Print_Expr (Get_Right (N), Prio); when others => Error_Kind ("print_expr", N); end case; diff --git a/scanner.adb b/scanner.adb index 70fe6ff0f..707519c53 100644 --- a/scanner.adb +++ b/scanner.adb @@ -952,6 +952,8 @@ package body Scanner is return True; end Scan_Comment_Identifier; + -- Scan tokens within a comment. Return TRUE if Current_Token was set, + -- return FALSE to discard the comment (ie treat it like a real comment). function Scan_Comment return Boolean is use Std_Names; @@ -966,10 +968,12 @@ package body Scanner is case Id is when Name_Psl => + -- Scan first identifier after '-- psl'. if not Scan_Comment_Identifier then return False; end if; - case Name_Table.Get_Identifier is + Id := Name_Table.Get_Identifier; + case Id is when Name_Property => Current_Token := Tok_Psl_Property; when Name_Sequence => @@ -978,6 +982,8 @@ package body Scanner is Current_Token := Tok_Psl_Endpoint; when Name_Assert => Current_Token := Tok_Psl_Assert; + when Name_Cover => + Current_Token := Tok_Psl_Cover; when Name_Default => Current_Token := Tok_Psl_Default; when others => diff --git a/sem_stmts.adb b/sem_stmts.adb index 77e5ac419..864cec640 100644 --- a/sem_stmts.adb +++ b/sem_stmts.adb @@ -1801,7 +1801,8 @@ package body Sem_Stmts is end; when Iir_Kind_Psl_Declaration => Sem_Psl.Sem_Psl_Declaration (El); - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => Sem_Psl.Sem_Psl_Assert_Statement (El); when Iir_Kind_Psl_Default_Clock => Sem_Psl.Sem_Psl_Default_Clock (El); diff --git a/testsuite/gna/ticket19/Makefile b/testsuite/gna/ticket19/Makefile new file mode 100644 index 000000000..215246320 --- /dev/null +++ b/testsuite/gna/ticket19/Makefile @@ -0,0 +1,12 @@ +psl_test_cover: psl_test_cover.vhd + ghdl -a --std=02 -fpsl psl_test_cover.vhd + ghdl -e --std=02 -fpsl psl_test_cover + ./psl_test_cover --stop-time=200ns + +all: clean psl_test_cover + +.PHONY: clean +clean: + rm -f *.cf + rm -f *.o + rm -f psl_test_cover
\ No newline at end of file diff --git a/testsuite/gna/ticket19/psl_test_cover.vhd b/testsuite/gna/ticket19/psl_test_cover.vhd new file mode 100644 index 000000000..4f3666f19 --- /dev/null +++ b/testsuite/gna/ticket19/psl_test_cover.vhd @@ -0,0 +1,53 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + + + +entity psl_test_cover is +end entity psl_test_cover; + + +architecture test of psl_test_cover is + + + signal s_rst_n : std_logic := '0'; + signal s_clk : std_logic := '0'; + signal s_write : std_logic; + signal s_read : std_logic; + + +begin + + + s_rst_n <= '1' after 100 ns; + s_clk <= not s_clk after 10 ns; + + + TestP : process is + begin + report "RUNNING PSL_TEST_COVER test case"; + report "================================"; + s_write <= '0'; + s_read <= '0'; + wait until s_rst_n = '1' and rising_edge(s_clk); + s_write <= '1'; -- cover should hit + wait until rising_edge(s_clk); + s_read <= '1'; -- assertion should hit + wait until rising_edge(s_clk); + s_write <= '0'; + s_read <= '0'; + wait; + end process TestP; + + + + -- psl statements + + -- psl default clock is rising_edge(s_clk); + + -- cover directive seems not supported (ignored by GHDL) + -- psl cover always (s_write -> not(s_read)); + + +end architecture test;
\ No newline at end of file diff --git a/testsuite/gna/ticket19/psl_test_cover2.vhd b/testsuite/gna/ticket19/psl_test_cover2.vhd new file mode 100644 index 000000000..16d6ac810 --- /dev/null +++ b/testsuite/gna/ticket19/psl_test_cover2.vhd @@ -0,0 +1,60 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + + + +entity psl_test_cover2 is +end entity psl_test_cover2; + + +architecture test of psl_test_cover2 is + + + signal s_rst_n : std_logic := '0'; + signal s_clk : std_logic := '0'; + signal s_write : std_logic; + signal s_read : std_logic; + + +begin + + + s_rst_n <= '1' after 20 ns; + s_clk <= not s_clk after 10 ns; + + + TestP : process is + begin + report "RUNNING PSL_TEST_COVER test case"; + report "================================"; + s_write <= '0'; + s_read <= '0'; + wait until s_rst_n = '1' and rising_edge(s_clk); + s_write <= '1'; -- cover should hit + wait until rising_edge(s_clk); + s_read <= '1'; -- assertion should hit + wait until rising_edge(s_clk); + s_write <= '0'; + s_read <= '0'; + wait until rising_edge(s_clk); + s_write <= '1'; -- cover should hit + wait until rising_edge(s_clk); + s_read <= '1'; -- assertion should hit + wait until rising_edge(s_clk); + s_write <= '0'; + s_read <= '0'; + wait; + end process TestP; + + + + -- psl statements + + -- psl default clock is rising_edge(s_clk); + + -- cover directive seems not supported (ignored by GHDL) + -- psl cover always (s_write -> not(s_read)); + + +end architecture test; diff --git a/testsuite/gna/ticket19/psl_test_cover3.vhd b/testsuite/gna/ticket19/psl_test_cover3.vhd new file mode 100644 index 000000000..0ef5d6ed9 --- /dev/null +++ b/testsuite/gna/ticket19/psl_test_cover3.vhd @@ -0,0 +1,53 @@ +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + + + +entity psl_test_cover3 is +end entity psl_test_cover3; + + +architecture test of psl_test_cover3 is + + + signal s_rst_n : std_logic := '0'; + signal s_clk : std_logic := '0'; + signal s_write : std_logic; + signal s_read : std_logic; + + +begin + + + s_rst_n <= '1' after 20 ns; + s_clk <= not s_clk after 10 ns; + + + TestP : process is + begin + report "RUNNING PSL_TEST_COVER test case"; + report "================================"; + s_write <= '0'; + s_read <= '0'; + wait until s_rst_n = '1' and rising_edge(s_clk); + s_write <= '1'; -- cover should hit + wait until rising_edge(s_clk); + s_read <= '0'; -- no hit + wait until rising_edge(s_clk); + s_write <= '0'; + s_read <= '0'; + wait; + end process TestP; + + + + -- psl statements + + -- psl default clock is rising_edge(s_clk); + + -- cover directive seems not supported (ignored by GHDL) + -- psl cover always (s_write -> not(s_read)); + + +end architecture test; diff --git a/testsuite/gna/ticket19/testsuite.sh b/testsuite/gna/ticket19/testsuite.sh new file mode 100755 index 000000000..a594dfcaf --- /dev/null +++ b/testsuite/gna/ticket19/testsuite.sh @@ -0,0 +1,16 @@ +#!/bin/sh + +. ../../testenv.sh + +GHDL_FLAGS="-fpsl --std=02" + +analyze psl_test_cover.vhd +elab_simulate psl_test_cover --stop-time=200ns + +analyze psl_test_cover2.vhd +elab_simulate psl_test_cover2 --stop-time=200ns + +analyze psl_test_cover3.vhd +elab_simulate psl_test_cover3 --stop-time=200ns + +clean diff --git a/tokens.adb b/tokens.adb index 415486cab..5d27be8d9 100644 --- a/tokens.adb +++ b/tokens.adb @@ -407,6 +407,8 @@ package body Tokens is return "endpoint"; when Tok_Psl_Assert => return "assert"; + when Tok_Psl_Cover => + return "cover"; when Tok_Psl_Const => return "const"; when Tok_Psl_Boolean => diff --git a/tokens.ads b/tokens.ads index bb431b95a..a0339a52c 100644 --- a/tokens.ads +++ b/tokens.ads @@ -241,6 +241,7 @@ package Tokens is Tok_Psl_Sequence, Tok_Psl_Endpoint, Tok_Psl_Assert, + Tok_Psl_Cover, Tok_Psl_Const, Tok_Psl_Boolean, diff --git a/translate/ghdldrv/ghdlprint.adb b/translate/ghdldrv/ghdlprint.adb index 325405911..3850ce40c 100644 --- a/translate/ghdldrv/ghdlprint.adb +++ b/translate/ghdldrv/ghdlprint.adb @@ -385,6 +385,7 @@ package body Ghdlprint is | Tok_Psl_Sequence | Tok_Psl_Endpoint | Tok_Psl_Assert + | Tok_Psl_Cover | Tok_Psl_Boolean | Tok_Psl_Const | Tok_Inf diff --git a/translate/ghdldrv/ghdlrun.adb b/translate/ghdldrv/ghdlrun.adb index 7dbce3ded..676c82824 100644 --- a/translate/ghdldrv/ghdlrun.adb +++ b/translate/ghdldrv/ghdlrun.adb @@ -246,8 +246,6 @@ package body Ghdlrun is Grt.Lib.Ghdl_Bound_Check_Failed_L1'Address); Def (Trans_Decls.Ghdl_Malloc0, Grt.Lib.Ghdl_Malloc0'Address); - Def (Trans_Decls.Ghdl_Assert_Default_Report, - Grt.Lib.Ghdl_Assert_Default_Report'Address); Def (Trans_Decls.Ghdl_Std_Ulogic_To_Boolean_Array, Grt.Lib.Ghdl_Std_Ulogic_To_Boolean_Array'Address); @@ -257,6 +255,10 @@ package body Ghdlrun is Grt.Lib.Ghdl_Assert_Failed'Address); Def (Trans_Decls.Ghdl_Psl_Assert_Failed, Grt.Lib.Ghdl_Psl_Assert_Failed'Address); + Def (Trans_Decls.Ghdl_Psl_Cover, + Grt.Lib.Ghdl_Psl_Cover'Address); + Def (Trans_Decls.Ghdl_Psl_Cover_Failed, + Grt.Lib.Ghdl_Psl_Cover_Failed'Address); Def (Trans_Decls.Ghdl_Program_Error, Grt.Lib.Ghdl_Program_Error'Address); Def (Trans_Decls.Ghdl_Malloc, diff --git a/translate/grt/grt-lib.adb b/translate/grt/grt-lib.adb index 2fe1bc6aa..fcbbecb64 100644 --- a/translate/grt/grt-lib.adb +++ b/translate/grt/grt-lib.adb @@ -43,6 +43,7 @@ package body Grt.Lib is procedure Do_Report (Msg : String; Str : Std_String_Ptr; + Default_Str : String; Severity : Integer; Loc : Ghdl_Location_Ptr; Unit : Ghdl_Rti_Access) @@ -96,7 +97,11 @@ package body Grt.Lib is Report_C ("???"); end case; Report_C ("): "); - Report_E (Str); + if Str /= null then + Report_E (Str); + else + Report_E (Default_Str); + end if; if Level >= Grt.Options.Severity_Level then Error_C (Msg); Error_E (" failed"); @@ -110,7 +115,8 @@ package body Grt.Lib is Unit : Ghdl_Rti_Access) is begin - Do_Report ("assertion", Str, Severity, Loc, Unit); + Do_Report ("assertion", + Str, "Assertion violation", Severity, Loc, Unit); end Ghdl_Assert_Failed; procedure Ghdl_Psl_Assert_Failed @@ -120,9 +126,31 @@ package body Grt.Lib is Unit : Ghdl_Rti_Access) is begin - Do_Report ("psl assertion", Str, Severity, Loc, Unit); + Do_Report ("psl assertion", + Str, "Assertion violation", Severity, Loc, Unit); end Ghdl_Psl_Assert_Failed; + procedure Ghdl_Psl_Cover + (Str : Std_String_Ptr; + Severity : Integer; + Loc : Ghdl_Location_Ptr; + Unit : Ghdl_Rti_Access) + is + begin + Do_Report ("psl cover", Str, "sequence covered", Severity, Loc, Unit); + end Ghdl_Psl_Cover; + + procedure Ghdl_Psl_Cover_Failed + (Str : Std_String_Ptr; + Severity : Integer; + Loc : Ghdl_Location_Ptr; + Unit : Ghdl_Rti_Access) + is + begin + Do_Report ("psl cover failure", + Str, "sequence not covered", Severity, Loc, Unit); + end Ghdl_Psl_Cover_Failed; + procedure Ghdl_Report (Str : Std_String_Ptr; Severity : Integer; @@ -130,7 +158,7 @@ package body Grt.Lib is Unit : Ghdl_Rti_Access) is begin - Do_Report ("report", Str, Severity, Loc, Unit); + Do_Report ("report", Str, "Assertion violation", Severity, Loc, Unit); end Ghdl_Report; procedure Ghdl_Program_Error (Filename : Ghdl_C_String; diff --git a/translate/grt/grt-lib.ads b/translate/grt/grt-lib.ads index f8cc92806..580406dcc 100644 --- a/translate/grt/grt-lib.ads +++ b/translate/grt/grt-lib.ads @@ -43,6 +43,19 @@ package Grt.Lib is Loc : Ghdl_Location_Ptr; Unit : Ghdl_Rti_Access); + -- Called when a sequence is covered (in a cover directive) + procedure Ghdl_Psl_Cover + (Str : Std_String_Ptr; + Severity : Integer; + Loc : Ghdl_Location_Ptr; + Unit : Ghdl_Rti_Access); + + procedure Ghdl_Psl_Cover_Failed + (Str : Std_String_Ptr; + Severity : Integer; + Loc : Ghdl_Location_Ptr; + Unit : Ghdl_Rti_Access); + procedure Ghdl_Report (Str : Std_String_Ptr; Severity : Integer; @@ -77,22 +90,6 @@ package Grt.Lib is function Ghdl_Real_Exp (X : Ghdl_Real; Exp : Ghdl_I32) return Ghdl_Real; - -- Create a vhdl string. - Ghdl_Assert_Default_Report_Arr : constant String := "Assertion violation"; - Ghdl_Assert_Default_Report_Bounds : constant Std_String_Bound := - (Dim_1 => (Left => 1, - Right => Ghdl_Assert_Default_Report_Arr'Length, - Dir => Dir_To, - Length => Ghdl_Assert_Default_Report_Arr'Length)); - Ghdl_Assert_Default_Report : constant Ghdl_Uc_Array := - (Base => Ghdl_Assert_Default_Report_Arr'Address, - Bounds => Ghdl_Assert_Default_Report_Bounds'Address); - - -- Unfortunatly, with gnat 3.15p, we cannot use a deferred constant with - -- the export pragma. - pragma Export (C, Ghdl_Assert_Default_Report, - "__ghdl_assert_default_report"); - type Ghdl_Std_Ulogic_Boolean_Array_Type is array (Ghdl_E8 range 0 .. 8) of Ghdl_B2; @@ -112,6 +109,8 @@ private pragma Export (C, Ghdl_Assert_Failed, "__ghdl_assert_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"); pragma Export (C, Ghdl_Report, "__ghdl_report"); pragma Export (C, Ghdl_Bound_Check_Failed_L0, diff --git a/translate/trans_decls.ads b/translate/trans_decls.ads index 23bd6d9dc..f5aab5c58 100644 --- a/translate/trans_decls.ads +++ b/translate/trans_decls.ads @@ -21,6 +21,9 @@ package Trans_Decls is -- Procedures called in case of assert failed. Ghdl_Assert_Failed : O_Dnode; Ghdl_Psl_Assert_Failed : O_Dnode; + + Ghdl_Psl_Cover : O_Dnode; + Ghdl_Psl_Cover_Failed : O_Dnode; -- Procedure for report statement. Ghdl_Report : O_Dnode; -- Ortho node for default report message. diff --git a/translate/translation.adb b/translate/translation.adb index 4c3360dee..1284bad2e 100644 --- a/translate/translation.adb +++ b/translate/translation.adb @@ -753,7 +753,7 @@ package body Translation is Kind_Interface, Kind_Disconnect, Kind_Process, - Kind_Psl_Assert, + Kind_Psl_Directive, Kind_Loop, Kind_Block, Kind_Component, @@ -1308,7 +1308,7 @@ package body Translation is -- RTI for the process. Process_Rti_Const : O_Dnode := O_Dnode_Null; - when Kind_Psl_Assert => + when Kind_Psl_Directive => -- Type of assert declarations record. Psl_Decls_Type : O_Tnode; @@ -1329,6 +1329,9 @@ package body Translation is -- State vector variable. Psl_Vect_Var : Var_Acc; + -- Boolean variable (for cover) + Psl_Bool_Var : Var_Acc; + -- RTI for the process. Psl_Rti_Const : O_Dnode := O_Dnode_Null; when Kind_Loop => @@ -1440,7 +1443,7 @@ package body Translation is subtype Object_Info_Acc is Ortho_Info_Acc (Kind_Object); subtype Alias_Info_Acc is Ortho_Info_Acc (Kind_Alias); subtype Proc_Info_Acc is Ortho_Info_Acc (Kind_Process); - subtype Psl_Info_Acc is Ortho_Info_Acc (Kind_Psl_Assert); + subtype Psl_Info_Acc is Ortho_Info_Acc (Kind_Psl_Directive); subtype Loop_Info_Acc is Ortho_Info_Acc (Kind_Loop); subtype Block_Info_Acc is Ortho_Info_Acc (Kind_Block); subtype Comp_Info_Acc is Ortho_Info_Acc (Kind_Component); @@ -19383,8 +19386,7 @@ package body Translation is Loc := Chap4.Get_Location (Stmt); Expr := Get_Report_Expression (Stmt); if Expr = Null_Iir then - Msg := New_Address (New_Obj (Ghdl_Assert_Default_Report), - Std_String_Ptr_Node); + Msg := New_Lit (New_Null_Access (Std_String_Ptr_Node)); else Msg := Chap7.Translate_Expression (Expr, String_Type_Definition); end if; @@ -21887,7 +21889,7 @@ package body Translation is Info.Process_Parent_Field := Field; end Translate_Process_Declarations; - procedure Translate_Psl_Assert_Declarations (Stmt : Iir) + procedure Translate_Psl_Directive_Declarations (Stmt : Iir) is use PSL.Nodes; use PSL.NFAs; @@ -21902,7 +21904,7 @@ package body Translation is -- Create process record. Push_Identifier_Prefix (Mark, Get_Identifier (Stmt)); Push_Instance_Factory (O_Tnode_Null); - Info := Add_Info (Stmt, Kind_Psl_Assert); + Info := Add_Info (Stmt, Kind_Psl_Directive); N := Get_PSL_NFA (Stmt); Labelize_States (N, Info.Psl_Vect_Len); @@ -21914,6 +21916,11 @@ package body Translation is Info.Psl_Vect_Var := Create_Var (Create_Var_Identifier ("VECT"), Info.Psl_Vect_Type); + if Get_Kind (Stmt) = Iir_Kind_Psl_Cover_Statement then + Info.Psl_Bool_Var := + Create_Var (Create_Var_Identifier ("BOOL"), Ghdl_Bool_Type); + end if; + Pop_Instance_Factory (Itype); New_Type_Decl (Create_Identifier ("INSTTYPE"), Itype); Pop_Identifier_Prefix (Mark); @@ -21925,7 +21932,7 @@ package body Translation is -- Set info in child record. Info.Psl_Decls_Type := Itype; Info.Psl_Parent_Field := Field; - end Translate_Psl_Assert_Declarations; + end Translate_Psl_Directive_Declarations; function Translate_Psl_Expr (Expr : PSL_Node; Eos : Boolean) return O_Enode @@ -21999,13 +22006,26 @@ package body Translation is return False; end Psl_Need_Finalizer; - procedure Translate_Psl_Assert_Statement + procedure Create_Psl_Final_Proc + (Stmt : Iir; Base : Block_Info_Acc; Instance : out O_Dnode) + is + Inter_List : O_Inter_List; + Info : constant Psl_Info_Acc := Get_Info (Stmt); + begin + Start_Procedure_Decl (Inter_List, Create_Identifier ("FINALPROC"), + O_Storage_Private); + New_Interface_Decl (Inter_List, Instance, Wki_Instance, + Base.Block_Decls_Ptr_Type); + Finish_Subprogram_Decl (Inter_List, Info.Psl_Proc_Final_Subprg); + end Create_Psl_Final_Proc; + + procedure Translate_Psl_Directive_Statement (Stmt : Iir; Base : Block_Info_Acc) is use PSL.NFAs; Inter_List : O_Inter_List; Instance : O_Dnode; - Info : Psl_Info_Acc; + Info : constant Psl_Info_Acc := Get_Info (Stmt); Var_I : O_Dnode; Var_Nvec : O_Dnode; Label : O_Snode; @@ -22020,7 +22040,6 @@ package body Translation is NFA : PSL_NFA; D_Lit : O_Cnode; begin - Info := Get_Info (Stmt); Start_Procedure_Decl (Inter_List, Create_Identifier ("PROC"), O_Storage_Private); New_Interface_Decl (Inter_List, Instance, Wki_Instance, @@ -22035,6 +22054,18 @@ package body Translation is -- New state vector. New_Var_Decl (Var_Nvec, Wki_Res, O_Storage_Local, Info.Psl_Vect_Type); + -- For cover directive, return now if already covered. + case Get_Kind (Stmt) is + when Iir_Kind_Psl_Assert_Statement => + null; + when Iir_Kind_Psl_Cover_Statement => + Start_If_Stmt (S_Blk, New_Value (Get_Var (Info.Psl_Bool_Var))); + New_Return_Stmt; + Finish_If_Stmt (S_Blk); + when others => + Error_Kind ("Translate_Psl_Directive_Statement(1)", Stmt); + end case; + -- Initialize the new state vector. Start_Declare_Stmt; New_Var_Decl (Var_I, Wki_I, O_Storage_Local, Ghdl_Index_Type); @@ -22111,8 +22142,18 @@ package body Translation is (New_Indexed_Element (New_Obj (Var_Nvec), New_Lit (New_Index_Lit (Unsigned_64 (S_Num)))))); - Chap8.Translate_Report - (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error); + case Get_Kind (Stmt) is + when Iir_Kind_Psl_Assert_Statement => + Chap8.Translate_Report + (Stmt, Ghdl_Psl_Assert_Failed, Severity_Level_Error); + when Iir_Kind_Psl_Cover_Statement => + Chap8.Translate_Report + (Stmt, Ghdl_Psl_Cover, Severity_Level_Note); + New_Assign_Stmt (Get_Var (Info.Psl_Bool_Var), + New_Lit (Ghdl_Bool_True_Node)); + when others => + Error_Kind ("Translate_Psl_Directive_Statement", Stmt); + end case; Finish_If_Stmt (S_Blk); -- Assign state vector. @@ -22145,54 +22186,76 @@ package body Translation is Finish_Subprogram_Body; -- The finalizer. - if Psl_Need_Finalizer (NFA) then - Start_Procedure_Decl (Inter_List, Create_Identifier ("FINALPROC"), - O_Storage_Private); - New_Interface_Decl (Inter_List, Instance, Wki_Instance, - Base.Block_Decls_Ptr_Type); - Finish_Subprogram_Decl (Inter_List, Info.Psl_Proc_Final_Subprg); - - Start_Subprogram_Body (Info.Psl_Proc_Final_Subprg); - Push_Local_Factory; - -- Push scope for architecture declarations. - Push_Scope (Base.Block_Decls_Type, Instance); + case Get_Kind (Stmt) is + when Iir_Kind_Psl_Assert_Statement => + if Psl_Need_Finalizer (NFA) then + Create_Psl_Final_Proc (Stmt, Base, Instance); + + Start_Subprogram_Body (Info.Psl_Proc_Final_Subprg); + Push_Local_Factory; + -- Push scope for architecture declarations. + Push_Scope (Base.Block_Decls_Type, Instance); + + S := Get_Final_State (NFA); + E := Get_First_Dest_Edge (S); + while E /= No_Edge loop + Sd := Get_Edge_Src (E); + + if PSL.NFAs.Utils.Has_EOS (Get_Edge_Expr (E)) then + + S_Num := Get_State_Label (Sd); + Open_Temp; + + Cond := New_Value + (New_Indexed_Element + (Get_Var (Info.Psl_Vect_Var), + New_Lit (New_Index_Lit (Unsigned_64 (S_Num))))); + Cond := New_Dyadic_Op + (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); + New_Return_Stmt; + Finish_If_Stmt (E_Blk); + + Close_Temp; + end if; - S := Get_Final_State (NFA); - E := Get_First_Dest_Edge (S); - while E /= No_Edge loop - Sd := Get_Edge_Src (E); + E := Get_Next_Dest_Edge (E); + end loop; - if PSL.NFAs.Utils.Has_EOS (Get_Edge_Expr (E)) then + Pop_Scope (Base.Block_Decls_Type); + Pop_Local_Factory; + Finish_Subprogram_Body; + else + Info.Psl_Proc_Final_Subprg := O_Dnode_Null; + end if; - S_Num := Get_State_Label (Sd); - Open_Temp; + when Iir_Kind_Psl_Cover_Statement => + Create_Psl_Final_Proc (Stmt, Base, Instance); - Cond := New_Value - (New_Indexed_Element - (Get_Var (Info.Psl_Vect_Var), - New_Lit (New_Index_Lit (Unsigned_64 (S_Num))))); - Cond := New_Dyadic_Op - (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); - New_Return_Stmt; - Finish_If_Stmt (E_Blk); + Start_Subprogram_Body (Info.Psl_Proc_Final_Subprg); + Push_Local_Factory; + -- Push scope for architecture declarations. + Push_Scope (Base.Block_Decls_Type, Instance); - Close_Temp; - end if; + Start_If_Stmt + (S_Blk, + New_Monadic_Op (ON_Not, + New_Value (Get_Var (Info.Psl_Bool_Var)))); + Chap8.Translate_Report + (Stmt, Ghdl_Psl_Cover_Failed, Severity_Level_Error); + Finish_If_Stmt (S_Blk); - E := Get_Next_Dest_Edge (E); - end loop; + Pop_Scope (Base.Block_Decls_Type); + Pop_Local_Factory; + Finish_Subprogram_Body; - Pop_Scope (Base.Block_Decls_Type); - Pop_Local_Factory; - Finish_Subprogram_Body; - else - Info.Psl_Proc_Final_Subprg := O_Dnode_Null; - end if; - end Translate_Psl_Assert_Statement; + when others => + Error_Kind ("Translate_Psl_Directive_Statement(3)", Stmt); + end case; + end Translate_Psl_Directive_Statement; -- Create the instance for block BLOCK. -- BLOCK can be either an entity, an architecture or a block statement. @@ -22212,8 +22275,9 @@ package body Translation is null; when Iir_Kind_Psl_Declaration => null; - when Iir_Kind_Psl_Assert_Statement => - Translate_Psl_Assert_Declarations (El); + when Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => + Translate_Psl_Directive_Declarations (El); when Iir_Kind_Component_Instantiation_Statement => Translate_Component_Instantiation_Statement (El); when Iir_Kind_Block_Statement => @@ -22445,7 +22509,8 @@ package body Translation is null; when Iir_Kind_Psl_Declaration => null; - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => declare Info : Psl_Info_Acc; begin @@ -22453,7 +22518,7 @@ package body Translation is Push_Scope (Info.Psl_Decls_Type, Info.Psl_Parent_Field, Block_Info.Block_Decls_Type); - Translate_Psl_Assert_Statement (Stmt, Base_Info); + Translate_Psl_Directive_Statement (Stmt, Base_Info); Pop_Scope (Info.Psl_Decls_Type); end; when Iir_Kind_Component_Instantiation_Statement => @@ -22781,9 +22846,9 @@ package body Translation is -- PROC: the process to be elaborated -- BLOCK_INFO: info for the block containing the process -- BASE_INFO: info for the global block - procedure Elab_Psl_Assert (Stmt : Iir; - Block_Info : Block_Info_Acc; - Base_Info : Block_Info_Acc) + procedure Elab_Psl_Directive (Stmt : Iir; + Block_Info : Block_Info_Acc; + Base_Info : Block_Info_Acc) is Constr : O_Assoc_List; Info : Psl_Info_Acc; @@ -22858,8 +22923,13 @@ package body Translation is Finish_Loop_Stmt (Label); Finish_Declare_Stmt; + if Info.Psl_Bool_Var /= null then + New_Assign_Stmt (Get_Var (Info.Psl_Bool_Var), + New_Lit (Ghdl_Bool_False_Node)); + end if; + Pop_Scope (Info.Psl_Decls_Type); - end Elab_Psl_Assert; + end Elab_Psl_Directive; procedure Elab_Implicit_Guard_Signal (Block : Iir_Block_Statement; Block_Info : Block_Info_Acc) @@ -23543,8 +23613,9 @@ package body Translation is null; when Iir_Kind_Psl_Declaration => null; - when Iir_Kind_Psl_Assert_Statement => - Elab_Psl_Assert (Stmt, Block_Info, Base_Info); + when Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => + Elab_Psl_Directive (Stmt, Block_Info, Base_Info); when Iir_Kind_Component_Instantiation_Statement => declare Info : Block_Info_Acc; @@ -27317,6 +27388,32 @@ package body Translation is Add_Rti_Node (Info.Block_Rti_Const); end Generate_Instance; + procedure Generate_Psl_Directive (Stmt : Iir) + is + Name : O_Dnode; + List : O_Record_Aggr_List; + + Rti : O_Dnode; + Res : O_Cnode; + Info : constant Psl_Info_Acc := Get_Info (Stmt); + Mark : Id_Mark_Type; + begin + Push_Identifier_Prefix (Mark, Get_Identifier (Stmt)); + Name := Generate_Name (Stmt); + + New_Const_Decl (Rti, Create_Identifier ("RTI"), + O_Storage_Public, Ghdl_Rtin_Type_Scalar); + + Start_Const_Value (Rti); + Start_Record_Aggr (List, Ghdl_Rtin_Type_Scalar); + New_Record_Aggr_El (List, Generate_Common (Ghdl_Rtik_Psl_Assert)); + New_Record_Aggr_El (List, New_Global_Address (Name, Char_Ptr_Type)); + Finish_Record_Aggr (List, Res); + Finish_Const_Value (Rti, Res); + Info.Psl_Rti_Const := Rti; + Pop_Identifier_Prefix (Mark); + end Generate_Psl_Directive; + procedure Generate_Declaration_Chain (Chain : Iir) is Decl : Iir; @@ -27427,32 +27524,9 @@ package body Translation is when Iir_Kind_Psl_Declaration => null; when Iir_Kind_Psl_Assert_Statement => - declare - Name : O_Dnode; - List : O_Record_Aggr_List; - - Rti : O_Dnode; - Res : O_Cnode; - Info : Psl_Info_Acc; - begin - Info := Get_Info (Stmt); - Push_Identifier_Prefix (Mark, Get_Identifier (Stmt)); - Name := Generate_Name (Stmt); - - New_Const_Decl (Rti, Create_Identifier ("RTI"), - O_Storage_Public, Ghdl_Rtin_Type_Scalar); - - Start_Const_Value (Rti); - Start_Record_Aggr (List, Ghdl_Rtin_Type_Scalar); - New_Record_Aggr_El - (List, Generate_Common (Ghdl_Rtik_Psl_Assert)); - New_Record_Aggr_El - (List, New_Global_Address (Name, Char_Ptr_Type)); - Finish_Record_Aggr (List, Res); - Finish_Const_Value (Rti, Res); - Info.Psl_Rti_Const := Rti; - Pop_Identifier_Prefix (Mark); - end; + Generate_Psl_Directive (Stmt); + when Iir_Kind_Psl_Cover_Statement => + Generate_Psl_Directive (Stmt); when others => Error_Kind ("rti.generate_concurrent_statement_chain", Stmt); end case; @@ -27832,7 +27906,8 @@ package body Translation is when Iir_Kind_Process_Statement | Iir_Kind_Sensitized_Process_Statement => Rti_Const := Node_Info.Process_Rti_Const; - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => Rti_Const := Node_Info.Psl_Rti_Const; when others => Error_Kind ("get_context_rti", Node); @@ -27862,7 +27937,8 @@ package body Translation is when Iir_Kind_Process_Statement | Iir_Kind_Sensitized_Process_Statement => Block_Type := Node_Info.Process_Decls_Type; - when Iir_Kind_Psl_Assert_Statement => + when Iir_Kind_Psl_Assert_Statement + | Iir_Kind_Psl_Cover_Statement => Block_Type := Node_Info.Psl_Decls_Type; when others => Error_Kind ("get_context_addr", Node); @@ -28634,6 +28710,9 @@ package body Translation is Create_Report_Subprg ("__ghdl_assert_failed", Ghdl_Assert_Failed); Create_Report_Subprg ("__ghdl_psl_assert_failed", Ghdl_Psl_Assert_Failed); + Create_Report_Subprg ("__ghdl_psl_cover", Ghdl_Psl_Cover); + Create_Report_Subprg ("__ghdl_psl_cover_failed", + Ghdl_Psl_Cover_Failed); Create_Report_Subprg ("__ghdl_report", Ghdl_Report); end; |