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/simulate/simul-elaboration.adb | 3 ++- src/vhdl/simulate/simul-simulation-main.adb | 11 +++++++++-- 2 files changed, 11 insertions(+), 3 deletions(-) (limited to 'src/vhdl/simulate') 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), -- cgit v1.2.3