Browse Source

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.
pull/1/head
T. Meissner 9 years ago
parent
commit
c1005badfc
1 changed files with 14 additions and 1 deletions
  1. +14
    -1
      syn/WishBoneMasterE.vhd

+ 14
- 1
syn/WishBoneMasterE.vhd View File

@ -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;

Loading…
Cancel
Save