mirror of
https://github.com/lowRISC/ibex.git
synced 2025-06-28 17:24:11 -04:00
fb2a17a5a4
Also (and probably more interestingly) put in the tooling framework to drive sby in the two different modes.
27 lines
517 B
Text
27 lines
517 B
Text
# Copyright lowRISC contributors.
|
|
# Licensed under the Apache License, Version 2.0, see LICENSE for details.
|
|
# SPDX-License-Identifier: Apache-2.0
|
|
|
|
[tasks]
|
|
prove pf
|
|
cover cv
|
|
|
|
[options]
|
|
pf: mode prove
|
|
pf: depth 3
|
|
|
|
cv: mode cover
|
|
cv: depth 32
|
|
|
|
[engines]
|
|
smtbmc boolector
|
|
|
|
[script]
|
|
read -sv @INPUT@
|
|
|
|
# Our formal properties are currently just about control logic, which
|
|
# isn't affected by the exact behaviour of the memories in the design.
|
|
# Blackbox them.
|
|
blackbox $abstract\prim_generic_ram_1p
|
|
|
|
prep -top ibex_icache
|