Skip to content

Commit ee1ca61

Browse files
rswarbrickrswarbrick
committed
A simple formal flow for the ICache based on SymbiYosys
To get this working, you need a corresponding patch in Edalize, which adds SymbiYosys as an EDA tool. At the moment, this proves a couple of simple bus assertions. Later patches will add more. There are currently some rough edges to this flow: (1) We use a hacky pre_build hook to run sv2v and edit the files in the work tree. Among other problems, this means that the any failure messages that come out of sby have bogus line numbers. (2) Since we haven't yet got bind support in Yosys, we have to include a fragment from the design itself.
1 parent e4dbe46 commit ee1ca61

7 files changed

Lines changed: 487 additions & 0 deletions

File tree

‎formal/icache/Makefile‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
# Copyright lowRISC contributors.
2+
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
3+
# SPDX-License-Identifier: Apache-2.0
4+
5+
# A simple wrapper around fusesoc to make it a bit easier to run the formal flow
6+
7+
core-name := lowrisc:fpv:ibex_icache_fpv
8+
vlnv := $(subst :,_,$(core-name))
9+
build-root := $(abspath ../../build/$(vlnv))
10+
11+
fusesoc-run := cd ../..; fusesoc --cores-root=. run
12+
13+
.PHONY: all prove lint
14+
all: prove
15+
16+
prove:
17+
fusesoc --cores-root=../.. run --build-root=$(build-root) $(core-name)
18+
19+
lint:
20+
mypy --strict sv2v_in_place.py

‎formal/icache/formal_tb.sv‎

