2026-04-27

Cadence Behavioral Property Sythesis

Setup

/var/home/brg8ve/cva6/vendor/pulp-platform/fpga-support/rtl/SyncDpRam.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/fpga-support/rtl/AsyncDpRam.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/fpga-support/rtl/AsyncThreePortRam.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/fpga-support/rtl/SyncThreePortRam.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/fpga-support/rtl/SyncDpRam_ind_r_w.sv 

+incdir+/var/home/brg8ve/cva6/core/include/ 
+incdir+/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/include/ 
+incdir+/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/ 
+incdir+/var/home/brg8ve/cva6/vendor/pulp-platform/axi/include/ 
+incdir+/var/home/brg8ve/cva6/common/local/util/ 

+incdir+/var/home/brg8ve/cva6/corev_apu/axi_node 
+incdir+/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/include/ 
+incdir+/var/home/brg8ve/cva6/vendor/pulp-platform/axi/include/ 
+incdir+/var/home/brg8ve/cva6/corev_apu/register_interface/include/ 
+incdir+/var/home/brg8ve/cva6/corev_apu/tb/common/ 
+incdir+/var/home/brg8ve/cva6/verif/core-v-verif/lib/uvm_agents/uvma_rvfi/ 
+incdir+/var/home/brg8ve/cva6/verif/core-v-verif/lib/uvm_components/uvmc_rvfi_reference_model/ 
+incdir+/var/home/brg8ve/cva6/verif/core-v-verif/lib/uvm_components/uvmc_rvfi_scoreboard/ 
+incdir+/var/home/brg8ve/cva6/verif/core-v-verif/lib/uvm_agents/uvma_core_cntrl/ 
+incdir+/var/home/brg8ve/cva6/verif/tb/core/ 
+incdir+/var/home/brg8ve/cva6/core/include/ 
+incdir+/var/home/brg8ve/cva6/tools/spike/include/disasm/ 
+incdir+/var/home/brg8ve/cva6/core/cvfpu/src/
+incdir+/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/

/var/home/brg8ve/cva6/core/cvfpu/src/common_cells/include/common_cells/registers.svh
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_pkg.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_cast_multi.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_classifier.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_divsqrt_multi.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_fma_multi.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_fma.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_noncomp.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_opgroup_block.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_opgroup_fmt_slice.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_opgroup_multifmt_slice.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_rounding.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_top.sv
/var/home/brg8ve/cva6/core/cvfpu/src/fpnew_divsqrt_th_64_multi.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpu_div_sqrt_mvp/hdl/defs_div_sqrt_mvp.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpu_div_sqrt_mvp/hdl/control_mvp.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpu_div_sqrt_mvp/hdl/div_sqrt_top_mvp.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpu_div_sqrt_mvp/hdl/iteration_div_sqrt_mvp.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpu_div_sqrt_mvp/hdl/norm_div_sqrt_mvp.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpu_div_sqrt_mvp/hdl/nrbd_nrsc_mvp.sv 
/var/home/brg8ve/cva6/core/cvfpu/src/fpu_div_sqrt_mvp/hdl/preprocess_mvp.sv 
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_top.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_ctrl.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_double.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_scalar_dp.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_prepare.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_srt.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_round.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_pack.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_srt_radix16_with_sqrt.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_ff1.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/vfdsu/rtl/ct_vfdsu_srt_radix16_bound_table.v
/var/home/brg8ve/cva6/core/cvfpu/vendor/openc910/C910_RTL_FACTORY/gen_rtl/clk/rtl/gated_clk_cell.v

/var/home/brg8ve/cva6/core/include/cvxif_types.svh    
/var/home/brg8ve/cva6/core/include/rvfi_types.svh 
/var/home/brg8ve/cva6/core/include/config_pkg.sv 
/var/home/brg8ve/cva6/core/include/cv64a6_imafdc_sv39_config_pkg.sv
/var/home/brg8ve/cva6/core/include/riscv_pkg.sv 
/var/home/brg8ve/cva6/core/include/ariane_pkg.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/axi/src/axi_pkg.sv 

