From dd3b18ef41b18ded69cf06087de489a3e840580a Mon Sep 17 00:00:00 2001 From: tmeissner Date: Wed, 25 Mar 2020 18:38:00 +0100 Subject: [PATCH] Add formal verification of Wishbone components --- formal/Makefile | 17 +++++ formal/WishBoneMasterE.sby | 20 +++++ formal/WishBoneSlaveE.sby | 19 +++++ syn/WishBoneMasterE.vhd | 114 ++++++++++++++++++++-------- syn/WishBoneSlaveE.vhd | 151 ++++++++++++++++++++++++++----------- 5 files changed, 244 insertions(+), 77 deletions(-) create mode 100644 formal/Makefile create mode 100644 formal/WishBoneMasterE.sby create mode 100644 formal/WishBoneSlaveE.sby diff --git a/formal/Makefile b/formal/Makefile new file mode 100644 index 0000000..8357b4d --- /dev/null +++ b/formal/Makefile @@ -0,0 +1,17 @@ +.PHONY: all-cover all-prove all +all: all-cover all-prove +all-cover: WishBoneMasterE-cover WishBoneSlaveE-cover +all-prove: WishBoneMasterE-prove WishBoneSlaveE-prove + + +%-cover: ../syn/%.vhd %.sby + mkdir -p work + sby --yosys "yosys -m ghdl" -f -d work/$@ $(subst -cover,,$@).sby cover + +%-prove: ../syn/%.vhd %.sby + mkdir -p work + sby --yosys "yosys -m ghdl" -f -d work/$@ $(subst -prove,,$@).sby prove + + +clean: + rm -rf work diff --git a/formal/WishBoneMasterE.sby b/formal/WishBoneMasterE.sby new file mode 100644 index 0000000..7a85361 --- /dev/null +++ b/formal/WishBoneMasterE.sby @@ -0,0 +1,20 @@ +[tasks] +prove +cover + +[options] +depth 20 +prove: mode prove +cover: mode cover + +[engines] +prove: abc pdr +cover: smtbmc z3 + +[script] +prove: ghdl --std=08 -gCoverage=false -gFormal=true -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere +cover: ghdl --std=08 -gCoverage=true -gFormal=true -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere +prep -auto-top + +[files] +../syn/WishBoneMasterE.vhd diff --git a/formal/WishBoneSlaveE.sby b/formal/WishBoneSlaveE.sby new file mode 100644 index 0000000..19ac428 --- /dev/null +++ b/formal/WishBoneSlaveE.sby @@ -0,0 +1,19 @@ +[tasks] +prove +cover + +[options] +depth 25 +prove: mode prove +cover: mode cover + +[engines] +prove: abc pdr +cover: smtbmc z3 + +[script] +ghdl --std=08 -gFormal=true -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee +prep -auto-top + +[files] +../syn/WishBoneSlaveE.vhd diff --git a/syn/WishBoneMasterE.vhd b/syn/WishBoneMasterE.vhd index 1f095c8..133ae3f 100644 --- a/syn/WishBoneMasterE.vhd +++ b/syn/WishBoneMasterE.vhd @@ -3,9 +3,11 @@ library ieee; use ieee.numeric_std.all; + entity WishBoneMasterE is generic ( - Coverage : boolean := false; + Coverage : boolean := true; + Formal : boolean := true; AddressWidth : natural := 8; DataWidth : natural := 8 ); @@ -97,8 +99,8 @@ begin --+ registered wishbone if outputs OutRegsP : process (WbClk_i) is begin - if(rising_edge(WbClk_i)) then - if(WbRst_i = '1') then + if (rising_edge(WbClk_i)) then + if (WbRst_i = '1') then WbAdr_o <= (others => '0'); WbDat_o <= (others => '0'); s_wb_wen <= '0'; @@ -117,41 +119,89 @@ begin end process OutRegsP; - -- psl default clock is rising_edge(WbClk_i); + FormalG : if Formal generate + + -- Glue logic + signal s_local_data : std_logic_vector(DataWidth-1 downto 0); + signal s_local_address : std_logic_vector(AddressWidth-1 downto 0); + + begin + + process is + begin + wait until rising_edge(WbClk_i); + if (s_wb_master_fsm = IDLE) then + if (LocalWen_i = '1') then + s_local_data <= LocalData_i; + s_local_address <= LocalAdress_i; + end if; + if (LocalRen_i = '1') then + s_local_address <= LocalAdress_i; + end if; + end if; + end process; + + + default clock is rising_edge(WbClk_i); + + restrict {WbRst_i = '1'; WbRst_i = '0'[+]}[*1]; - -- PSL assert directives + RESET : assert always + WbRst_i -> next + WbCyc_o = '0' and WbStb_o = '0' and WbWe_o = '0' and + to_integer(unsigned(WbAdr_o)) = 0 and to_integer(unsigned(WbDat_o)) = 0 and + LocalAck_o = '0' and LocalError_o = '0' and to_integer(unsigned(LocalData_o)) = 0 + report "WB master: Reset error"; - -- psl RESET : assert always - -- WbRst_i -> - -- WbCyc_o = '0' and WbStb_o = '0' and WbWe_o = '0' and - -- to_integer(unsigned(WbAdr_o)) = 0 and to_integer(unsigned(WbDat_o)) = 0 and - -- LocalAck_o = '0' and LocalError_o = '0' and to_integer(unsigned(LocalData_o)) = 0 - -- report "WB master: Reset error"; - -- - -- psl WB_WRITE : assert always - -- ((not(WbCyc_o) and not(WbStb_o) and LocalWen_i and not (LocalRen_i)) -> - -- next (WbCyc_o = '1' and WbStb_o = '1' and WbWe_o = '1')) abort WbRst_i - -- report "WB master: Write error"; - -- - -- psl WB_READ : assert always - -- ((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"; + WB_WRITE : assert always + ((not WbCyc_o and not WbStb_o and LocalWen_i and not LocalRen_i) -> + next (WbCyc_o and WbStb_o and WbWe_o)) abort WbRst_i + report "WB master: Write error"; + + WB_READ : assert always + ((not WbCyc_o and not WbStb_o and LocalRen_i and not LocalWen_i) -> + next (WbCyc_o and WbStb_o and not WbWe_o)) abort WbRst_i + report "WB master: Read error"; + + assert never LocalError_o and LocalAck_o; + + assert always WbStb_o = WbCyc_o; + + assert always + not WbRst_i and WbCyc_o and not WbAck_i and not WbErr_i -> + next (WbCyc_o until (WbAck_i or WbErr_i)) abort WbRst_i; + + assert always WbCyc_o and WbAck_i -> next not WbCyc_o; + assert always WbWe_o and WbAck_i -> next not WbWe_o; + assert always WbWe_o -> WbCyc_o; + + assert always WbWe_o -> WbDat_o = s_local_data abort WbRst_i; + assert always WbWe_o -> WbAdr_o = s_local_address abort WbRst_i; + + assert always WbCyc_o and not WbWe_o -> WbAdr_o = s_local_address abort WbRst_i; + + end generate FormalG; CoverageG : if Coverage generate - -- psl COVER_LOCAL_WRITE : cover {s_wb_master_fsm = IDLE and LocalWen_i = '1' and - -- LocalRen_i = '0' and WbRst_i = '0'} - -- report "WB master: Local write"; - -- - -- psl COVER_LOCAL_READ : cover {s_wb_master_fsm = IDLE and LocalRen_i = '1' and - -- LocalWen_i = '0' and WbRst_i = '0'} - -- report "WB master: Local read"; - -- - -- psl COVER_LOCAL_WRITE_READ : cover {s_wb_master_fsm = IDLE and LocalWen_i = '1' and - -- LocalRen_i = '1' and WbRst_i = '0'} - -- report "WB master: Local write & read"; + default clock is rising_edge(WbClk_i); + + restrict {WbRst_i = '1'; WbRst_i = '0'[+]}[*1]; + + COVER_LOCAL_WRITE : cover {s_wb_master_fsm = IDLE and LocalWen_i = '1' and + LocalRen_i = '0' and WbRst_i = '0'} + report "WB master: Local write"; + + COVER_LOCAL_READ : cover {s_wb_master_fsm = IDLE and LocalRen_i = '1' and + LocalWen_i = '0' and WbRst_i = '0'} + report "WB master: Local read"; + + COVER_LOCAL_WRITE_READ : cover {s_wb_master_fsm = IDLE and LocalWen_i = '1' and + LocalRen_i = '1' and WbRst_i = '0'} + report "WB master: Local write & read"; + + test_cover : cover {s_wb_master_fsm = IDLE and LocalWen_i = '1'; s_wb_master_fsm = ADDRESS; s_wb_master_fsm = DATA}; end generate CoverageG; diff --git a/syn/WishBoneSlaveE.vhd b/syn/WishBoneSlaveE.vhd index ed723eb..d5ae522 100644 --- a/syn/WishBoneSlaveE.vhd +++ b/syn/WishBoneSlaveE.vhd @@ -6,8 +6,9 @@ library ieee; entity WishBoneSlaveE is generic ( - AddressWidth : natural := 8; - DataWidth : natural := 8 + Formal : boolean := false; + AddressWidth : natural := 32; + DataWidth : natural := 32 ); port ( --+ wishbone system if @@ -84,49 +85,109 @@ begin --+ wishbone if outputs WbDat_o <= LocalData_i when s_wb_slave_fsm = DATA and WbWe_i = '0' else (others => '0'); - WbAck_o <= '1' when s_wb_slave_fsm = DATA or (s_wb_slave_fsm = ADDRESS and s_wb_active and WbWe_i = '1') else '0'; - WbErr_o <= '0'; - - - -- 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)) and - -- (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)) and - -- (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"; + WbAck_o <= '1' when (s_wb_slave_fsm = DATA and WbWe_i = '0') or (s_wb_slave_fsm = ADDRESS and s_wb_active and WbWe_i = '1') else '0'; + WbErr_o <= '1' when s_wb_slave_fsm = DATA and WbWe_i = '1' else '0'; + + + FormalG : if Formal generate + + -- Glue logic + signal s_wb_data : std_logic_vector(DataWidth-1 downto 0); + signal s_wb_address : std_logic_vector(AddressWidth-1 downto 0); + + begin + + SyncWbSignals : process is + begin + wait until rising_edge(WbClk_i); + if (s_wb_slave_fsm = ADDRESS and WbCyc_i = '1' and WbStb_i = '1') then + if (WbWe_i = '1') then + s_wb_data <= WbDat_i; + end if; + s_wb_address <= WbAdr_i; + end if; + end process SyncWbSignals; + + + default clock is rising_edge(WbClk_i); + + restrict {WbRst_i = '1'; WbRst_i = '0'[+]}[*1]; + + assume always WbCyc_i = WbStb_i; + assume always WbWe_i -> WbStb_i; + assume always WbWe_i and WbAck_o -> next not WbWe_i; + + -- FSM state checks + FSM_IDLE_TO_ADDRESS : assert always + not WbRst_i and s_wb_slave_fsm = IDLE -> + next s_wb_slave_fsm = ADDRESS abort WbRst_i; + + FSM_ADDRESS_TO_DATA : assert always + not WbRst_i and s_wb_slave_fsm = ADDRESS and WbStb_i and WbCyc_i and not WbWe_i -> + next s_wb_slave_fsm = DATA abort WbRst_i; + + FSM_ADDRESS_TO_ADDRESS : assert always + not WbRst_i and s_wb_slave_fsm = ADDRESS and not (WbStb_i and WbCyc_i and not WbWe_i) -> + next s_wb_slave_fsm = ADDRESS abort WbRst_i; + + FSM_DATA_TO_ADDRESS : assert always + not WbRst_i and s_wb_slave_fsm = DATA -> + next s_wb_slave_fsm = ADDRESS abort WbRst_i; + + -- Wishbone write cycle checks + WB_WRITE_CYCLE_0 : assert always + s_wb_slave_fsm = ADDRESS and WbStb_i and WbCyc_i and WbWe_i -> + LocalWen_o and WbAck_o; + + WB_WRITE_CYCLE_1 : assert always + LocalWen_o -> LocalAdress_o = WbAdr_i; + + WB_WRITE_CYCLE_2 : assert always + LocalWen_o -> LocalData_o = WbDat_i; + + -- Wishbone read cycle checks + WB_READ_CYCLE_0 : assert always + s_wb_slave_fsm = ADDRESS and WbStb_i and WbCyc_i and not WbWe_i -> + LocalRen_o and not WbAck_o; + + WB_READ_CYCLE_1 : assert always + LocalRen_o -> LocalAdress_o = WbAdr_i; + + WB_READ_CYCLE_2 : assert always + s_wb_slave_fsm = DATA and not WbWe_i -> + WbAck_o and WbDat_o = LocalData_i; + + WB_READ_ERROR : assert always + s_wb_slave_fsm = DATA and WbWe_i -> + WbErr_o; + + WB_NEVER_ACK_AND_ERR : assert never + WbAck_o and WbErr_o; + + WB_ERR : assert always + WbErr_o -> + (WbCyc_i and WbStb_i) + report "PSL ERROR: WbErr invalid"; + + LOCAL_WE : assert always + LocalWen_o -> + (WbCyc_i and WbStb_i and WbWe_i and not LocalRen_o) and + (next not LocalWen_o) + report "PSL ERROR: LocalWen invalid"; + + LOCAL_RE : assert always + LocalRen_o -> + (WbCyc_i and WbStb_i and not WbWe_i and not LocalWen_o) and + (next not LocalRen_o) + report "PSL ERROR: LocalRen invalid"; + + RESET : assert always + WbRst_i -> next + (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 generate FormalG; end architecture rtl;