quasar/verif/LEC/formality_work/run_me.fms

# Set Search Path for Golden/Implementation Design
	set search_path "./verif/LEC ./verif/LEC/LEC_RTL/Golden_RTL ./verif/LEC/LEC_RTL/Imp_BB_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/Imp_BB_RTL/pkt.sv
 			$LEC_ROOT/LEC_RTL/Imp_BB_RTL/beh_lib.sv
 			$LEC_ROOT/LEC_RTL/Imp_BB_RTL/mem_lib.sv
 			$LEC_ROOT/LEC_RTL/Imp_BB_RTL/ifu_ic_mem.sv
 			$LEC_ROOT/LEC_RTL/Imp_BB_RTL/gated_latch.sv 
 			$LEC_ROOT/LEC_RTL/Imp_BB_RTL/ifu_iccm_mem.sv 
 			$LEC_ROOT/LEC_RTL/Imp_BB_RTL/lsu_dccm_mem.sv
 			$LEC_ROOT/LEC_RTL/Imp_BB_RTL/mem.sv   
 			$LEC_ROOT/LEC_RTL/Imp_BB_RTL/dmi_jtag_to_core_sync.sv 
 			$LEC_ROOT/LEC_RTL/Imp_BB_RTL/rvjtag_tap.sv
 			$LEC_ROOT/LEC_RTL/Imp_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_2.0.fms

 # Setting User Match on output ports
 	source $LEC_ROOT/setup_files/Output_ports_2.0.fms
 
 # Setting User Match on input Black Box Pins
	source $LEC_ROOT/setup_files/BB_input_pins_2.0.fms

 # Setting User Match on output Black Box Pins
	source $LEC_ROOT/setup_files/BB_output_pins_2.0.fms

 # Setting User Match on Flip Flops
 	source $LEC_ROOT/setup_files/DFF_2.0.fms
 
 # Setting up constants potentially constant registers 
 	source $LEC_ROOT/setup_files/Constant_2.0.fms

 # Setting up dont verify points 
 	source $LEC_ROOT/setup_files/Dont_verify_points_2.0.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