/var/home/brg8ve/cva6/core/include/wt_cache_pkg.sv 
/var/home/brg8ve/cva6/core/include/std_cache_pkg.sv 
/var/home/brg8ve/cva6/core/include/instr_tracer_pkg.sv 
/var/home/brg8ve/cva6/core/include/build_config_pkg.sv 

/var/home/brg8ve/cva6/core/cvxif_compressed_if_driver.sv 
/var/home/brg8ve/cva6/core/cvxif_issue_register_commit_if_driver.sv 
/var/home/brg8ve/cva6/core/cvxif_example/include/cvxif_instr_pkg.sv 
/var/home/brg8ve/cva6/core/cvxif_fu.sv 
/var/home/brg8ve/cva6/core/cvxif_example/cvxif_example_coprocessor.sv 
/var/home/brg8ve/cva6/core/cvxif_example/instr_decoder.sv 
/var/home/brg8ve/cva6/core/cvxif_example/compressed_instr_decoder.sv 
/var/home/brg8ve/cva6/core/cvxif_example/copro_alu.sv 

/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/cf_math_pkg.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/fifo_v3.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/lfsr.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/lfsr_8bit.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/stream_arbiter.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/stream_arbiter_flushable.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/stream_mux.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/stream_demux.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/lzc.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/rr_arb_tree.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/shift_reg.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/unread.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/popcount.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/exp_backoff.sv 

/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/counter.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/common_cells/src/delta_counter.sv 

/var/home/brg8ve/cva6/core/cva6.sv 
/var/home/brg8ve/cva6/core/cva6_rvfi_probes.sv
/var/home/brg8ve/cva6/core/cva6_rvfi.sv 
/var/home/brg8ve/cva6/core/alu.sv 
/var/home/brg8ve/cva6/core/alu_wrapper.sv
/var/home/brg8ve/cva6/core/raw_checker.sv
/var/home/brg8ve/cva6/core/fpu_wrap.sv 
/var/home/brg8ve/cva6/core/branch_unit.sv 
/var/home/brg8ve/cva6/core/compressed_decoder.sv 
/var/home/brg8ve/cva6/core/macro_decoder.sv 
/var/home/brg8ve/cva6/core/controller.sv 
/var/home/brg8ve/cva6/core/zcmt_decoder.sv 
/var/home/brg8ve/cva6/core/csr_buffer.sv 
/var/home/brg8ve/cva6/core/csr_regfile.sv 
/var/home/brg8ve/cva6/core/decoder.sv 
/var/home/brg8ve/cva6/core/ex_stage.sv 
/var/home/brg8ve/cva6/core/instr_realign.sv 
/var/home/brg8ve/cva6/core/id_stage.sv 
/var/home/brg8ve/cva6/core/issue_read_operands.sv 
/var/home/brg8ve/cva6/core/issue_stage.sv 
/var/home/brg8ve/cva6/core/load_unit.sv 
/var/home/brg8ve/cva6/core/load_store_unit.sv 
/var/home/brg8ve/cva6/core/lsu_bypass.sv 
/var/home/brg8ve/cva6/core/mult.sv 
/var/home/brg8ve/cva6/core/multiplier.sv 
/var/home/brg8ve/cva6/core/serdiv.sv 
/var/home/brg8ve/cva6/core/perf_counters.sv 
/var/home/brg8ve/cva6/core/ariane_regfile_ff.sv 
/var/home/brg8ve/cva6/core/ariane_regfile_fpga.sv 
/var/home/brg8ve/cva6/core/scoreboard.sv 
/var/home/brg8ve/cva6/core/store_buffer.sv 
/var/home/brg8ve/cva6/core/amo_buffer.sv 
/var/home/brg8ve/cva6/core/store_unit.sv 
/var/home/brg8ve/cva6/core/commit_stage.sv 
/var/home/brg8ve/cva6/core/axi_shim.sv 
/var/home/brg8ve/cva6/core/cva6_accel_first_pass_decoder_stub.sv 
/var/home/brg8ve/cva6/core/acc_dispatcher.sv 
/var/home/brg8ve/cva6/core/cva6_fifo_v3.sv 

