New Wishbone checks; Fix illegal PSL property

* A lot of new checks are added to WishboneCheckerE unit
  trying to implement the rules of the Wishbone spec.
* An illegal use of the suffix implication instead of logical
  implicationis fixed in WishboneMasterE unit

syn/WishBoneCheckerE.vhd

@@ -18,7 +18,8 @@ entity WishBoneCheckerE is
     --+ wishbone inputs
     WbSDat_i      : in std_logic_vector;
     WbSAck_i      : in std_logic;
-    WbSErr_i      : in std_logic
+    WbSErr_i      : in std_logic;
+    WbRty_i       : in std_logic
   );
 end entity WishBoneCheckerE;
 
@@ -33,10 +34,10 @@ begin
   --
   -- Wishbone protocol checks
   --
-  -- psl property initialize(boolean init_state) is
+  -- psl property initialize_interface (boolean init_state) is
   --   always ({WbRst_i} |=> {init_state[+] && {WbRst_i[*]; not(WbRst_i)}});
   --
-  -- psl RULE_3_00 : assert initialize(not(WbMCyc_i) and not(WbMStb_i) and not(WbMWe_i))
+  -- psl RULE_3_00 : assert initialize_interface (not(WbMCyc_i) and not(WbMStb_i) and not(WbMWe_i))
   --   report "Wishbone rule 3.00 violated";
   --
   -- psl property reset_signal is
@@ -45,11 +46,48 @@ begin
   -- psl RULE_3_05 : assert reset_signal
   --   report "Wishbone rule 3.05 violated";
   --
---  -- psl property master_cycle_signal(boolean master_strobe, master_cyc) is
---  --   always {master_strobe} |-> {master_cyc[+] && {not(master_strobe)[->]:WbClk_i}};
---  --
---  -- psl RULE_3_25 : assert master_cycle_signal(WbMStb_i, WbMCyc_i)
---  --   report "Wishbone rule 3.25 violated";
+  -- psl property CYC_O_signal is
+  --   always {not(WbMStb_i); WbMStb_i} |-> {(WbMCyc_i and WbMStb_i)[+]; not(WbMStb_i)};
+  --
+  -- psl RULE_3_25 : assert CYC_O_signal
+  --   report "Wishbone rule 3.25 violated";
+  --
+  -- psl property slave_no_response is
+  --   always not(WbMCyc_i) -> not(WbSAck_i) and not(WbSErr_i);
+  --
+  -- psl property slave_response_to_master is
+  --  always {not(WbMStb_i); WbMStb_i} |->
+  --         {{(WbMStb_i and not(WbSAck_i))[*];
+  --           WbMStb_i and WbSAck_i;
+  --           not(WbMStb_i)} |
+  --          {(WbMStb_i and not(WbSErr_i))[*];
+  --           WbMStb_i and WbSErr_i;
+  --           not(WbMStb_i)} |
+  --          {(WbMStb_i and not(WbRty_i))[*];
+  --           WbMStb_i and WbRty_i;
+  --           not(WbMStb_i)}
+  -- };
+  --
+  -- psl RULE_3_30_0 : assert slave_no_response
+  --   report "Wishbone rule 3.30_0 violated";
+  --
+  -- psl RULE_3_30_1 : assert slave_response_to_master
+  --   report "Wishbone rule 3.30_0 violated";
+  --
+  -- psl property slave_response is 
+  --   always {not(WbMStb_i); WbMCyc_i and WbMStb_i} |->
+  --     {not(WbSAck_i or WbSErr_i or WbRty_i)[*]; WbSAck_i or WbSErr_i or WbRty_i};
+  --
+  -- psl RULE_3_35 : assert slave_response
+  --   report "Wishbone rule 3.35 violated";
+  --
+  -- psl property response_signals is
+  --   never ((WbSErr_i and WbRty_i) or (WbSErr_i and WbSAck_i) or (WbSAck_i and WbRty_i));
+  --
+  -- psl RULE_3_45 : assert response_signals
+  --   report "Wishbone rule 3.45 violated";
+  --
+  -- -- psl property slave_negated_response is
 
 
 end architecture check;

syn/WishBoneMasterE.vhd

@@ -129,7 +129,7 @@ begin
   --   report "WB master: Write error";
   --
   -- psl WB_READ : assert always
-  --   ((not(WbCyc_o) and not(WbStb_o) and LocalRen_i and not(LocalWen_i)) |->
+  --   ((not(WbCyc_o) and not(WbStb_o) and LocalRen_i and not(LocalWen_i)) ->
   --    next (WbCyc_o = '1' and WbStb_o = '1' and WbWe_o = '0')) abort WbRst_i
   --   report "WB master: Read error";
 

syn/WishBoneP.vhd

@@ -73,7 +73,8 @@ package WishBoneP is
       --+ wishbone inputs
       WbSDat_i      : in std_logic_vector;
       WbSAck_i      : in std_logic;
-      WbSErr_i      : in std_logic
+      WbSErr_i      : in std_logic;
+      WbRty_i       : in std_logic
     );
   end component WishBoneCheckerE;
 

test/Makefile

@@ -68,7 +68,7 @@ spi: spit
 	ghdl -r --std=$(VHD_STD) $@t --wave=$@t.ghw
 
 
-wishbonet: OsvvmContext.o AssertP.o SimP.o QueueP.o DictP.o UtilsP.o \
+wishbonet: OsvvmContext.o AssertP.o SimP.o QueueP.o DictP.o UtilsP.o $(SYN_SRC)/WishBoneCheckerE.vhd \
 	  $(SYN_SRC)/WishBoneP.vhd $(SYN_SRC)/WishBoneMasterE.vhd $(SYN_SRC)/WishBoneSlaveE.vhd WishBoneT.vhd
 	ghdl -a --std=$(VHD_STD) -fpsl $(SYN_SRC)/WishBoneP.vhd
 	ghdl -a --std=$(VHD_STD) -fpsl $(SYN_SRC)/WishBoneCheckerE.vhd $(SYN_SRC)/WishBoneMasterE.vhd $(SYN_SRC)/WishBoneSlaveE.vhd

test/WishBoneT.vhd

@@ -236,7 +236,6 @@ begin
 
 
   WbSlaveLocalP : process is
-    variable v_data : std_logic_vector(s_slave_local_din'range);
   begin
     wait until rising_edge(s_wb_clk);
     if (s_wb_reset = '1') then
@@ -248,8 +247,7 @@ begin
         WB_SLAVE_REG : assert sv_wb_slave_dict.hasKey(slv_to_uint(s_slave_local_adress))
           report "ERROR: Requested register at addr 0x" & to_hstring(s_slave_local_adress) & " not written before"
           severity failure;
-        sv_wb_slave_dict.get(slv_to_uint(s_slave_local_adress), v_data);
-        s_slave_local_din <= v_data;
+        s_slave_local_din <= sv_wb_slave_dict.get(slv_to_uint(s_slave_local_adress));
       end if;
     end if;
   end process WbSlaveLocalP;
@@ -269,7 +267,8 @@ i_WishBoneChecker : WishBoneCheckerE
     --+ wishbone inputs
     WbSDat_i      => s_wishbone.RDat,
     WbSAck_i      => s_wishbone.Ack,
-    WbSErr_i      => s_wishbone.Err
+    WbSErr_i      => s_wishbone.Err,
+    WbRty_i       => '0'
   );