Add formal verification of Wishbone components

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

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

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

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;
 

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;