Lines changed: 169 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,169 @@
1+
// Copyright lowRISC contributors.
2+
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
3+
// SPDX-License-Identifier: Apache-2.0
4+
5+
// A formal testbench for the ICache. This gets bound into the actual ICache DUT.
6+
7+
`include "prim_assert.sv"
8+
9+
// A macro to emulate |-> (a syntax that Yosys doesn't currently support).
10+
`define IMPLIES(a, b) ((b) || (!(a)))
11+
12+
module formal_tb #(
13+
// DUT parameters
14+
parameter int unsigned BusWidth = 32,
15+
parameter int unsigned CacheSizeBytes = 4*1024,
16+
parameter bit ICacheECC = 1'b0,
17+
parameter int unsigned LineSize = 64,
18+
parameter int unsigned NumWays = 2,
19+
parameter bit SpecRequest = 1'b0,
20+
parameter bit BranchCache = 1'b0,
21+
22+
// Internal parameters / localparams
23+
parameter int unsigned NUM_FB = 4
24+
) (
25+
// Top-level ports
26+
input logic clk_i,
27+
input logic rst_ni,
28+
input logic req_i,
29+
input logic branch_i,
30+
input logic branch_spec_i,
31+
input logic [31:0] addr_i,
32+
input logic ready_i,
33+
input logic valid_o,
34+
input logic [31:0] rdata_o,
35+
input logic [31:0] addr_o,
36+
input logic err_o,
37+
input logic err_plus2_o,
38+
input logic instr_req_o,
39+
input logic instr_gnt_i,
40+
input logic [31:0] instr_addr_o,
41+
input logic [BusWidth-1:0] instr_rdata_i,
42+
input logic instr_err_i,
43+
input logic instr_pmp_err_i,
44+
input logic instr_rvalid_i,
45+
input logic icache_enable_i,
46+
input logic icache_inval_i,
47+
input logic busy_o,
48+
49+
// Internal signals
50+
input logic [NUM_FB-1:0] fill_busy_q,
51+
input logic [NUM_FB-1:0][NUM_FB-1:0] fill_older_q
52+
);
53+
54+
// We are bound into the DUT. This means we don't control the clock and reset directly, but we
55+
// still want to constrain rst_ni to reset the module at the start of time (for one cycle) and
56+
// then stay high.
57+
//
58+
// Note that having a cycle with rst_ni low at the start of time means that we can safely use
59+
// $past, $rose and $fell in calls to `ASSERT without any need for an "f_past_valid signal": they
60+
// will only be evaluated from cycle 2 onwards.
61+
logic [1:0] f_startup_count = 2'd0;
62+
always_ff @(posedge clk_i) begin : reset_assertion
63+
f_startup_count <= f_startup_count + ((f_startup_count == 2'd3) ? 2'd0 : 2'd1);
64+
65+
// Assume that rst_ni is low for the first cycle and not true after that.
66+
assume (~((f_startup_count == 2'd0) ^ ~rst_ni));
67+
68+
// There is a feed-through path from branch_i to req_o which isn't squashed when in reset. Assume
69+
// that branch_i isn't asserted when in reset.
70+
assume (`IMPLIES(!rst_ni, !branch_i));
71+
end
72+
73+
// Top-level assertions
74+
//
75+
// This section contains the assertions that prove the properties we care about. All should be
76+
// about observable signals (so shouldn't contain any references to anything that isn't exposed as
77+
// an input port).
78+
79+
// REQ stays high until GNT
80+
//
81+
// If instr_req_o goes high, we won't drive it low again until instr_gnt_i or instr_pmp_err_i is
82+
// high (the latter signals that the outgoing request got squashed, so we can forget about it).
83+
//
84+
// Read this as "a negedge of instr_req_o implies that the transaction was granted or squashed on
85+
// the previous cycle".
86+
`ASSERT(req_to_gnt,
87+
`IMPLIES($fell(instr_req_o), $past(instr_gnt_i | instr_pmp_err_i)))
88+
89+
// ADDR stability
90+
//
91+
// If instr_req_o goes high, the address at instr_addr_o will stay constant until the request is
92+
// squashed or granted. The encoding below says "either the address is stable, the request has
93+
// been squashed, we've had a grant or this is a new request".
94+
`ASSERT(req_addr_stable,
95+
$stable(instr_addr_o) | $past(instr_gnt_i | instr_pmp_err_i | ~instr_req_o))
96+
97+
98+
// Internal (induction) assertions
99+
//
100+
// Code below this line can refer to internal signals of the DUT. The assertions shouldn't be
101+
// needed for BMC checks, but will be required to constrain the state space used for k-induction.
102+
103+
for (genvar fb = 0; fb < NUM_FB; fb++) begin : g_fb_older_asserts
104+
// If fill buffer i is busy then fill_older_q[i][j] means that that fill buffer j has an
105+
// outstanding request which started before us (and should take precedence). We should check
106+
// that this only happens if buffer j is indeed busy.
107+
//
108+
// fill_busy_q[i] -> fill_older_q[i][j] -> fill_busy_q[j]
109+
//
110+
// which we can encode as
111+
//
112+
// (fill_older_q[i][j] -> fill_busy_q[j]) | ~fill_busy_q[i]
113+
// = (fill_busy_q[j] | ~fill_older_q[i][j]) | ~fill_busy_q[i]
114+
//
115+
// Grouping by j, we can rewrite this as:
116+
`ASSERT(older_is_busy, &(fill_busy_q | ~fill_older_q[fb]) | ~fill_busy_q[fb])
117+
118+
// No fill buffer should ever think that it's older than itself
119+
`ASSERT(older_anti_refl, !fill_older_q[fb][fb])
120+
121+
// The "older" relation should be anti-symmetric (a fill buffer can't be both older than, and
122+
// younger than, another). This takes NUM_FB*(NUM_FB-1)/2 assertions, comparing each pair of
123+
// buffers. Here, we do this by looping over the indices below fb.
124+
//
125+
// If I and J both think the other is older, then fill_older_q[I][J] and fill_older_q[J][I] will
126+
// both be true. Check that doesn't happen.
127+
for (genvar fb2 = 0; fb2 < fb; fb2++) begin : g_older_anti_symm_asserts
128+
`ASSERT(older_anti_symm, ~(fill_older_q[fb][fb2] & fill_older_q[fb2][fb]))
129+
end
130+
131+
// The older relation should be transitive (if i is older than j and j is older than k, then i
132+
// is older than k). That is:
133+
//
134+
// (fill_busy_q[i] & fill_older_q[i][j]) ->
135+
// (fill_busy_q[j] & fill_older_q[j][k]) ->
136+
// (fill_busy_q[i] & fill_older_q[i][k])
137+
//
138+
// Note that the second fill_busy_q[i] holds trivially and fill_busy_q[j] holds because of
139+
// order_is_busy, so this can be rewritten as:
140+
//
141+
// fill_busy_q[i] & fill_older_q[i][j] -> fill_older_q[j][k] -> fill_older_q[i][k]
142+
//
143+
// Converting A->B->C into (A&B)->C and then rewriting A->B as B|~A, this is equivalent to
144+
//
145+
// (fill_older_q[i][k] | ~fill_older_q[j][k]) | ~(fill_busy_q[i] & fill_older_q[i][j])
146+
//
147+
// Looping over i and j, we can simplify this as
148+
//
149+
// &(fill_older_q[i] | ~fill_older_q[j]) | ~(fill_busy_q[i] & fill_older_q[i][j])
150+
//
151+
for (genvar fb2 = 0; fb2 < NUM_FB; fb2++) begin : g_older_transitive_asserts
152+
`ASSERT(older_transitive,
153+
(&(fill_older_q[fb] | ~fill_older_q[fb2]) |
154+
~(fill_busy_q[fb] & fill_older_q[fb][fb2])))
155+
end
156+
157+
// The older relation should be total. This is a bit finicky because of fill buffers that aren't
158+
// currently busy. Specifically, we want
159+
//
160+
// i != j -> fill_busy_q[i] -> fill_busy_q[j] -> (fill_older_q[i][j] | fill_older_q[j][i])
161+
//
162+
for (genvar fb2 = 0; fb2 < fb; fb2++) begin : g_older_total_asserts
163+
`ASSERT(older_total,
164+
`IMPLIES(fill_busy_q[fb] & fill_busy_q[fb2],
165+
fill_older_q[fb][fb2] | fill_older_q[fb2][fb]))
166+
end
167+
end
168+
169+
endmodule

‎formal/icache/formal_tb_frag.svh‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
// Copyright lowRISC contributors.
2+
// Licensed under the Apache License, Version 2.0, see LICENSE for details.
3+
// SPDX-License-Identifier: Apache-2.0
4+
5+
// A fragment of SystemVerilog code that is inserted into the ICache. We're using this to emulate
6+
// missing bind support, so this file should do nothing but instantiate a module.
7+
//
8+
// Using a wildcard (.*) for ports allows the testbench to inspect internal signals of the cache.
9+
10+
formal_tb #(
11+
.BusWidth (BusWidth),
12+
.CacheSizeBytes (CacheSizeBytes),
13+
.ICacheECC (ICacheECC),
14+
.LineSize (LineSize),
15+
.NumWays (NumWays),
16+
.SpecRequest (SpecRequest),
17+
.BranchCache (BranchCache),
18+
19+
.NUM_FB (NUM_FB)
20+
) tb_i (.*);

‎formal/icache/ibex_icache_fpv.core‎

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,60 @@
1+
CAPI=2:
2+
# Copyright lowRISC contributors.
3+
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
4+
# SPDX-License-Identifier: Apache-2.0
5+
6+
name: "lowrisc:fpv:ibex_icache_fpv:0.1"
7+
description: "Formal properties for Ibex ICache"
8+
9+
filesets:
10+
all:
11+
depend:
12+
- lowrisc:ibex:ibex_icache
13+
- lowrisc:prim:assert
14+
files:
15+
- run.sby : {file_type: sbyConfig}
16+
- formal_tb_frag.svh : {file_type: systemVerilogSource, is_include_file: true}
17+
- formal_tb.sv : {file_type: systemVerilogSource}
18+
- sv2v_in_place.py : { copyto: sv2v_in_place.py }
19+
20+
scripts:
21+
sv2v_in_place:
22+
cmd:
23+
- python3
24+
- sv2v_in_place.py
25+
- --incdir-list=incdirs.txt
26+
# A bit of a hack: The primitives directory (vendored from OpenTitan)
27+
# contains SystemVerilog code that has proper SVA assertions, using
28+
# things like the |-> operator.
29+
#
30+
# The Yosys-style prim_assert.sv assertions are immediate, rather than
31+
# concurrent. Such assertions only allow expressions (not full property
32+
# specifiers), which cause a syntax error if you try to use them with
33+
# the assertions in the primitives directory.
34+
#
35+
# Since we don't care about those assertions here, we want to strip
36+
# them out. The code that selects an assertion backend in
37+
# prim_assert.sv doesn't have an explicit "NO_ASSERTIONS" mode, but
38+
# "SYNTHESIS" implies the same thing, so we use that.
39+
- --define-if=prim:SYNTHESIS
40+
- -DYOSYS
41+
- -DFORMAL
42+
- -v
43+
- files.txt
44+
45+
parameters:
46+
ICacheECC:
47+
datatype: int
48+
default: 0
49+
paramtype: vlogparam
50+
description: "Enable ECC protection in instruction cache"
51+
52+
targets:
53+
default:
54+
hooks:
55+
pre_build:
56+
- sv2v_in_place
57+
filesets:
58+
- all
59+
toplevel: tb
60+
default_tool: symbiyosys

‎formal/icache/run.sby‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
# Copyright lowRISC contributors.
2+
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
3+
# SPDX-License-Identifier: Apache-2.0
4+
5+
[options]
6+
mode prove
7+
depth 3
8+
9+
[engines]
10+
smtbmc boolector
11+
12+
[script]
13+
read -sv @INPUT@
14+
15+
# We don't care about the exact behaviour of the memories in the
16+
# design, so we should blackbox them.
17+
blackbox $abstract\prim_generic_ram_1p
18+
19+
prep -top ibex_icache

0 commit comments

Comments
 (0)