Add PSL assertions to check WishBone & Local IF

Various new PSL assertions to check ports during Wishbone write & read
transfer and reset state

syn/WishBoneSlaveE.vhd

@@ -1,5 +1,6 @@
 library ieee;
   use ieee.std_logic_1164.all;
+  use ieee.numeric_std.all;
 
 
 
@@ -87,4 +88,45 @@ begin
   WbErr_o <= '0';
 
 
-end architecture rtl;
+  -- psl default clock is rising_edge(WbClk_i);
+  --
+  -- psl LOCAL_WRITE : assert always
+  --   ((WbCyc_i and WbStb_i and WbWe_i) ->
+  --    (LocalWen_o = '1' and WbAck_o = '1' and LocalAdress_o = WbAdr_i and LocalData_o = WbDat_i)) abort WbRst_i
+  --   report "PSL ERROR: Local write error";
+  --
+  -- psl LOCAL_READ : assert always
+  --   ({not(WbCyc_i) and not(WbStb_i); WbCyc_i and WbStb_i and not(WbWe_i)} |->
+  --    {LocalRen_o = '1' and LocalAdress_o = WbAdr_i and WbAck_o = '0'; LocalRen_o = '0' and WbDat_o = LocalData_i and WbAck_o = '1'}) abort WbRst_i
+  --   report "PSL ERROR: Local read error";
+  --
+  -- psl WB_ACK : assert always
+  --   WbAck_o ->
+  --   (WbCyc_i and WbStb_i)
+  --   report "PSL ERROR: WbAck invalid";
+  --
+  --  psl WB_ERR : assert always
+  --   WbErr_o ->
+  --   (WbCyc_i and WbStb_i)
+  --   report "PSL ERROR: WbErr invalid";
+  --
+  -- psl LOCAL_WE : assert always
+  --   LocalWen_o ->
+  --   (WbCyc_i and WbStb_i and WbWe_i and not(LocalRen_o)) ->
+  --   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)
+  --   report "PSL ERROR: LocalRen invalid";
+  --
+  -- psl RESET : assert always
+  --   WbRst_i ->
+  --   (to_integer(unsigned(WbDat_o)) = 0 and WbAck_o = '0' and WbErr_o = '0' and
+  --    LocalWen_o = '0' and LocalRen_o = '0' and to_integer(unsigned(LocalAdress_o)) = 0 and to_integer(unsigned(LocalData_o)) = 0)
+  --   report "PSL ERROR: Reset error";
+
+
+end architecture rtl;

test/Makefile

@@ -59,7 +59,7 @@ spi: spit
 
 wishbonet: RandomPkg.o AssertP.o SimP.o QueueP.o $(SYN_SRC)/WishBoneMasterE.vhd $(SYN_SRC)/WishBoneSlaveE.vhd WishBoneT.vhd
 	ghdl -a --std=$(VHD_STD) -fpsl $(SYN_SRC)/WishBoneMasterE.vhd $(SYN_SRC)/WishBoneSlaveE.vhd
-	ghdl -a --std=$(VHD_STD) WishBoneT.vhd
+	ghdl -a --std=$(VHD_STD) -fpsl WishBoneT.vhd
 	ghdl -e --std=$(VHD_STD) $@
 
 .PHONY: wishbone