| # 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 \ |
| -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 |
