[fpv] Adding VC Formal support to the script and document Signed-off-by: Will Chen <haihui@synopsys.com>
diff --git a/doc/ug/dv_methodology.md b/doc/ug/dv_methodology.md index 7157ed2..3ce4e3b 100644 --- a/doc/ug/dv_methodology.md +++ b/doc/ug/dv_methodology.md
@@ -22,6 +22,7 @@ For professional tooling, the team has chosen [Synopsys' VCS](https://www.synopsys.com/verification/simulation/vcs.html) as the simulator of choice with respect to the tracking of verification completeness and [JasperGold](https://www.cadence.com/content/cadence-www/global/en_US/home/tools/system-design-and-verification/formal-and-static-verification/jasper-gold-verification-platform.html) for FPV. Wherever possible we attempt to remain tool-agnostic, but we must choose a simulator as our ground truth for our own confidence of signoff-level assurances. +Likewise, for FPV, [Synopsys VC Formal](https://www.synopsys.com/verification/static-and-formal-verification/vc-formal.html) is also supported within the same flow, and can be used by those with access to VC Formal licenses. At this time there is also some support for Cadence's Xcelium, for those organizations which have few Synopsys VCS licenses. However support is not as mature as for VCS, which remains the tool for signoff. Furthermore, as a project we promote other open source verification methodologies - Verilator, Yosys, cocoTB, etc - and work towards a future where these are signoff-grade.
diff --git a/hw/formal/README.md b/hw/formal/README.md index b89f624..5fb7e70 100644 --- a/hw/formal/README.md +++ b/hw/formal/README.md
@@ -252,8 +252,9 @@ property uses the same SVA syntax, operators, and system functions as the the assert properties. -## How To Run JasperGold +## How To Run FPV on OpenTitan +### Cadence JapserGold If you have access to JasperGold from Cadence, you can formally verify your assertions. For example, to run formal property verification (FPV) using JasperGold on module `gpio`, type: @@ -301,6 +302,31 @@ ... ``` +## How To Run VC Formal + +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: +``` + cd hw/formal + fpv gpio +``` +VC Formal will then report which assertions have been proven or disproven, +and whether or not there are any unreachable assertions or coverpoints. + +To run formal property verification for all modules, type: +``` + cd hw/formal + fpv_all +``` +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. + +... +``` + ## Naming Convenctions For assertions, it is preferred to use postfix `_A` for assertions, `_M` for assumptions, `_P` for properties, and `_S` for sequences.
diff --git a/hw/formal/fpv_vcf.tcl b/hw/formal/fpv_vcf.tcl new file mode 100644 index 0000000..6674676 --- /dev/null +++ b/hw/formal/fpv_vcf.tcl
@@ -0,0 +1,164 @@ +# Copyright lowRISC contributors. +# Licensed under the Apache License, Version 2.0, see LICENSE for details. +# SPDX-License-Identifier: Apache-2.0 + +# This script has commands to run the design using VC Formal + +#------------------------------------------------------------------------- +# Analysing and elaborating the design +#------------------------------------------------------------------------- +# only one scr file exists in this folder + +analyze -format sverilog \ + -vcs "+define+FPV_ON -assert svaext \ + +define+INC_ASSERT \ + -f [glob *.scr]" + +elaborate -sva $env(FPV_TOP) + +#------------------------------------------------------------------------- +# Specify clock(s) and reset(s) +#------------------------------------------------------------------------- +# specify the primary clocks and resets in the design. +# use "-period" option with "create_clock" to specify the period +# use "-sense low/high" option with "create_reset" to specify active low or high reset respectively +# +# note: the TL-UL protocol checker tlul_assert.sv operates on the negedge clock + +if {$env(FPV_TOP) == "rv_dm"} { + create_clock clk_i -period 100 + create_clock tck_i -period 100 + create_reset rst_ni -sense low + create_reset trst_ni -sense low +} elseif {$env(FPV_TOP) == "spi_device"} { + create_clock clk_i -period 100 + create_clock cio_sck_i -period 100 + create_reset rst_ni -sense low + create_reset cio_csb_i -sense high +} elseif {$env(FPV_TOP) == "usb_fs_nb_pe"} { + create_clock clk_48mhz_i -period 100 + create_reset rst_ni -sense low +} elseif {$env(FPV_TOP) == "usbuart"} { + create_clock clk_i -period 100 + create_clock clk_48mhz_i -period 100 + create_reset rst_ni -sense low +} elseif {$env(FPV_TOP) == "usbdev"} { + create_clock clk_i -period 100 + create_clock clk_usb_48mhz_i -period 100 + create_reset rst_ni -sense low +} elseif {$env(FPV_TOP) == "top_earlgrey"} { + create_clock clk_i -period 100 + create_clock jtag_tck_i -period 100 + create_reset rst_ni -sense low + create_reset jtag_trst_ni -sense low +} elseif {$env(FPV_TOP) == "xbar_main"} { + create_clock clk_main_i -period 100 + create_reset rst_main_ni -sense low +} else { + create_clock clk_i -period 100 + create_reset rst_ni -sense low +} + +#------------------------------------------------------------------------- +# Assume properties for inputs +#------------------------------------------------------------------------- + +# For sram2tlul, input tl_i.a_ready is constrained by below asssertion +fvassume sram2tlul.validNotReady* + +# Input scanmode_i should not be X +fvassume *.scanmodeKnown + +#------------------------------------------------------------------------- +# TODO: eventually remove below assert disable lines +# To reduce prohibitive runtimes, below assertions are simply turned off for now +#------------------------------------------------------------------------- + +# spi_device +fvdisable {*spi_device.u_tlul2sram.tlul_assert_host.responseSize*} +fvdisable {*spi_device.u_tlul2sram.tlul_assert_host.onlyOnePendingReq*} +fvdisable {*spi_device.tlul_assert_host.responseMustHaveReq*} +fvdisable {*spi_device.tlul_assert_host.checkResponseOpcode*} +fvdisable {*spi_device.u_reg.tlul_assert_host.responseMustHaveReq*} +fvdisable {*spi_device.u_reg.tlul_assert_host.checkResponseOpcode*} +fvdisable {*spi_device.u_reg.u_socket.tlul_assert_host.responseMustHaveReq*} +fvdisable {*spi_device.u_reg.u_socket.tlul_assert_host.checkResponseOpcode*} +fvdisable {*spi_device.u_reg.u_socket.tlul_assert_device.gen_assert*.tlul_assert.responseSize*} +fvdisable {*spi_device.u_reg.u_socket.tlul_assert_device.gen_assert*.tlul_assert.onlyOnePendingReq*} +fvdisable {*spi_device.u_reg.u_socket.tlul_assert_host.responseSizeMustEqualReq*} +fvdisable {*spi_device.tlul_assert_host.responseSizeMustEqualReq*} + +# hmac +fvdisable {*hmac.u_tlul_adapter.tlul_assert_host.onlyOnePendingReq*} +fvdisable {*hmac.u_reg.u_socket.tlul_assert_device.gen_assert[0]*onlyOnePendingReq*} + +# flash_ctrl +fvdisable {*flash_ctrl.tlul_assert_host.response*Must*} +fvdisable {*flash_ctrl.u_reg.u_socket.tlul_assert_*.response*Must*} +fvdisable {*flash_ctrl.u_reg.u_socket.tlul_assert_device.gen_assert*.tlul_assert.onlyOnePendingReq*} + +# xbar +fvdisable {*xbar_main.tlul_assert_device_*.sizeMatches*} +fvdisable {*xbar_main.tlul_assert_device_*.legalA*} +fvdisable {*xbar_main.tlul_assert_device_*.addressAligned*} +fvdisable {*xbar_main.tlul_assert_device_*.maskMustBeCont*} +fvdisable {*xbar_main.tlul_assert_host_*.legal*} +fvdisable {*xbar_main.u_*.tlul_assert_host.legalDParam*} +fvdisable {*xbar_main.u_*.tlul_assert_device.response*} +fvdisable {*xbar_main.u_*.tlul_assert_device.legalA*} +fvdisable {*xbar_main.u_*.tlul_assert_device.addressAligned*} +fvdisable {*xbar_main.u_*.tlul_assert_device.checkResponseOp*} +fvdisable {*xbar_main.u_*.tlul_assert_device.maskMustBeCont*} +fvdisable {*xbar_main.u_*.tlul_assert_device.sizeMatches*} +fvdisable {*xbar_main.u_*.tlul_assert_*.gen_assert*.tlul_assert.maskMustBeCont*} +fvdisable {*xbar_main.u_*.tlul_assert_*.gen_assert*.tlul_assert.addressAlignedToSize*} +fvdisable {*xbar_main.u_*.tlul_assert_*.gen_assert*.tlul_assert.legal*} +fvdisable {*xbar_main.u_*.tlul_assert_*.gen_assert*.tlul_assert.sizeMatches*} + +# top_earlgrey +fvdisable {top_earlgrey.*addressAligned*} +fvdisable {top_earlgrey.*tlul_assert*Must*} +fvdisable {top_earlgrey.*onlyOne*} +fvdisable {top_earlgrey.*Response*} +fvdisable {top_earlgrey.*legal*} +fvdisable {top_earlgrey.u_xbar_main.u_sm1_*.rspIdInRange} +fvdisable {top_earlgrey.u_xbar_main.*depthShall*} +fvdisable {top_earlgrey.u_xbar_main.*tlul_assert*DataKnown*} +fvdisable {top_earlgrey.u_dm_top.*tlul_assert_*DataKnown*} + +#------------------------------------------------------------------------- +# Configure grid usage +#------------------------------------------------------------------------- +# Use "set_grid_usage" option to launch the run on the grid. +# Use option "-type <LSF|RTDA|SGE>=<# of workers>" to specify the type of grid and the numbers of workers +# "-control {<submission commands>} is used to specify the exact qsub/bsub string to use for accessing the grid resources +# Ex: set_grid_usage -type sge=12 -control { qsub -P <machine name> } +set_grid_usage -type RSH=12 + +#------------------------------------------------------------------------- +# Run all the assertion and cover properties +#------------------------------------------------------------------------- +# time limit set to 2 hours +set_fml_var fml_max_time 2H + +# initialize the design +sim_run -stable +sim_save_reset + +check_fv -block + +#------------------------------------------------------------------------- +# Report +#------------------------------------------------------------------------- +# to generate detailed report add "-verbose" option to "report_fv" +# Ex: report_fv -verbose > ../../../$env(FPV_TOP)_verbose.result +report_fv > ../../../$env(FPV_TOP).result + +#------------------------------------------------------------------------- +# Generate Formal Coverage +#------------------------------------------------------------------------- +# VC Formal also provides formal coverage metrics as part of formal signoff flow. +# If you would like to generate formal coverage or need any other help, please send email to vcf_support@synopsys.com + +quit +