# 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]
{{"-sv"|gen_reads}}

# 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 {{top_level}}

[files]
{{files}}
