From 83d3e057578c2838dbcba38528aeca70f3216982 Mon Sep 17 00:00:00 2001 From: tmeissner Date: Thu, 26 Mar 2020 14:24:29 +0100 Subject: [PATCH] Add bmc mode; integrate simulation PSL checks * Add BMC mode to formal tests * Adapt wishbone simulation testbench to new generics * Integrate simulation PSL checks in Wishbone components * Add generic for Simulation PSL checks to Wishbone components --- formal/Makefile | 9 +++++-- formal/WishBoneMasterE.sby | 10 +++++--- formal/WishBoneSlaveE.sby | 7 +++++- syn/WishBoneMasterE.vhd | 51 +++++++++++++++++++++++++++++++------- syn/WishBoneP.vhd | 13 ++++++++++ syn/WishBoneSlaveE.vhd | 49 +++++++++++++++++++++++++++++++++--- test/WishBoneT.vhd | 13 ++++++++++ 7 files changed, 134 insertions(+), 18 deletions(-) diff --git a/formal/Makefile b/formal/Makefile index 8357b4d..9c63064 100644 --- a/formal/Makefile +++ b/formal/Makefile @@ -1,6 +1,7 @@ -.PHONY: all-cover all-prove all -all: all-cover all-prove +.PHONY: all-cover all-bmc all-prove all +all: all-cover all-bmc all-prove all-cover: WishBoneMasterE-cover WishBoneSlaveE-cover +all-bmc: WishBoneMasterE-bmc WishBoneSlaveE-bmc all-prove: WishBoneMasterE-prove WishBoneSlaveE-prove @@ -8,6 +9,10 @@ all-prove: WishBoneMasterE-prove WishBoneSlaveE-prove mkdir -p work sby --yosys "yosys -m ghdl" -f -d work/$@ $(subst -cover,,$@).sby cover +%-bmc: ../syn/%.vhd %.sby + mkdir -p work + sby --yosys "yosys -m ghdl" -f -d work/$@ $(subst -bmc,,$@).sby bmc + %-prove: ../syn/%.vhd %.sby mkdir -p work sby --yosys "yosys -m ghdl" -f -d work/$@ $(subst -prove,,$@).sby prove diff --git a/formal/WishBoneMasterE.sby b/formal/WishBoneMasterE.sby index 7a85361..5d53ab0 100644 --- a/formal/WishBoneMasterE.sby +++ b/formal/WishBoneMasterE.sby @@ -1,19 +1,23 @@ [tasks] +bmc prove cover [options] -depth 20 +depth 25 +bmc: mode bmc prove: mode prove cover: mode cover [engines] +bmc: smtbmc z3 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 +bmc: ghdl --std=08 -gCoverage=false -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere +prove: ghdl --std=08 -gCoverage=false -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere +cover: ghdl --std=08 -gCoverage=true -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere prep -auto-top [files] diff --git a/formal/WishBoneSlaveE.sby b/formal/WishBoneSlaveE.sby index 19ac428..27b03bd 100644 --- a/formal/WishBoneSlaveE.sby +++ b/formal/WishBoneSlaveE.sby @@ -1,18 +1,23 @@ [tasks] +bmc prove cover [options] depth 25 +bmc: mode bmc prove: mode prove cover: mode cover [engines] +bmc: smtbmc z3 prove: abc pdr cover: smtbmc z3 [script] -ghdl --std=08 -gFormal=true -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee +bmc: ghdl --std=08 -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee +prove: ghdl --std=08 -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee +cover: ghdl --std=08 -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee prep -auto-top [files] diff --git a/syn/WishBoneMasterE.vhd b/syn/WishBoneMasterE.vhd index 133ae3f..ad3932f 100644 --- a/syn/WishBoneMasterE.vhd +++ b/syn/WishBoneMasterE.vhd @@ -6,8 +6,9 @@ library ieee; entity WishBoneMasterE is generic ( - Coverage : boolean := true; - Formal : boolean := true; + Coverage : boolean := false; + Formal : boolean := false; + Simulation : boolean := false; AddressWidth : natural := 8; DataWidth : natural := 8 ); @@ -119,6 +120,8 @@ begin end process OutRegsP; + default clock is rising_edge(WbClk_i); + FormalG : if Formal generate -- Glue logic @@ -141,9 +144,6 @@ begin end if; end process; - - default clock is rising_edge(WbClk_i); - restrict {WbRst_i = '1'; WbRst_i = '0'[+]}[*1]; RESET : assert always @@ -185,8 +185,6 @@ begin CoverageG : if Coverage generate - 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 @@ -201,9 +199,44 @@ begin 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; + SimulationG : if Simulation generate + + -- assert directives + 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"; + + 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"; + + 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"; + + + -- cover directives + 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"; + + end generate SimulationG; + + end architecture rtl; diff --git a/syn/WishBoneP.vhd b/syn/WishBoneP.vhd index 8bf3fd8..1289d82 100644 --- a/syn/WishBoneP.vhd +++ b/syn/WishBoneP.vhd @@ -8,6 +8,13 @@ package WishBoneP is component WishBoneMasterE is + generic ( + Coverage : boolean := false; + Formal : boolean := false; + Simulation : boolean := false; + AddressWidth : natural := 8; + DataWidth : natural := 8 + ); port ( --+ wishbone system if WbRst_i : in std_logic; @@ -35,6 +42,12 @@ package WishBoneP is component WishBoneSlaveE is + generic ( + Formal : boolean := false; + Simulation : boolean := false; + AddressWidth : natural := 32; + DataWidth : natural := 32 + ); port ( --+ wishbone system if WbRst_i : in std_logic; diff --git a/syn/WishBoneSlaveE.vhd b/syn/WishBoneSlaveE.vhd index d5ae522..0c63ac7 100644 --- a/syn/WishBoneSlaveE.vhd +++ b/syn/WishBoneSlaveE.vhd @@ -7,6 +7,7 @@ library ieee; entity WishBoneSlaveE is generic ( Formal : boolean := false; + Simulation : boolean := false; AddressWidth : natural := 32; DataWidth : natural := 32 ); @@ -89,6 +90,8 @@ begin WbErr_o <= '1' when s_wb_slave_fsm = DATA and WbWe_i = '1' else '0'; + default clock is rising_edge(WbClk_i); + FormalG : if Formal generate -- Glue logic @@ -108,9 +111,6 @@ begin 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; @@ -190,4 +190,47 @@ begin end generate FormalG; + SimulationG : if Simulation generate + + 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"; + + 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"; + + WB_ACK : assert always + WbAck_o -> + (WbCyc_i and WbStb_i) + report "PSL ERROR: WbAck invalid"; + + 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 -> + (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 SimulationG; + + end architecture rtl; diff --git a/test/WishBoneT.vhd b/test/WishBoneT.vhd index 38147c4..b9f8659 100644 --- a/test/WishBoneT.vhd +++ b/test/WishBoneT.vhd @@ -160,6 +160,13 @@ begin i_WishBoneMasterE : WishBoneMasterE + generic map ( + Coverage => false, + Formal => false, + Simulation => true, + AddressWidth => C_ADDRESS_WIDTH, + DataWidth => C_DATA_WIDTH + ) port map ( --+ wishbone system if WbRst_i => s_wb_reset, @@ -212,6 +219,12 @@ begin i_WishBoneSlaveE : WishBoneSlaveE + generic map ( + Formal => false, + Simulation => true, + AddressWidth => C_ADDRESS_WIDTH, + DataWidth => C_DATA_WIDTH + ) port map ( --+ wishbone system if WbRst_i => s_wb_reset,