diff --git a/formal/icache/Makefile b/formal/icache/Makefile new file mode 100644 index 00000000..423c401b --- /dev/null +++ b/formal/icache/Makefile @@ -0,0 +1,20 @@ +# Copyright lowRISC contributors. +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +# A simple wrapper around fusesoc to make it a bit easier to run the formal flow + +core-name := lowrisc:fpv:ibex_icache_fpv +vlnv := $(subst :,_,$(core-name)) +build-root := $(abspath ../../build/$(vlnv)) + +fusesoc-run := cd ../..; fusesoc --cores-root=. run + +.PHONY: all prove lint +all: prove + +prove: + fusesoc --cores-root=../.. run --build-root=$(build-root) $(core-name) + +lint: + mypy --strict sv2v_in_place.py diff --git a/formal/icache/formal_tb.sv b/formal/icache/formal_tb.sv new file mode 100644 index 00000000..77a06552 --- /dev/null +++ b/formal/icache/formal_tb.sv @@ -0,0 +1,169 @@ +// Copyright lowRISC contributors. +// Licensed under the Apache License, Version 2.0, see LICENSE for details. +// SPDX-License-Identifier: Apache-2.0 + +// A formal testbench for the ICache. This gets bound into the actual ICache DUT. + +`include "prim_assert.sv" + +// A macro to emulate |-> (a syntax that Yosys doesn't currently support). +`define IMPLIES(a, b) ((b) || (!(a))) + +module formal_tb #( + // DUT parameters + parameter int unsigned BusWidth = 32, + parameter int unsigned CacheSizeBytes = 4*1024, + parameter bit ICacheECC = 1'b0, + parameter int unsigned LineSize = 64, + parameter int unsigned NumWays = 2, + parameter bit SpecRequest = 1'b0, + parameter bit BranchCache = 1'b0, + + // Internal parameters / localparams + parameter int unsigned NUM_FB = 4 +) ( + // Top-level ports + input logic clk_i, + input logic rst_ni, + input logic req_i, + input logic branch_i, + input logic branch_spec_i, + input logic [31:0] addr_i, + input logic ready_i, + input logic valid_o, + input logic [31:0] rdata_o, + input logic [31:0] addr_o, + input logic err_o, + input logic err_plus2_o, + input logic instr_req_o, + input logic instr_gnt_i, + input logic [31:0] instr_addr_o, + input logic [BusWidth-1:0] instr_rdata_i, + input logic instr_err_i, + input logic instr_pmp_err_i, + input logic instr_rvalid_i, + input logic icache_enable_i, + input logic icache_inval_i, + input logic busy_o, + + // Internal signals + input logic [NUM_FB-1:0] fill_busy_q, + input logic [NUM_FB-1:0][NUM_FB-1:0] fill_older_q +); + + // We are bound into the DUT. This means we don't control the clock and reset directly, but we + // still want to constrain rst_ni to reset the module at the start of time (for one cycle) and + // then stay high. + // + // Note that having a cycle with rst_ni low at the start of time means that we can safely use + // $past, $rose and $fell in calls to `ASSERT without any need for an "f_past_valid signal": they + // will only be evaluated from cycle 2 onwards. + logic [1:0] f_startup_count = 2'd0; + always_ff @(posedge clk_i) begin : reset_assertion + f_startup_count <= f_startup_count + ((f_startup_count == 2'd3) ? 2'd0 : 2'd1); + + // Assume that rst_ni is low for the first cycle and not true after that. + assume (~((f_startup_count == 2'd0) ^ ~rst_ni)); + + // There is a feed-through path from branch_i to req_o which isn't squashed when in reset. Assume + // that branch_i isn't asserted when in reset. + assume (`IMPLIES(!rst_ni, !branch_i)); + end + + // Top-level assertions + // + // This section contains the assertions that prove the properties we care about. All should be + // about observable signals (so shouldn't contain any references to anything that isn't exposed as + // an input port). + + // REQ stays high until GNT + // + // If instr_req_o goes high, we won't drive it low again until instr_gnt_i or instr_pmp_err_i is + // high (the latter signals that the outgoing request got squashed, so we can forget about it). + // + // Read this as "a negedge of instr_req_o implies that the transaction was granted or squashed on + // the previous cycle". + `ASSERT(req_to_gnt, + `IMPLIES($fell(instr_req_o), $past(instr_gnt_i | instr_pmp_err_i))) + + // ADDR stability + // + // If instr_req_o goes high, the address at instr_addr_o will stay constant until the request is + // squashed or granted. The encoding below says "either the address is stable, the request has + // been squashed, we've had a grant or this is a new request". + `ASSERT(req_addr_stable, + $stable(instr_addr_o) | $past(instr_gnt_i | instr_pmp_err_i | ~instr_req_o)) + + + // Internal (induction) assertions + // + // Code below this line can refer to internal signals of the DUT. The assertions shouldn't be + // needed for BMC checks, but will be required to constrain the state space used for k-induction. + + for (genvar fb = 0; fb < NUM_FB; fb++) begin : g_fb_older_asserts + // If fill buffer i is busy then fill_older_q[i][j] means that that fill buffer j has an + // outstanding request which started before us (and should take precedence). We should check + // that this only happens if buffer j is indeed busy. + // + // fill_busy_q[i] -> fill_older_q[i][j] -> fill_busy_q[j] + // + // which we can encode as + // + // (fill_older_q[i][j] -> fill_busy_q[j]) | ~fill_busy_q[i] + // = (fill_busy_q[j] | ~fill_older_q[i][j]) | ~fill_busy_q[i] + // + // Grouping by j, we can rewrite this as: + `ASSERT(older_is_busy, &(fill_busy_q | ~fill_older_q[fb]) | ~fill_busy_q[fb]) + + // No fill buffer should ever think that it's older than itself + `ASSERT(older_anti_refl, !fill_older_q[fb][fb]) + + // The "older" relation should be anti-symmetric (a fill buffer can't be both older than, and + // younger than, another). This takes NUM_FB*(NUM_FB-1)/2 assertions, comparing each pair of + // buffers. Here, we do this by looping over the indices below fb. + // + // If I and J both think the other is older, then fill_older_q[I][J] and fill_older_q[J][I] will + // both be true. Check that doesn't happen. + for (genvar fb2 = 0; fb2 < fb; fb2++) begin : g_older_anti_symm_asserts + `ASSERT(older_anti_symm, ~(fill_older_q[fb][fb2] & fill_older_q[fb2][fb])) + end + + // The older relation should be transitive (if i is older than j and j is older than k, then i + // is older than k). That is: + // + // (fill_busy_q[i] & fill_older_q[i][j]) -> + // (fill_busy_q[j] & fill_older_q[j][k]) -> + // (fill_busy_q[i] & fill_older_q[i][k]) + // + // Note that the second fill_busy_q[i] holds trivially and fill_busy_q[j] holds because of + // order_is_busy, so this can be rewritten as: + // + // fill_busy_q[i] & fill_older_q[i][j] -> fill_older_q[j][k] -> fill_older_q[i][k] + // + // Converting A->B->C into (A&B)->C and then rewriting A->B as B|~A, this is equivalent to + // + // (fill_older_q[i][k] | ~fill_older_q[j][k]) | ~(fill_busy_q[i] & fill_older_q[i][j]) + // + // Looping over i and j, we can simplify this as + // + // &(fill_older_q[i] | ~fill_older_q[j]) | ~(fill_busy_q[i] & fill_older_q[i][j]) + // + for (genvar fb2 = 0; fb2 < NUM_FB; fb2++) begin : g_older_transitive_asserts + `ASSERT(older_transitive, + (&(fill_older_q[fb] | ~fill_older_q[fb2]) | + ~(fill_busy_q[fb] & fill_older_q[fb][fb2]))) + end + + // The older relation should be total. This is a bit finicky because of fill buffers that aren't + // currently busy. Specifically, we want + // + // i != j -> fill_busy_q[i] -> fill_busy_q[j] -> (fill_older_q[i][j] | fill_older_q[j][i]) + // + for (genvar fb2 = 0; fb2 < fb; fb2++) begin : g_older_total_asserts + `ASSERT(older_total, + `IMPLIES(fill_busy_q[fb] & fill_busy_q[fb2], + fill_older_q[fb][fb2] | fill_older_q[fb2][fb])) + end + end + +endmodule diff --git a/formal/icache/formal_tb_frag.svh b/formal/icache/formal_tb_frag.svh new file mode 100644 index 00000000..c3927250 --- /dev/null +++ b/formal/icache/formal_tb_frag.svh @@ -0,0 +1,20 @@ +// Copyright lowRISC contributors. +// Licensed under the Apache License, Version 2.0, see LICENSE for details. +// SPDX-License-Identifier: Apache-2.0 + +// A fragment of SystemVerilog code that is inserted into the ICache. We're using this to emulate +// missing bind support, so this file should do nothing but instantiate a module. +// +// Using a wildcard (.*) for ports allows the testbench to inspect internal signals of the cache. + +formal_tb #( + .BusWidth (BusWidth), + .CacheSizeBytes (CacheSizeBytes), + .ICacheECC (ICacheECC), + .LineSize (LineSize), + .NumWays (NumWays), + .SpecRequest (SpecRequest), + .BranchCache (BranchCache), + + .NUM_FB (NUM_FB) +) tb_i (.*); diff --git a/formal/icache/ibex_icache_fpv.core b/formal/icache/ibex_icache_fpv.core new file mode 100644 index 00000000..b61cacd2 --- /dev/null +++ b/formal/icache/ibex_icache_fpv.core @@ -0,0 +1,60 @@ +CAPI=2: +# Copyright lowRISC contributors. +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +name: "lowrisc:fpv:ibex_icache_fpv:0.1" +description: "Formal properties for Ibex ICache" + +filesets: + all: + depend: + - lowrisc:ibex:ibex_icache + - lowrisc:prim:assert + files: + - run.sby : {file_type: sbyConfig} + - formal_tb_frag.svh : {file_type: systemVerilogSource, is_include_file: true} + - formal_tb.sv : {file_type: systemVerilogSource} + - sv2v_in_place.py : { copyto: sv2v_in_place.py } + +scripts: + sv2v_in_place: + cmd: + - python3 + - sv2v_in_place.py + - --incdir-list=incdirs.txt + # A bit of a hack: The primitives directory (vendored from OpenTitan) + # contains SystemVerilog code that has proper SVA assertions, using + # things like the |-> operator. + # + # The Yosys-style prim_assert.sv assertions are immediate, rather than + # concurrent. Such assertions only allow expressions (not full property + # specifiers), which cause a syntax error if you try to use them with + # the assertions in the primitives directory. + # + # Since we don't care about those assertions here, we want to strip + # them out. The code that selects an assertion backend in + # prim_assert.sv doesn't have an explicit "NO_ASSERTIONS" mode, but + # "SYNTHESIS" implies the same thing, so we use that. + - --define-if=prim:SYNTHESIS + - -DYOSYS + - -DFORMAL + - -v + - files.txt + +parameters: + ICacheECC: + datatype: int + default: 0 + paramtype: vlogparam + description: "Enable ECC protection in instruction cache" + +targets: + default: + hooks: + pre_build: + - sv2v_in_place + filesets: + - all + toplevel: tb + default_tool: symbiyosys diff --git a/formal/icache/run.sby b/formal/icache/run.sby new file mode 100644 index 00000000..48b534de --- /dev/null +++ b/formal/icache/run.sby @@ -0,0 +1,19 @@ +# Copyright lowRISC contributors. +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +[options] +mode prove +depth 3 + +[engines] +smtbmc boolector + +[script] +read -sv @INPUT@ + +# We don't care about the exact behaviour of the memories in the +# design, so we should blackbox them. +blackbox $abstract\prim_generic_ram_1p + +prep -top ibex_icache diff --git a/formal/icache/sv2v_in_place.py b/formal/icache/sv2v_in_place.py new file mode 100644 index 00000000..b8394a9b --- /dev/null +++ b/formal/icache/sv2v_in_place.py @@ -0,0 +1,190 @@ +#!/usr/bin/env python3 +# Copyright lowRISC contributors. +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +import argparse +import logging +import os +import re +import shlex +import shutil +import subprocess +import tempfile +from typing import List, Pattern, Tuple + + +def read_file_list(path: str) -> List[str]: + '''Read in a list of paths from a file, one per line.''' + ret = [] + with open(path) as handle: + for line in handle: + ret.append(line.strip()) + return ret + + +def transform_one(sv2v: str, + defines: List[str], + incdirs: List[str], + pkg_paths: List[str], + sv_path: str, + dst_path: str) -> None: + '''Run sv2v to edit a file in place''' + defines_args = ['--define=' + d for d in defines] + incdirs_args = ['--incdir=' + d for d in incdirs] + paths = pkg_paths + ([] if sv_path in pkg_paths else [sv_path]) + + cmd = ([sv2v, + # Pass --exclude=assert to tell sv2v not to strip out assertions. + # Since the whole point of this flow is to prove assertions, we + # need to leave them unscathed! + '--exclude=assert'] + + defines_args + + incdirs_args + + paths) + logging.info('Running sv2v on {}'.format(sv_path)) + logging.debug('Command: {}'.format(cmd)) + with open(dst_path, 'w') as dst_file: + proc = subprocess.run(cmd, stdout=dst_file) + if proc.returncode != 0: + cmd_str = ' '.join([shlex.quote(a) for a in cmd]) + raise RuntimeError('Failed to run sv2v on {}. ' + 'Exit code: {}. Full command: {}' + .format(sv_path, proc.returncode, cmd_str)) + + +def parse_define_if(arg: str) -> Tuple[Pattern[str], str]: + '''Handle a --define-if argument''' + parts = arg.rsplit(':', 1) + if len(parts) != 2: + msg = ('The --define-if argument {!r} contains no colon. The correct ' + 'syntax is "--define-if regex:define".' + .format(arg)) + raise argparse.ArgumentTypeError(msg) + + re_str, define = parts + try: + return (re.compile(re_str), define) + except re.error as err: + raise argparse.ArgumentTypeError('The regex for the --define-if ' + 'argument ({!r}) is malformed: {}.' + .format(re_str, err)) + + +def transform(sv2v: str, + defines: List[str], + defines_if: List[Tuple[Pattern[str], str]], + incdirs: List[str], + pkg_paths: List[str], + sv_paths: List[str]) -> None: + '''Run sv2v to transform a list of files in-place''' + with tempfile.TemporaryDirectory() as tmpdir: + # First write each file to a file in a temporary directory, then copy + # everything back. We have to do it like this because otherwise we + # might trash a file that needs to be included by a later one. + dst_paths = [] + for idx, src_path in enumerate(sv_paths): + dst_path = os.path.join(tmpdir, str(idx)) + + extra_file_defines = [] + for regex, define in defines_if: + if regex.search(src_path): + extra_file_defines.append(define) + + transform_one(sv2v, defines + extra_file_defines, + incdirs, pkg_paths, src_path, dst_path) + dst_paths.append(dst_path) + + # Now copy everything back, overwriting the original code + for dst_path, src_path in zip(dst_paths, sv_paths): + shutil.copy(dst_path, src_path) + + +def main() -> int: + parser = argparse.ArgumentParser() + parser.add_argument('file_list', + help=('File containing a list of ' + 'paths on which to work.')) + parser.add_argument('--verbose', '-v', action='store_true', + help="Log messages about what we're doing.") + parser.add_argument('--define', '-D', action='append', dest='defines', + default=[], + help='Add a preprocessor define.') + parser.add_argument('--define-if', action='append', + dest='defines_if', type=parse_define_if, default=[], + help=('Add a preprocessor define which applies to ' + 'specific files. For example ' + '--define-if=foo:bar would define `bar on any ' + 'files whose paths contained a match for the ' + 'regex "foo".')) + parser.add_argument('--incdir', '-I', action='append', dest='incdirs', + default=[], + help='Add an include dir for the preprocessor.') + parser.add_argument('--incdir-list', + help=('Specify a file containing a list of include ' + 'directories (which are appended to any defined ' + 'through the --incdir argument).')) + parser.add_argument('--sv2v', + default='sv2v', + help=("Specify the name or path of the sv2v binary. " + "Defaults to 'sv2v'.")) + + args = parser.parse_args() + + if args.verbose: + logging.basicConfig(level=logging.INFO) + + try: + logging.info('Reading file list from {!r}.'.format(args.file_list)) + paths = read_file_list(args.file_list) + except IOError: + logging.error('Failed to read file list from {!r}' + .format(args.file_list)) + return 1 + + if args.incdir_list is not None: + try: + logging.info('Reading incdir list from {!r}.' + .format(args.incdir_list)) + args.incdirs += read_file_list(args.incdir_list) + except IOError: + logging.error('Failed to read incdir list from {!r}' + .format(args.file_list)) + return 1 + + # Find all .sv or .svh files, splitting out paths ending in "pkg.sv" + # specially. We treat these as packages, which are included in each sv2v + # conversion. + sv_paths = [] + svh_paths = [] + pkg_paths = [] + for path in paths: + if os.path.splitext(path)[1] == '.sv': + sv_paths.append(path) + if os.path.splitext(path)[1] == '.svh': + svh_paths.append(path) + if path.endswith('pkg.sv'): + pkg_paths.append(path) + + logging.info('Running sv2v in-place on {} files ({} packages).' + .format(len(sv_paths), len(pkg_paths))) + + try: + transform(args.sv2v, args.defines, args.defines_if, args.incdirs, + pkg_paths, sv_paths) + except RuntimeError as err: + logging.error(err) + return 1 + + # Empty out any remaining .svh files: they should have been included by + # this point (sv2v includes a preprocessor). + logging.info('Splatting contents of {} .svh files.'.format(len(svh_paths))) + for path in svh_paths: + with open(path, 'w'): + pass + + return 0 + + +if __name__ == '__main__': + exit(main()) diff --git a/rtl/ibex_icache.sv b/rtl/ibex_icache.sv index 9a12fdb4..796819cc 100644 --- a/rtl/ibex_icache.sv +++ b/rtl/ibex_icache.sv @@ -1022,4 +1022,13 @@ module ibex_icache #( `ASSERT_KNOWN(TagHitKnown, lookup_valid_ic1 & tag_hit_ic1) `ASSERT_KNOWN(TagInvalidKnown, lookup_valid_ic1 & tag_invalid_ic1) + // This is only used for the Yosys-based formal flow. Once we have working bind support, we can + // get rid of it. +`ifdef FORMAL + `ifdef YOSYS + `include "formal_tb_frag.svh" + `endif +`endif + + endmodule