/var/home/brg8ve/cva6/core/frontend/btb.sv 
/var/home/brg8ve/cva6/core/frontend/bht.sv 
/var/home/brg8ve/cva6/core/frontend/bht2lvl.sv 
/var/home/brg8ve/cva6/core/frontend/ras.sv 
/var/home/brg8ve/cva6/core/frontend/instr_scan.sv 
/var/home/brg8ve/cva6/core/frontend/instr_queue.sv 
/var/home/brg8ve/cva6/core/frontend/frontend.sv 

/var/home/brg8ve/cva6/core/cache_subsystem/wt_dcache_ctrl.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/wt_dcache_mem.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/wt_dcache_missunit.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/wt_dcache_wbuffer.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/wt_dcache.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/cva6_icache.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/wt_cache_subsystem.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/wt_axi_adapter.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/tag_cmp.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/axi_adapter.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/miss_handler.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/cache_ctrl.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/cva6_icache_axi_wrapper.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/std_cache_subsystem.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/std_nbdcache.sv 
+incdir+/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/include 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_pkg.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/utils/hpdcache_mem_req_read_arbiter.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/utils/hpdcache_mem_req_write_arbiter.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_demux.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_lfsr.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_sync_buffer.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_fifo_reg.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_fifo_reg_initialized.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_fxarb.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_rrarb.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_mux.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_decoder.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_1hot_to_binary.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_prio_1hot_encoder.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_sram.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_sram_wbyteenable.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_sram_wmask.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_regbank_wbyteenable_1rw.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_regbank_wmask_1rw.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_data_downsize.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_data_upsize.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/hpdcache_data_resize.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hwpf_stride/hwpf_stride_pkg.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hwpf_stride/hwpf_stride.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hwpf_stride/hwpf_stride_arb.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hwpf_stride/hwpf_stride_wrapper.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_amo.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_cmo.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_core_arbiter.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_ctrl.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_ctrl_pe.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_memctrl.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_miss_handler.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_mshr.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_rtab.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_uncached.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_victim_plru.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_victim_random.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_victim_sel.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_wbuf.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/hpdcache_flush.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/utils/hpdcache_mem_resp_demux.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/utils/hpdcache_mem_to_axi_read.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/utils/hpdcache_mem_to_axi_write.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/cva6_hpdcache_subsystem.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/cva6_hpdcache_subsystem_axi_arbiter.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/cva6_hpdcache_if_adapter.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/cva6_hpdcache_wrapper.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/macros/behav/hpdcache_sram_1rw.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/macros/behav/hpdcache_sram_wbyteenable_1rw.sv 
/var/home/brg8ve/cva6/core/cache_subsystem/hpdcache/rtl/src/common/macros/behav/hpdcache_sram_wmask_1rw.sv 

+incdir+/var/home/brg8ve/cva6/core/pmp/include/
+incdir+/var/home/brg8ve/cva6/core/pmp/tb/
/var/home/brg8ve/cva6/core/pmp/src/pmp.sv 
/var/home/brg8ve/cva6/core/pmp/src/pmp_entry.sv 
/var/home/brg8ve/cva6/core/pmp/src/pmp_data_if.sv 

/var/home/brg8ve/cva6/common/local/util/instr_tracer.sv 
/var/home/brg8ve/cva6/common/local/util/tc_sram_wrapper.sv 
/var/home/brg8ve/cva6/common/local/util/tc_sram_wrapper_cache_techno.sv 
/var/home/brg8ve/cva6/vendor/pulp-platform/tech_cells_generic/src/rtl/tc_sram.sv 
/var/home/brg8ve/cva6/common/local/util/sram.sv 
/var/home/brg8ve/cva6/common/local/util/sram_cache.sv 

/var/home/brg8ve/cva6/core/cva6_mmu/cva6_mmu.sv 
/var/home/brg8ve/cva6/core/cva6_mmu/cva6_ptw.sv 
/var/home/brg8ve/cva6/core/cva6_mmu/cva6_tlb.sv 
/var/home/brg8ve/cva6/core/cva6_mmu/cva6_shared_tlb.sv

.tcl file used

#clear -all

