Browse Source

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
T. Meissner 3 months ago
parent
commit
83d3e05757
7 changed files with 134 additions and 18 deletions
  1. 7
    2
      formal/Makefile
  2. 7
    3
      formal/WishBoneMasterE.sby
  3. 6
    1
      formal/WishBoneSlaveE.sby
  4. 42
    9
      syn/WishBoneMasterE.vhd
  5. 13
    0
      syn/WishBoneP.vhd
  6. 46
    3
      syn/WishBoneSlaveE.vhd
  7. 13
    0
      test/WishBoneT.vhd

+ 7
- 2
formal/Makefile View File

@@ -1,6 +1,7 @@
1
-.PHONY: all-cover all-prove all
2
-all: all-cover all-prove
1
+.PHONY: all-cover all-bmc all-prove all
2
+all: all-cover all-bmc all-prove
3 3
 all-cover: WishBoneMasterE-cover WishBoneSlaveE-cover
4
+all-bmc: WishBoneMasterE-bmc WishBoneSlaveE-bmc
4 5
 all-prove: WishBoneMasterE-prove WishBoneSlaveE-prove
5 6
 
6 7
 
@@ -8,6 +9,10 @@ all-prove: WishBoneMasterE-prove WishBoneSlaveE-prove
8 9
 	mkdir -p work
9 10
 	sby --yosys "yosys -m ghdl" -f -d work/$@ $(subst -cover,,$@).sby cover
10 11
 
12
+%-bmc: ../syn/%.vhd %.sby
13
+	mkdir -p work
14
+	sby --yosys "yosys -m ghdl" -f -d work/$@ $(subst -bmc,,$@).sby bmc
15
+
11 16
 %-prove: ../syn/%.vhd %.sby
12 17
 	mkdir -p work
13 18
 	sby --yosys "yosys -m ghdl" -f -d work/$@ $(subst -prove,,$@).sby prove

+ 7
- 3
formal/WishBoneMasterE.sby View File

@@ -1,19 +1,23 @@
1 1
 [tasks]
2
+bmc
2 3
 prove
3 4
 cover
4 5
 
5 6
 [options]
6
-depth 20
7
+depth 25
8
+bmc: mode bmc
7 9
 prove: mode prove
8 10
 cover: mode cover
9 11
 
10 12
 [engines]
13
+bmc: smtbmc z3
11 14
 prove: abc pdr
12 15
 cover: smtbmc z3
13 16
 
14 17
 [script]
15
-prove: ghdl --std=08 -gCoverage=false -gFormal=true -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere
16
-cover: ghdl --std=08 -gCoverage=true -gFormal=true -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere
18
+bmc: ghdl --std=08 -gCoverage=false -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere
19
+prove: ghdl --std=08 -gCoverage=false -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere
20
+cover: ghdl --std=08 -gCoverage=true -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneMasterE.vhd -e wishbonemastere
17 21
 prep -auto-top
18 22
 
19 23
 [files]

+ 6
- 1
formal/WishBoneSlaveE.sby View File

@@ -1,18 +1,23 @@
1 1
 [tasks]
2
+bmc
2 3
 prove
3 4
 cover
4 5
 
5 6
 [options]
6 7
 depth 25
8
+bmc: mode bmc
7 9
 prove: mode prove
8 10
 cover: mode cover
9 11
 
10 12
 [engines]
13
+bmc: smtbmc z3
11 14
 prove: abc pdr
12 15
 cover: smtbmc z3
13 16
 
14 17
 [script]
15
-ghdl --std=08 -gFormal=true -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee
18
+bmc: ghdl --std=08 -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee
19
+prove: ghdl --std=08 -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee
20
+cover: ghdl --std=08 -gFormal=true -gSimulation=false -gAddressWidth=32 -gDataWidth=32 WishBoneSlaveE.vhd -e wishboneslavee
16 21
 prep -auto-top
17 22
 
18 23
 [files]

+ 42
- 9
syn/WishBoneMasterE.vhd View File

@@ -6,8 +6,9 @@ library ieee;
6 6
 
7 7
 entity WishBoneMasterE is
8 8
   generic (
9
-    Coverage     : boolean := true;
10
-    Formal       : boolean := true;
9
+    Coverage     : boolean := false;
10
+    Formal       : boolean := false;
11
+    Simulation   : boolean := false;
11 12
     AddressWidth : natural := 8;
12 13
     DataWidth    : natural := 8
13 14
   );
@@ -119,6 +120,8 @@ begin
119 120
   end process OutRegsP;
