Assertions are statements about your design that are expected to be always true. Here are two examples:
Above examples are using the `ASSERT macro defined in prim_assert.sv, whose four arguments are assertion name, property, clock, and reset (active-high reset).
Assertions are usually added by the designer in the RTL file. Assertions can also be added in a separate module, see for example tlul_assert.sv and its [documentation]({{< relref “hw/ip/tlul/doc/TlulProtocolChecker.md” >}}), which contains a generic protocol checker for the TileLink-UL standard.
There are two types of assertions:
initial begin checkFifoWidth: assert (FifoDepth > 0) else begin $error("FifoDepth parameter should be > 0"); end end
The file prim_assert.sv and prim_assert_standard_macros.svh define many useful shortcuts that you can use in your RTL code. Some of them are detailed below:
ASSERT_DEFAULT_CLK, __rst =
ASSERT_DEFAULT_RST)req |-> ack
.For example, `ASSERT(myAssertion, req |-> ack, clk, !rst_n) is expanded as follows:
myAssertion: assert property ( @(posedge clk) disable iff ((!rst_n) !== 1'b0) (req |-> ack) ) else begin $error("Assert failed: [%m] %s: %s\n", `STRINGIFY(myAssertion), `STRINGIFY(req |-> ack)); end
Concurrent assertion inside an initial block. It can be used for checking parameters.
Concurrent assertion inside a final block. It can be used e.g. for making sure that a FIFO is empty at the end of each sim.
ASSERT_NEVER(__name, __prop, __clk =
ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST)Assert that a concurrent property never happens.
ASSERT_KNOWN(__name, __signal, __clk =
ASSERT_DEFAULT_CLK, __rst = `ASSERT_DEFAULT_RST)Assert that signal
has a known value after reset, where “known” refers to a value that is not X.
grep -r ASSERT .
Below table lists useful SVA (SystemVerilog assertion) functions that can be used for assertion properties.
Below table lists useful operators that can be used for assertion properties.
There are also powerful repetition operators, see here for more details.
When design has a set of modules or signals that share same properties, symbolic variables can be used to reduce duplicated assertions. For example, in the rv_plic design, the array of input intr_src_i
are signals sharing the same properties. Each intr_src_i[index]
will trigger the interrupt pending (ip
) signal depending on the corresponding level indicator (le
) is set to level triggered or edge triggered. Without symbolic variables, the above assertions can be implemented as below:
genvar i; generate for (i = 0; i < N_SOURCE; i++) begin : gen_rv_plic_fpv `ASSERT(LevelTriggeredIp_A, $rose(rv_plic.ip[i]) |-> $past(rv_plic.le[i]) || $past(intr_src_i[i]), clk_i, !rst_ni) end
In contrast, symbolic variable can abstract the design by declaring the index with constraints. To ensure the symbolic variable performs the expected behaviors, two assumptions need to be written:
logic [$clog2(N_SOURCE)-1:0] src_sel; `ASSUME_FPV(IsrcRange_M, src_sel >= 0 && src_sel < N_SOURCE, clk_i, !rst_ni) `ASSUME_FPV(IsrcStable_M, ##1 $stable(src_sel), clk_i, !rst_ni) `ASSERT(LevelTriggeredIp_A, $rose(rv_plic.ip[src_sel]) |-> $past(rv_plic.le[src_sel]) || $past(intr_src_i[src_sel]), clk_i, !rst_ni)
Coverpoints are used for properties and corner cases that the designer wants to make sure are being exercised by the testbench (e.g. FIFO-full checks). The code coverage tool then reports the coverage percentage of these coverpoints together with the other cover metrics (such as line coverage and branch coverage).
The macro `COVER(name, prop, clk, rst) of prim_assert.sv can be used to add coverpoints to your design, where the cover property uses the same SVA syntax, operators, and system functions as the the assert properties.
If you have access to JasperGold from Cadence, you can formally verify your assertions. Before running FPV, please make sure the target has been added to one of the [three batch scripts]({{< relref “doc/getting_started/setup_formal.md#formal-property-verification-fpv” >}}).
For example, to run formal property verification (FPV) using JasperGold on the prim module prim_arbiter_fixed
, type:
$REPO_TOP/util/dvsim/dvsim.py $REPO_TOP/hw/top_earlgrey/formal/top_earlgrey_prim_fpv_cfgs.hjson --select-cfgs prim_arbiter_fixed_fpv
JasperGold will then report which assertions have been proven or disproven, and whether or not there are any unreachable assertions or coverpoints. Adding a --gui
option will open the JasperGold GUI.
To run formal property verification for all prim modules, type:
$REPO_TOP/util/dvsim/dvsim.py $REPO_TOP/hw/top_earlgrey/formal/top_earlgrey_prim_fpv_cfgs.hjson
If you have access to VC Formal from Synopsys, you can formally verify your assertions. For example, to run formal property verification (FPV) using VC Formal on module gpio
, type:
$REPO_TOP/util/dvsim/dvsim.py $REPO_TOP/hw/top_earlgrey/formal/top_earlgrey_prim_fpv_cfgs.hjson --select-cfgs prim_arbiter_fixed_fpv -t vcformal
VC Formal will then report which assertions have been proven or disproven, and whether or not there are any unreachable assertions or coverpoints. Adding a --gui
option will open the VCFormal GUI.
To run formal property verification for all prim modules, type:
$REPO_TOP/util/dvsim/dvsim.py $REPO_TOP/hw/top_earlgrey/formal/top_earlgrey_prim_fpv_cfgs.hjson -t vcformal
This script generates a report of all FPV runs. The report is printed at the end of the run, which lists the total number of assertions and the number of proven, vacuous, covered and failing assertions for each block. CRASH identifies modules that fail to run VC Formal.
Connectivity tests use formal method to exhaustively verify system-level connections, which are specified in a high-level format (for example: CSV format for JasperGold).
The dvsim
formal flow supports connectivity test. Each top-level can create its own connectivity setting with a customized Hjson file. For example, top_earlgrey
has hw/top_earlgrey/formal/chip_conn_cfgs.hjson
that specifies its top_level name, fusesoc_core file, and csv file path. You can trigger top_earlgrey's connectivity test using dvsim
:
util/dvsim/dvsim.py hw/top_earlgrey/formal/chip_conn_cfgs.hjson
Adding a --gui
option will open the JaperGold GUI.
A [security countermeasure verification framework]({{< relref “doc/ug/sec_cm_dv_framework” >}}) is implemented in design and fpv tcl script to verify common countermeasure primitives in a semi-automated way.
OpenTitan's security IP blocks have implemented assertions to check against common fault injections. These assertions ensure if the security prim module returns an error, a corresponding alert should fire immediately without any gating conditions. There are three pre-defined assertion macros under file hw/ip/prim/rtl/prim_assert_sec_cm.svh
:
prim_sparse_fsm_flop
returns state_o
value that is not one of the defined FSM states, which means the FSM state might be attacked, a fatal alert is expected to fire.prim_count
sets err_o
to 1, which means the two counters do not match, a fatal alert is expected to fire.prim_double_lfsr
sets err_o
to 1, which means two LFSR states do not match, a fatal alert is expected to fire. Note that assertions defined with these macros will have a common prefix name FpvSecCm
, which will help the FPV tcl file to group them in a specific task.The above security assertions are expected to be unreachable in normal design environment. They are only reachable if a fault is injected. To create a FPV environment that has fault injections, the stopat
command and black-box methods are used.
stopat
is placed at state_o
output.To set up the FPV security check environment, please follow the steps below:
hw/top_earlgrey/formal/top_earlgrey_sec_cm_fpv_cfgs.hjson
with the naming convention “{ip_name}_sec_cm”.FpvSecCm
.Here is an example on csrng module:
{ name: csrng_sec_cm dut: csrng fusesoc_core: lowrisc:dv:csrng_sva import_cfgs: ["{proj_root}/hw/formal/tools/dvsim/common_fpv_cfg.hjson"] rel_path: "hw/ip/csrng/{sub_flow}/{tool}" cov: false task: "FpvSecCm" stopats: ["*u_state_regs.state_o"] }
For assertions, it is preferred to use postfix _A
for assertions, _M
for assumptions, _P
for properties, and _S
for sequences. For example:
`ASSUME_FPV(IsrcRange_M, src_sel >= 0 && src_sel < N_SOURCE, clk_i, !rst_ni) `ASSERT(LevelTriggeredIp_A, $rose(rv_plic.ip[src_sel]) |-> $past(rv_plic.le[src_sel]) || $past(intr_src_i[src_sel]), clk_i, !rst_ni)
The recommended guidelines for where to implement assertions are as follows:
ip/hw/module_name/fpv/vip
folder. This FPV environment can be automatically generated by the fpvgen.py
script.ip/hw/submodule_or_interface/fpv/vip
folder. These portable assertion collections can be easily reused by other testbench via a bind file.