From dd494f090179adbbd377700e732233aff4c6525a Mon Sep 17 00:00:00 2001 From: tmeissner Date: Sat, 27 Oct 2018 17:39:48 +0200 Subject: [PATCH] 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 | 54 ++++++++++++++++++++++++++++++++++------ syn/WishBoneMasterE.vhd | 2 +- syn/WishBoneP.vhd | 3 ++- test/Makefile | 2 +- test/WishBoneT.vhd | 7 +++--- 5 files changed, 53 insertions(+), 15 deletions(-) diff --git a/syn/WishBoneCheckerE.vhd b/syn/WishBoneCheckerE.vhd index 866a9cc..042f2cf 100644 --- a/syn/WishBoneCheckerE.vhd +++ b/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; \ No newline at end of file diff --git a/syn/WishBoneMasterE.vhd b/syn/WishBoneMasterE.vhd index ec44c7d..a74157e 100644 --- a/syn/WishBoneMasterE.vhd +++ b/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"; diff --git a/syn/WishBoneP.vhd b/syn/WishBoneP.vhd index ee9faf4..8bf3fd8 100644 --- a/syn/WishBoneP.vhd +++ b/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; diff --git a/test/Makefile b/test/Makefile index 86e974b..65701ce 100644 --- a/test/Makefile +++ b/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 diff --git a/test/WishBoneT.vhd b/test/WishBoneT.vhd index 0443ba3..38147c4 100644 --- a/test/WishBoneT.vhd +++ b/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' );