From 0331772c3ef05bad40b748542939ccafab2a9c68 Mon Sep 17 00:00:00 2001 From: Pepijn de Vos Date: Wed, 7 Aug 2019 04:20:14 +0200 Subject: Add support for PSL assumptions, used in formal verification (#880) * vhdl: make the parser understand PSL assume * assume does not actually have report according to the spec. Just a property. * add SPL assume to semantic analysis * canonicalise PSL assume * add assume to annotations * add PSL assume to simulation code * statement -> directive * add assume to translation files * update ticked24 testcase * correctly parse assume * add assume testcase * refactor chunk of duplicated code --- src/vhdl/translate/trans-chap9.adb | 29 +++++++++++++++++++++-------- src/vhdl/translate/trans-rtis.adb | 16 ++++++++++++---- src/vhdl/translate/trans-rtis.ads | 1 + src/vhdl/translate/trans_decls.ads | 1 + src/vhdl/translate/translation.adb | 2 ++ 5 files changed, 37 insertions(+), 12 deletions(-) (limited to 'src/vhdl/translate') 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 @@ -321,6 +321,9 @@ package body Trans.Rtis is New_Enum_Literal (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); @@ -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); -- cgit v1.2.3