From 6659dbbe31f4ea23d2a801ea9c3ff5f6abf10271 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Sat, 22 Aug 2015 12:23:31 +0200 Subject: [PATCH] Fix PSL assertions for local wen and local ren The second logical implication was made the whole property holding when the part after the 1st implication didn't hold. So, the 2nd implication is replaced by an and in combination with the next operator. Now the property fails when one of the two and'ed parts after the implication fails. --- syn/WishBoneSlaveE.vhd | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/syn/WishBoneSlaveE.vhd b/syn/WishBoneSlaveE.vhd index 31b49d1..37fd010 100644 --- a/syn/WishBoneSlaveE.vhd +++ b/syn/WishBoneSlaveE.vhd @@ -112,14 +112,14 @@ begin -- -- psl LOCAL_WE : assert always -- LocalWen_o -> - -- (WbCyc_i and WbStb_i and WbWe_i and not(LocalRen_o)) -> - -- next not(LocalWen_o) + -- (WbCyc_i and WbStb_i and WbWe_i and not(LocalRen_o)) and + -- (next not(LocalWen_o)) -- report "PSL ERROR: LocalWen invalid"; -- -- psl LOCAL_RE : assert always -- LocalRen_o -> - -- (WbCyc_i and WbStb_i and not(WbWe_i) and not(LocalWen_o)) -> - -- next not(LocalRen_o) + -- (WbCyc_i and WbStb_i and not(WbWe_i) and not(LocalWen_o)) and + -- (next not(LocalRen_o)) -- report "PSL ERROR: LocalRen invalid"; -- -- psl RESET : assert always