120 121
 
121 122
 
123
+  default clock is rising_edge(WbClk_i);
124
+
122 125
   FormalG : if Formal generate
123 126
 
124 127
     -- Glue logic
@@ -141,9 +144,6 @@ begin
141 144
       end if;
142 145
     end process;
143 146
 
144
-
145
-    default clock is rising_edge(WbClk_i);
146
-
147 147
     restrict {WbRst_i = '1'; WbRst_i = '0'[+]}[*1];
148 148
 
149 149
     RESET : assert always
@@ -185,8 +185,6 @@ begin
185 185
 
186 186
   CoverageG : if Coverage generate
187 187
 
188
-    default clock is rising_edge(WbClk_i);
189
-
190 188
     restrict {WbRst_i = '1'; WbRst_i = '0'[+]}[*1];
191 189
 
192 190
     COVER_LOCAL_WRITE : cover {s_wb_master_fsm = IDLE and LocalWen_i = '1' and
@@ -201,9 +199,44 @@ begin
201 199
        LocalRen_i = '1' and WbRst_i = '0'}
202 200
       report "WB master: Local write & read";
203 201
 
204
-    test_cover : cover {s_wb_master_fsm = IDLE and LocalWen_i = '1'; s_wb_master_fsm = ADDRESS; s_wb_master_fsm = DATA};
205
-
206 202
   end generate CoverageG;
207 203
 
208 204
 
205
+  SimulationG : if Simulation generate
206
+
207
+    -- assert directives
208
+    RESET : assert always
209
+      WbRst_i ->
210
+      WbCyc_o = '0' and WbStb_o = '0' and WbWe_o = '0' and
211
+      to_integer(unsigned(WbAdr_o)) = 0 and to_integer(unsigned(WbDat_o)) = 0 and
212
+      LocalAck_o = '0' and LocalError_o = '0' and to_integer(unsigned(LocalData_o)) = 0
213
+      report "WB master: Reset error";
214
+
215
+    WB_WRITE : assert always
216
+      ((not(WbCyc_o) and not(WbStb_o) and LocalWen_i and not (LocalRen_i)) ->
217
+      next (WbCyc_o = '1' and WbStb_o = '1' and WbWe_o = '1')) abort WbRst_i
218
+      report "WB master: Write error";
219
+
220
+    WB_READ : assert always
221
+      ((not(WbCyc_o) and not(WbStb_o) and LocalRen_i and not(LocalWen_i)) ->
222
+      next (WbCyc_o = '1' and WbStb_o = '1' and WbWe_o = '0')) abort WbRst_i
223
+      report "WB master: Read error";
224
+
225
+
226
+    -- cover directives
227
+    COVER_LOCAL_WRITE : cover {s_wb_master_fsm = IDLE and LocalWen_i = '1' and
228
+      LocalRen_i = '0' and WbRst_i = '0'}
229
+      report "WB master: Local write";
230
+
231
+    COVER_LOCAL_READ : cover {s_wb_master_fsm = IDLE and LocalRen_i = '1' and
232
+      LocalWen_i = '0' and WbRst_i = '0'}
233
+      report "WB master: Local read";
234
+
235
+    COVER_LOCAL_WRITE_READ : cover {s_wb_master_fsm = IDLE and LocalWen_i = '1' and
236
+      LocalRen_i = '1' and WbRst_i = '0'}
237
+      report "WB master: Local write & read";
238
+
239
+  end generate SimulationG;
240
+
241
+
209 242
 end architecture rtl;

+ 13
- 0
syn/WishBoneP.vhd View File

@@ -8,6 +8,13 @@ package WishBoneP is
8 8
 
9 9
 
10 10
   component WishBoneMasterE is
