From c1005badfcf3c995389a8d71a434ed81bdd88df7 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Wed, 26 Aug 2015 21:09:50 +0200 Subject: [PATCH] Add PSL assertions to check initiating of WishBone write/read transfer WB_WRITE & WB_READ check that a write/read transfer is started on the WishBone bus if requested on the local port of the WishBoneMasterE unit at the adequate time. --- syn/WishBoneMasterE.vhd | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/syn/WishBoneMasterE.vhd b/syn/WishBoneMasterE.vhd index eeb971c..4ac64d1 100644 --- a/syn/WishBoneMasterE.vhd +++ b/syn/WishBoneMasterE.vhd @@ -1,6 +1,6 @@ library ieee; use ieee.std_logic_1164.all; - + use ieee.numeric_std.all; entity WishBoneMasterE is @@ -116,4 +116,17 @@ begin end process OutRegsP; + -- psl default clock is rising_edge(WbClk_i); + -- + -- psl WB_WRITE : assert always + -- ((not(WbCyc_o) and not(WbStb_o) and LocalWen_i) -> + -- next (WbCyc_o = '1' and WbStb_o = '1' and WbWe_o = '1')) abort WbRst_i + -- report "PSL ERROR: Wishbone write error"; + -- + -- psl WB_READ : assert always + -- ((not(WbCyc_o) and not(WbStb_o) and LocalRen_i) |-> + -- next (WbCyc_o = '1' and WbStb_o = '1' and WbWe_o = '0')) abort WbRst_i + -- report "PSL ERROR: Wishbone read error"; + + end architecture rtl;