quasar/verif/LEC/formality_work/run_me.fms

127 lines
4.0 KiB
Plaintext
Executable File

# Set Search Path for Golden/Implementation Design
set search_path "./verif/LEC ./verif/LEC/LEC_RTL/Golden_RTL ./verif/LEC/LEC_RTL/generated_rtl"
# Set LEC_ROOT to presentt working directory
set LEC_ROOT [pwd]/verif/LEC
# Set formality path to refference design
set fm_path_r $LEC_ROOT/LEC_RTL/Golden_RTL
# Synopsis Auto Setup
set synopsys_auto_setup true
set_host_options -max_cores 8
if {![file isdirectory $fm_path_r]} {
puts "ERROR: path is not valid"
exit
} else {
# Loading verilog reference file
read_sverilog -r "
$fm_path_r/design/lib/el2_lib.sv
$fm_path_r/design/lib/beh_lib.sv
$fm_path_r/design/lib/mem_lib.sv
$fm_path_r/design/include/pkt.sv
$fm_path_r/design/el2_swerv_wrapper.sv
$fm_path_r/design/el2_mem.sv
$fm_path_r/design/el2_pic_ctrl.sv
$fm_path_r/design/el2_swerv.sv
$fm_path_r/design/el2_dma_ctrl.sv
$fm_path_r/design/ifu/el2_ifu_aln_ctl.sv
$fm_path_r/design/ifu/el2_ifu_compress_ctl.sv
$fm_path_r/design/ifu/el2_ifu_ifc_ctl.sv
$fm_path_r/design/ifu/el2_ifu_bp_ctl.sv
$fm_path_r/design/ifu/el2_ifu_ic_mem.sv
$fm_path_r/design/ifu/el2_ifu_mem_ctl.sv
$fm_path_r/design/ifu/el2_ifu_iccm_mem.sv
$fm_path_r/design/ifu/el2_ifu.sv
$fm_path_r/design/dec/el2_dec_decode_ctl.sv
$fm_path_r/design/dec/el2_dec_gpr_ctl.sv
$fm_path_r/design/dec/el2_dec_ib_ctl.sv
$fm_path_r/design/dec/el2_dec_tlu_ctl.sv
$fm_path_r/design/dec/el2_dec_trigger.sv
$fm_path_r/design/dec/el2_dec.sv
$fm_path_r/design/exu/el2_exu_alu_ctl.sv
$fm_path_r/design/exu/el2_exu_mul_ctl.sv
$fm_path_r/design/exu/el2_exu_div_ctl.sv
$fm_path_r/design/exu/el2_exu.sv
$fm_path_r/design/lsu/el2_lsu.sv
$fm_path_r/design/lsu/el2_lsu_clkdomain.sv
$fm_path_r/design/lsu/el2_lsu_addrcheck.sv
$fm_path_r/design/lsu/el2_lsu_lsc_ctl.sv
$fm_path_r/design/lsu/el2_lsu_stbuf.sv
$fm_path_r/design/lsu/el2_lsu_bus_buffer.sv
$fm_path_r/design/lsu/el2_lsu_bus_intf.sv
$fm_path_r/design/lsu/el2_lsu_ecc.sv
$fm_path_r/design/lsu/el2_lsu_dccm_mem.sv
$fm_path_r/design/lsu/el2_lsu_dccm_ctl.sv
$fm_path_r/design/lsu/el2_lsu_trigger.sv
$fm_path_r/design/dbg/el2_dbg.sv
$fm_path_r/design/dmi/rvjtag_tap.v
$fm_path_r/design/dmi/dmi_jtag_to_core_sync.v
$fm_path_r/design/dmi/dmi_wrapper.v
"
# Setting top reference design
set_top r:/WORK/el2_swerv_wrapper
}
# Loading verilog implementation file
read_sverilog -i " \
$LEC_ROOT/LEC_RTL/BB_RTL/pkt.sv
$LEC_ROOT/LEC_RTL/BB_RTL/beh_lib.sv
$LEC_ROOT/LEC_RTL/BB_RTL/mem_lib.sv
$LEC_ROOT/LEC_RTL/BB_RTL/ifu_ic_mem.sv
$LEC_ROOT/LEC_RTL/BB_RTL/gated_latch.sv
$LEC_ROOT/LEC_RTL/BB_RTL/ifu_iccm_mem.sv
$LEC_ROOT/LEC_RTL/BB_RTL/lsu_dccm_mem.sv
$LEC_ROOT/LEC_RTL/BB_RTL/mem.sv
$LEC_ROOT/LEC_RTL/BB_RTL/dmi_jtag_to_core_sync.sv
$LEC_ROOT/LEC_RTL/BB_RTL/rvjtag_tap.sv
$LEC_ROOT/LEC_RTL/BB_RTL/dmi_wrapper.sv
./generated_rtl/quasar_wrapper.sv
"
# Setting top implementation design
set_top i:/WORK/quasar_wrapper
# Setting Black Boxes on Memories
set_black_box r:/WORK/el2_mem
set_black_box i:/WORK/mem_DCCM_BANK_BITS*
# Setting User Match on input ports
source $LEC_ROOT/setup_files/Input_ports_1.3.fms
# Setting User Match on output ports
source $LEC_ROOT/setup_files/Output_ports_1.3.fms
# Setting User Match on input Black Box Pins
source $LEC_ROOT/setup_files/BB_input_pins_1.3.fms
# Setting User Match on output Black Box Pins
source $LEC_ROOT/setup_files/BB_output_pins_1.3.fms
# Setting User Match on Flip Flops
source $LEC_ROOT/setup_files/DFF_1.3.fms
# Setting up constants potentially constant registers
source $LEC_ROOT/setup_files/Constant_1.3.fms
# Setting up dont verify points
source $LEC_ROOT/setup_files/Dont_verify_points_1.3.fms
if {[verify] != 1} {
set verification_failing_points_limit 500
start_gui &
}
# Save Current Session
save_session -replace $LEC_ROOT/LEC_PASSED.fss
# Toal Elapsed Time in Seconds
elapsed_time
exit