11
+    generic (
12
+      Coverage     : boolean := false;
13
+      Formal       : boolean := false;
14
+      Simulation   : boolean := false;
15
+      AddressWidth : natural := 8;
16
+      DataWidth    : natural := 8
17
+    );
11 18
     port (
12 19
       --+ wishbone system if
13 20
       WbRst_i       : in  std_logic;
@@ -35,6 +42,12 @@ package WishBoneP is
35 42
 
36 43
 
37 44
   component WishBoneSlaveE is
45
+    generic (
46
+      Formal       : boolean := false;
47
+      Simulation   : boolean := false;
48
+      AddressWidth : natural := 32;
49
+      DataWidth    : natural := 32
50
+    );
38 51
     port (
39 52
       --+ wishbone system if
40 53
       WbRst_i       : in  std_logic;

+ 46
- 3
syn/WishBoneSlaveE.vhd View File

@@ -7,6 +7,7 @@ library ieee;
7 7
 entity WishBoneSlaveE is
8 8
   generic (
9 9
     Formal       : boolean := false;
10
+    Simulation   : boolean := false;
10 11
     AddressWidth : natural := 32;
11 12
     DataWidth    : natural := 32
12 13
   );
@@ -89,6 +90,8 @@ begin
89 90
   WbErr_o <= '1' when s_wb_slave_fsm = DATA and WbWe_i = '1' else '0';
90 91
 
91 92
 
93
+  default clock is rising_edge(WbClk_i);
94
+
92 95
   FormalG : if Formal generate
93 96
 
94 97
     -- Glue logic
@@ -108,9 +111,6 @@ begin
108 111
       end if;
109 112
     end process SyncWbSignals;
110 113
 
111
-
112
-    default clock is rising_edge(WbClk_i);
113
-
114 114
     restrict {WbRst_i = '1'; WbRst_i = '0'[+]}[*1];
115 115
 
116 116
     assume always WbCyc_i = WbStb_i;
@@ -190,4 +190,47 @@ begin
190 190
   end generate FormalG;
191 191
 
192 192
 
193
+  SimulationG : if Simulation generate
194
+
195
+    LOCAL_WRITE : assert always
196
+      ((WbCyc_i and WbStb_i and WbWe_i) ->
197
+       (LocalWen_o = '1' and WbAck_o = '1' and LocalAdress_o = WbAdr_i and LocalData_o = WbDat_i)) abort WbRst_i
198
+      report "PSL ERROR: Local write error";
199
+
200
+    LOCAL_READ : assert always
201
+      ({not(WbCyc_i) and not(WbStb_i); WbCyc_i and WbStb_i and not(WbWe_i)} |->
202
+       {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
203
+      report "PSL ERROR: Local read error";
204
+
205
+    WB_ACK : assert always
206
+      WbAck_o ->
207
+      (WbCyc_i and WbStb_i)
208
+      report "PSL ERROR: WbAck invalid";
209
+
210
+    WB_ERR : assert always
211
+      WbErr_o ->
212
+      (WbCyc_i and WbStb_i)
213
+      report "PSL ERROR: WbErr invalid";
214
+
215
+    LOCAL_WE : assert always
216
+      LocalWen_o ->
217
+      (WbCyc_i and WbStb_i and WbWe_i and not(LocalRen_o)) and
218
+      (next not(LocalWen_o))
219
+      report "PSL ERROR: LocalWen invalid";
220
+
221
+    LOCAL_RE : assert always
222
+      LocalRen_o ->
223
+      (WbCyc_i and WbStb_i and not(WbWe_i) and not(LocalWen_o)) and
224
+      (next not(LocalRen_o))
225
+      report "PSL ERROR: LocalRen invalid";
226
+
227
+    RESET : assert always
228
+      WbRst_i ->
229
+      (to_integer(unsigned(WbDat_o)) = 0 and WbAck_o = '0' and WbErr_o = '0' and
230
+       LocalWen_o = '0' and LocalRen_o = '0' and to_integer(unsigned(LocalAdress_o)) = 0 and to_integer(unsigned(LocalData_o)) = 0)
231
+      report "PSL ERROR: Reset error";
232
+
233
+  end generate SimulationG;
234
+
235
+
193 236
 end architecture rtl;

+ 13
- 0
test/WishBoneT.vhd View File

@@ -160,6 +160,13 @@ begin
160 160
 
161 161
 
162 162
   i_WishBoneMasterE : WishBoneMasterE
163
+    generic map (
164
+      Coverage     => false,
165
+      Formal       => false,
166
+      Simulation   => true,
167
+      AddressWidth => C_ADDRESS_WIDTH,
168
+      DataWidth    => C_DATA_WIDTH
169
+    )
163 170
     port map (
164 171
       --+ wishbone system if
165 172
       WbRst_i       => s_wb_reset,
@@ -212,6 +219,12 @@ begin
212 219
 
213 220
 
214 221
   i_WishBoneSlaveE : WishBoneSlaveE
222
+    generic map (
223
+      Formal       => false,
224
+      Simulation   => true,
225
+      AddressWidth => C_ADDRESS_WIDTH,
226
+      DataWidth    => C_DATA_WIDTH
227
+    )
215 228
     port map (
216 229
       --+ wishbone system if
217 230
       WbRst_i       => s_wb_reset,