fm_mv.tcl

synopsys dc_shell 用户手册

#################################################################################
# Formality Verification Script for
# Design Compiler Top-Down Reference Methodology Script
# Script: fm.tcl
# Version: B-2008.09 (Oct. 3, 2008)
# Copyright (C) 2007, 2008 Synopsys All rights reserved.
#################################################################################

#################################################################################
# Shared setup with DC
#################################################################################

source -echo -verbose dc_setup.tcl

#################################################################################
# Synopsys Auto Setup Mode
#################################################################################

set synopsys_auto_setup true

# Note: The Synopsys Auto Setup mode is less conservative than the Formality default mode, 
# and is more likely to result in a successful verification out-of-the-box.
#
# Using the Setting this variable will change the default values of the variables listed here below
# You may change any of these variables back to their default settings to be more conservative.
# Uncomment the appropriate lines below to revert back to their default settings:

	# set hdlin_ignore_parallel_case true
	# set hdlin_ignore_full_case true
	# set verification_verify_directly_undriven_output true
	# set hdlin_ignore_embedded_configuration false
	# set svf_ignore_unqualified_fsm_information true

# Other variables with changed default values are described in the next few sections.

#################################################################################
# Setup for handling undriven signals in the design
#################################################################################

# The Synopsys Auto Setup mode sets undriven signals in the reference design to "0" similar to DC.
# Undriven signals in the implementation design are set to "X".
# Uncomment the next line to revert back to the more conservative default setting:

	# set verification_set_undriven_signals BINARY:X

#################################################################################
# Setup for simulation/synthesis mismatch messaging
#################################################################################

# The Synopsys Auto Setup mode will produce warning messages, not error messages,
# when Formality encounters potential differences between simulation and synthesis.
# Uncomment the next line to revert back to the more conservative default setting:

	# set hdlin_error_on_mismatch_message true

#################################################################################
# Setup for Clock-gating
#################################################################################

# The Synopsys Auto Setup mode, along with the SVF file, will appropriately set the clock-gating variable.
# Otherwise, the user will need to notify Formality of clock-gating by uncommenting the next line:

	# set verification_clock_gate_hold_mode any

#################################################################################
# Setup for instantiated DW or Function-inferred DW
#################################################################################

# Set this variable ONLY if your design contains instantiated DW or function-inferred DW

	#set hdlin_dwroot "" ;# Enter the pathname to the top-level of the DC tree

#################################################################################
# Setup for handling missing design modules
#################################################################################

# If the design has missing blocks or missing components in both the reference and implementation designs,
# uncomment the following variable so that Formality can complete linking each design:

	# set hdlin_unresolved_modules black_box

#################################################################################
# Read in the SVF file(s)
#################################################################################

# Set this variable to point to individual SVF file(s) or to a directory containing SVF files.

set_svf ${RESULTS_DIR}/${DESIGN_NAME}.mapped.svf

#################################################################################
# Read in the libraries
#################################################################################

foreach tech_lib "${TARGET_LIBRARY_FILES} ${ADDITIONAL_LINK_LIB_FILES}" {
  read_db -technology_library $tech_lib
}

#################################################################################
# Read in the Reference Design as verilog/vhdl source code
#################################################################################

#read_vhdl -r ${RTL_SOURCE_FILES} -work_library WORK

read_verilog -r $RTL_SOURCE_FILES -work_library WORK

# Note: If retention registers are instantiated in the RTL then replace the
#       technology retention register models here.  See the implementation read
#       section below for details.  This should be done before set_top.
#       Most designs do not have retention registers until after mapping so
#       this is not needed.

set_top r:/WORK/${DESIGN_NAME}

#################################################################################
# For a UPF MV flow, read in the UPF file for the Reference Design
#################################################################################

load_upf -r ${DESIGN_NAME}.upf

#################################################################################
# Read in the Implementation Design from DC-RM result
#
# Choose the format that is used in your flow
#################################################################################

# For Verilog
#read_verilog -i ./${RESULTS_DIR}/${DESIGN_NAME}.mapped.v

# OR

# For DDC
read_ddc -i ./${RESULTS_DIR}/${DESIGN_NAME}.mapped.ddc

# Note: Milkyway design format is not supported with UPF flow in Formality.

#################################################################################
# Read in Retention Register Simulation Models
#################################################################################

# If you are mapping to retention registers in your design, you need to replace the
# technology library models of those cells with Verilog simulation models for
# Formality verification.  Please see the following SolvNet article for details:

# https://solvnet.synopsys.com/retrieve/024106.html

# set_top should be run only after the retention register models have been replaced. 

set_top i:/WORK/${DESIGN_NAME}

#################################################################################
# For a UPF MV flow, read in the UPF file for the Implementation Design
#################################################################################

load_upf -i ${RESULTS_DIR}/${DESIGN_NAME}.mapped.upf

#################################################################################
# Configure constant ports
#
# When using the Synopsys Auto Setup mode, the SVF file will convey information
# automatically to Formality about how to disable scan.
#
# Otherwise, manually define those ports whose inputs should be assumed constant
# during verification.
#
# Example command format:
#
#   set_constant -type port i:/WORK/$DESIGN_NAME/<port_name> <constant_value> 
#
#################################################################################

match
report_unmatched_points > ${REPORTS_DIR}/${DESIGN_NAME}.fmv_unmatched_points.rpt

#################################################################################
# Verify and Report
#################################################################################
 
if { ![verify] }  {  
  save_session -replace ${REPORTS_DIR}/${DESIGN_NAME}
  report_failing_points > ${REPORTS_DIR}/${DESIGN_NAME}.fmv_failing_points.rpt
  report_aborted > ${REPORTS_DIR}/${DESIGN_NAME}.fmv_aborted_points.rpt
} 

exit