analyze -sv -f cva6.f \
-bbox_m alu_wrapper\
-bbox_m fpu_wrap\
-bbox_m raw_checker\
-bbox_m fpnew_divsqrt_th_64_multi\
-bbox_m fpnew_opgroup_block\
-bbox_m aes

elaborate -top cva6

clock clk_i
reset !rst_ni

waveform -reset rst_ni==1'b1
check_bps -init


scope -extract all
#scope -extract module -top -clock clk_i -clock_edge posedge
#scope -extract counter -silent
#scope -extract fifo -silent
#scope -extract fsm -silent
#scope -extract onehot -silent

#set_scan_seek_mode all; set_scan_seek_depth 1;
#set_scan_trace_stuck_at_values_limit 2; set_waveform_import_multiple_segments off; set_scan_verbosity 0;

check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_00.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_01.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_02.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_03.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_04.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_05.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_06.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_07.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_08.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_09.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_10.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_11.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_12.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_13.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_14.vcd  -hier_path "TOP.ariane_testharness.i_ariane"
check_bps -scan -trace -vcd /net/marysrock.ece.Virginia.EDU/maryisan/users/brg8ve/scratch/cva6_traces/program_15.vcd  -hier_path "TOP.ariane_testharness.i_ariane"

check_bps -export -class unclassified

prove -all

export -bps -to_sva [get_proj_dir]/example.sva \
	-to_tcl [get_proj_dir]/connect_sva.tcl \
       	-type coverage_hole -type exercised_cover \
       	-class certified -class unclassified

export -bps -to_html [get_proj_dir]/example.htm \
	-type coverage_hole -type exercised_cover \
	-class certified -class unclassified

Cadence’s own example

They have a non-trivial toy design of considerable size.
Running BPS on this results in 21 assertions and 134 covers.

==============================================================
SUMMARY
==============================================================
           Total Tasks                        : 2
           Total Properties                   : 155
                 assumptions                  : 0
                  - approved                  : 0
                  - temporary                 : 0
                 soft assumptions             : 0
                 assertions                   : 21
                  - proven                    : 21 (100%)
                  - bounded_proven (user)     : 0 (0%)
                  - bounded_proven (auto)     : 0 (0%)
                  - marked_proven             : 0 (0%)
                  - cex                       : 0 (0%)
                  - ar_cex                    : 0 (0%)
                  - undetermined              : 0 (0%)
                  - unknown                   : 0 (0%)
                  - error                     : 0 (0%)
                 covers                       : 134
                  - unreachable               : 1 (0.746269%)
                  - bounded_unreachable (user): 0 (0%)
                  - covered                   : 133 (99.2537%)
                - ar_covered                : 0 (0%)
                  - undetermined              : 0 (0%)
                  - unknown                   : 0 (0%)
                  - error                     : 0 (0%)

The tools seems to be heavily skewed towards generating covers
All the assertions were proved.

CVA6

Extracting POIs

I tried to extract the FSM, counters, One shot, fifos in the design
Extracting One-Shots took a considerable amount of time
BPS was only able to generate 28 properties from this

Extracting just the top module

Next I turned off the POIs and asked it to extract all the signals from the top module alone

==============================================================
SUMMARY
==============================================================
	   Total Tasks                        : 2
	   Total Properties                   : 226
			 assumptions                  : 0
			  - approved                  : 0
			  - temporary                 : 0
			 soft assumptions             : 0
			 assertions                   : 5
			  - proven                    : 0 (0%)
			  - bounded_proven (user)     : 0 (0%)
			  - bounded_proven (auto)     : 0 (0%)
			  - marked_proven             : 0 (0%)
			  - cex                       : 5 (100%)
			  - ar_cex                    : 0 (0%)
			  - undetermined              : 0 (0%)
			  - unknown                   : 0 (0%)
			  - error                     : 0 (0%)
			 covers                       : 221
			  - unreachable               : 16 (7.23982%)
			  - bounded_unreachable (user): 0 (0%)
			  - covered                   : 205 (92.7602%)
			  - ar_covered                : 0 (0%)
			  - undetermined              : 0 (0%)
			  - unknown                   : 0 (0%)
			  - error                     : 0 (0%)

It seems to be able to generate covers pretty well