Jasper® Apps Behavioral Property SynthesisReport

module: ariane create date: May 09 15:27:29 EDT 2026 filter: class in ( unclassified ) and rank = high and type in ( assert ) and progress state in ( new, hole, covered, covered_now_hole, assert, violated, certified_hole, certified_assert )

DESIGN INFORMATION SUMMARY:

Flops	1668 (22383) (0 property flop bits)	RTL Lines	23908
Latches	7 (256)	RTL Instances	233
Gates	46994 (422353)	Embedded Assumptions	0
Nets	50153	Embedded Assertions	0
Ports	10	Embedded Covers	0

PROPERTY SYNTHESIS SUMMARY:

POI Type	Number of POIs	Exercised Behaviors	Coverage Holes
User-defined	1	875	0

POI#	Signals
User-defined
	Classification	Type	Status	Property
1	i_frontend.bht_prediction[0].taken , i_frontend.bht_prediction[0].valid , i_frontend.bht_prediction[1].taken , i_frontend.bht_prediction[1].valid , i_frontend.bht_prediction_shifted[0].taken , i_frontend.bht_prediction_shifted[0].valid , i_frontend.bht_prediction_shifted[1].taken , ...
	unclassified	assert	cex	i_frontend.bht_prediction[0].taken \|=> i_frontend.i_ras.data_o.valid
	unclassified	assert	cex	i_frontend.bht_prediction[0].taken \|=> i_frontend.i_ras.stack_d[0].valid
	unclassified	assert	cex	i_frontend.bht_prediction[0].taken \|=> i_frontend.i_ras.stack_q[0].valid
	unclassified	assert	cex	i_frontend.bht_prediction[0].taken \|=> i_frontend.ras_predict.valid
	unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.branch_empty
	unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.ready_o
	unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.icache_dreq_o.req
	unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.instr_queue_ready
	unclassified	assert	cex	i_frontend.bp_valid \|=> i_frontend.i_instr_queue.branch_empty
	unclassified	assert	cex	i_frontend.bp_valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
	unclassified	assert	cex	i_frontend.bp_valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
	unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.branch_empty
	unclassified	assert	proven	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
	unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
	unclassified	assert	proven	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
	unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
	unclassified	assert	proven	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.idx_ds_d[0]
	unclassified	assert	proven	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.idx_ds_q[0]
	unclassified	assert	proven	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
	unclassified	assert	proven	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
	unclassified	assert	proven	i_frontend.btb_update.valid \|=> i_frontend.i_instr_queue.ready_o
	unclassified	assert	proven	i_frontend.btb_update.valid \|=> i_frontend.icache_dreq_o.req
	unclassified	assert	proven	i_frontend.btb_update.valid \|=> i_frontend.instr_queue_ready
	unclassified	assert	cex	i_frontend.debug_mode_i \|=> i_frontend.i_instr_queue.ready_o
	unclassified	assert	cex	i_frontend.debug_mode_i \|=> i_frontend.icache_dreq_o.req
	unclassified	assert	cex	i_frontend.debug_mode_i \|=> i_frontend.instr_queue_ready
	unclassified	assert	cex	i_frontend.eret_i \|=> i_frontend.i_instr_queue.branch_empty
	unclassified	assert	proven	i_frontend.eret_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
	unclassified	assert	cex	i_frontend.eret_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
	unclassified	assert	proven	i_frontend.eret_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
	unclassified	assert	cex	i_frontend.eret_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
	unclassified	assert	proven	i_frontend.eret_i \|=> i_frontend.i_instr_queue.idx_ds_d[0]
	unclassified	assert	proven	i_frontend.eret_i \|=> i_frontend.i_instr_queue.idx_ds_q[0]
	unclassified	assert	proven	i_frontend.eret_i \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
	unclassified	assert	proven	i_frontend.eret_i \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
	unclassified	assert	proven	i_frontend.eret_i \|=> i_frontend.i_instr_queue.ready_o
	unclassified	assert	proven	i_frontend.eret_i \|=> i_frontend.icache_dreq_o.req
	unclassified	assert	proven	i_frontend.eret_i \|=> i_frontend.instr_queue_ready
	unclassified	assert	cex	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.branch_empty
	unclassified	assert	proven	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
	unclassified	assert	cex	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
	unclassified	assert	proven	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
	unclassified	assert	cex	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
	unclassified	assert	proven	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.idx_ds_d[0]
	unclassified	assert	proven	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.idx_ds_q[0]
	unclassified	assert	proven	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
	unclassified	assert	proven	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
	unclassified	assert	proven	i_frontend.ex_valid_i \|=> i_frontend.i_instr_queue.ready_o
	unclassified	assert	proven	i_frontend.ex_valid_i \|=> i_frontend.icache_dreq_o.req
	unclassified	assert	proven	i_frontend.ex_valid_i \|=> i_frontend.instr_queue_ready
	unclassified	assert	cex	i_frontend.flush_i \|=> i_frontend.i_instr_queue.branch_empty
	unclassified	assert	proven	i_frontend.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
	unclassified	assert	cex	i_frontend.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
	unclassified	assert	proven	i_frontend.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
	unclassified	assert	cex	i_frontend.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
	unclassified	assert	proven	i_frontend.flush_i \|=> i_frontend.i_instr_queue.idx_ds_d[0]
	unclassified	assert	proven	i_frontend.flush_i \|=> i_frontend.i_instr_queue.idx_ds_q[0]
	unclassified	assert	proven	i_frontend.flush_i \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
	unclassified	assert	proven	i_frontend.flush_i \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
	unclassified	assert	proven	i_frontend.flush_i \|=> i_frontend.i_instr_queue.ready_o
	unclassified	assert	proven	i_frontend.flush_i \|=> i_frontend.icache_dreq_o.req
	unclassified	assert	proven	i_frontend.flush_i \|=> i_frontend.instr_queue_ready
	unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_branch_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_branch_o \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_branch_o \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_branch_o \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_branch_o \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_realign.unaligned_d
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_call_o \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_realign.unaligned_d
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jalr_o \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jr_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_return_o \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_return_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_return_o \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.btb_prediction[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.btb_prediction_shifted[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_btb.btb_prediction_o[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_realign.unaligned_d
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.i_instr_realign.valid_i
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.icache_dreq_i.ready
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.icache_dreq_i.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.icache_valid_q
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.if_ready
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jalr_o \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.is_jal_r \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[0]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_branch_o \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.instr_queue_usage[0][1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.instr_queue_usage[1][1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_call_o \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.instr_queue_usage[0][1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.instr_queue_usage[1][1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jalr_o \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jr_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jump_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jump_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jump_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jump_o \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jump_o \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jump_o \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jump_o \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jump_o \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jump_o \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.gen_instr_scan[1].i_instr_scan.rvc_return_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_bht.bht_prediction_o[0].taken \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.i_bht.bht_prediction_o[0].taken \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.i_bht.bht_prediction_o[0].taken \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.i_bht.bht_prediction_o[0].taken \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.i_bht.debug_mode_i \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.i_bht.debug_mode_i \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.i_bht.debug_mode_i \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	proven	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	proven	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	proven	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	proven	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	proven	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.i_btb.debug_mode_i \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.i_btb.debug_mode_i \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.i_btb.debug_mode_i \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	proven	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	proven	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	proven	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	proven	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	proven	i_frontend.i_instr_queue.flush_i \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.i_instr_queue.flush_i \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.i_instr_queue.flush_i \|=> i_frontend.instr_queue_ready
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.flush_i \|=> i_frontend.instr_queue_ready
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.flush_i \|=> i_frontend.instr_queue_ready
unclassified	assert	proven	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.pop_i \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	proven	i_frontend.i_instr_queue.idx_ds_d[0] \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow \|=> i_frontend.icache_dreq_i.ready
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[0] \|=> i_frontend.icache_dreq_i.ready
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.instr_overflow_fifo[1] \|=> i_frontend.icache_dreq_i.ready
unclassified	assert	proven	i_frontend.i_instr_queue.instr_queue_empty[0] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.i_instr_queue.instr_queue_empty[0] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.i_instr_queue.instr_queue_empty[0] \|=> i_frontend.instr_queue_ready
unclassified	assert	proven	i_frontend.i_instr_queue.instr_queue_empty[1] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.i_instr_queue.instr_queue_empty[1] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.i_instr_queue.instr_queue_empty[1] \|=> i_frontend.instr_queue_ready
unclassified	assert	proven	i_frontend.i_instr_queue.pop_instr[1] \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.i_instr_queue.replay_o \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.replay_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.replay_o \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.replay_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.replay_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.replay_o \|=> i_frontend.icache_dreq_i.ready
unclassified	assert	cex	i_frontend.i_instr_queue.taken[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.taken[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.taken[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.taken[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.taken[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.taken[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.taken[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.taken[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_realign.flush_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_realign.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_realign.flush_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_ras.pop_i \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_ras.pop_i \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.i_ras.pop_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_ras.pop_i \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_ras.pop_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_ras.pop_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_ras.push_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	proven	i_frontend.i_ras.push_i \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.i_ras.push_i \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	proven	i_frontend.i_ras.push_i \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	proven	i_frontend.i_ras.push_i \|=> i_frontend.ras_predict.valid
unclassified	assert	proven	i_frontend.i_ras.stack_d[0].valid \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	proven	i_frontend.i_ras.stack_d[0].valid \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	proven	i_frontend.i_ras.stack_d[0].valid \|=> i_frontend.ras_predict.valid
unclassified	assert	proven	i_frontend.i_ras.stack_d[1].valid \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	proven	i_frontend.i_ras.stack_d[1].valid \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	proven	i_frontend.i_ras.stack_d[1].valid \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	proven	i_frontend.i_ras.stack_d[1].valid \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	proven	i_frontend.i_ras.stack_d[1].valid \|=> i_frontend.ras_predict.valid
unclassified	assert	proven	i_frontend.i_ras.stack_q[1].valid \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.i_ras.stack_q[1].valid \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	proven	i_frontend.i_ras.stack_q[1].valid \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	proven	i_frontend.i_ras.stack_q[1].valid \|=> i_frontend.ras_predict.valid
unclassified	assert	proven	i_frontend.icache_dreq_i.valid \|=> i_frontend.i_instr_realign.valid_i
unclassified	assert	proven	i_frontend.icache_dreq_i.valid \|=> i_frontend.icache_valid_q
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s1 \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s1 \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s1 \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s2 \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s2 \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s2 \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[0]
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.idx_is_d
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.instr_queue_usage[0][1]
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.is_branch[1] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.is_call[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_call[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_call[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_call[0] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.is_call[0] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.is_call[0] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.is_call[0] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_instr_queue.instr_queue_usage[0][1]
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_instr_queue.instr_queue_usage[1][1]
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.is_call[1] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.read_pointer_n[0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.read_pointer_n[1]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.read_pointer_q[0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.read_pointer_q[1]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.read_pointer_n[1]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.read_pointer_q[1]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_n[0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.idx_ds_q[1]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.idx_is_q
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.is_jump[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_jump[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_jump[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.is_jump[1] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	proven	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	proven	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	proven	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	proven	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	proven	i_frontend.is_mispredict \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.is_mispredict \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.is_mispredict \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_jal_r
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jr_o
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.rvc_return_o
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.rvc_jr[0]
unclassified	assert	cex	i_frontend.is_return[0] \|=> i_frontend.rvc_return[0]
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.gen_instr_scan[1].i_instr_scan.is_jal_r
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.gen_instr_scan[1].i_instr_scan.rvc_jr_o
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.gen_instr_scan[1].i_instr_scan.rvc_return_o
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.rvc_jr[1]
unclassified	assert	cex	i_frontend.is_return[1] \|=> i_frontend.rvc_return[1]
unclassified	assert	cex	i_frontend.npc_rst_load_q \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	proven	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	proven	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	proven	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	proven	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	proven	i_frontend.npc_rst_load_q \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.npc_rst_load_q \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.npc_rst_load_q \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.ras_pop \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.ras_pop \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.ras_pop \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.ras_pop \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.ras_pop \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.ras_pop \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.ras_push \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	proven	i_frontend.ras_push \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.ras_push \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	proven	i_frontend.ras_push \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	proven	i_frontend.ras_push \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.replay \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.replay \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.replay \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.replay \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.replay \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.replay \|=> i_frontend.icache_dreq_i.ready
unclassified	assert	cex	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	proven	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	proven	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	proven	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	proven	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	proven	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	proven	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	proven	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.icache_dreq_o.req
unclassified	assert	proven	i_frontend.resolved_branch_i.is_mispredict \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.rvc_branch[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvc_branch[0] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.rvc_branch[0] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.rvc_branch[0] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.rvc_branch[0] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[0]
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.rvc_branch[1] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_instr_realign.unaligned_d
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.rvc_call[0] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_instr_queue.instr_queue_usage[0][1]
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_instr_queue.instr_queue_usage[1][1]
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.rvc_call[1] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_instr_realign.unaligned_d
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.rvc_jalr[0] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.usage_o[1]
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_instr_queue.instr_queue_usage[0][1]
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_instr_queue.instr_queue_usage[1][1]
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.rvc_jalr[1] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.rvc_jr[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvc_jr[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvc_jump[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvc_jump[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.rvc_jump[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.rvc_jump[1] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.rvc_jump[1] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.rvc_jump[1] \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.rvc_jump[1] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.rvc_jump[1] \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.rvc_jump[1] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.rvc_return[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.rvc_return[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvc_return[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.rvc_return[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.btb_prediction[1].valid
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.btb_prediction_shifted[1].valid
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_btb.btb_prediction_o[1].valid
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_queue.ready_o
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_realign.unaligned_d
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.i_instr_realign.valid_i
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.icache_dreq_i.ready
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.icache_dreq_i.valid
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.icache_dreq_o.req
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.icache_valid_q
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.if_ready
unclassified	assert	cex	i_frontend.rvi_jalr[0] \|=> i_frontend.instr_queue_ready
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_ras.data_o.valid
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_ras.stack_d[0].valid
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_ras.stack_d[1].valid
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_ras.stack_q[0].valid
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.i_ras.stack_q[1].valid
unclassified	assert	cex	i_frontend.taken_rvc_cf[1] \|=> i_frontend.ras_predict.valid
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.bht_update.taken \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.bht_update.taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.bht_update.taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.bht_update.taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.bht_update.taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.bht_update.taken \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.bht_update.taken \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.gen_instr_scan[0].i_instr_scan.rvi_branch_o
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.bht_update.valid \|=> i_frontend.rvi_branch[0]
unclassified	assert	cex	i_frontend.bp_valid \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.bp_valid \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.bp_valid \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.bp_valid \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.btb_prediction[0].valid \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.btb_prediction_shifted[0].valid \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.btb_prediction[0].valid
unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.btb_prediction_shifted[0].valid
unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_jal_r
unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jr_o
unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.i_btb.btb_prediction_o[0].valid
unclassified	assert	cex	i_frontend.btb_update.valid \|=> i_frontend.rvc_jr[0]
unclassified	assert	cex	i_frontend.fetch_entry_ready_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.fetch_entry_valid_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.is_jal_r \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.is_jal_r \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jr_o \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jump_o \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jump_o \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_branch_o \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_branch_o \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_branch_o \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jump_o \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jump_o \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.gen_instr_scan[0].i_instr_scan.rvi_jump_o \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.taken \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.taken \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.taken \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.gen_instr_scan[0].i_instr_scan.rvi_branch_o
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.i_bht.bht_update_i.valid \|=> i_frontend.rvi_branch[0]
unclassified	assert	cex	i_frontend.i_btb.btb_prediction_o[0].valid \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.btb_prediction[0].valid
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.btb_prediction_shifted[0].valid
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_jal_r
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jr_o
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.i_btb.btb_prediction_o[0].valid
unclassified	assert	cex	i_frontend.i_btb.btb_update_i.valid \|=> i_frontend.rvc_jr[0]
unclassified	assert	cex	i_frontend.i_instr_queue.consumed_o[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.consumed_o[1] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.i_instr_queue.consumed_o[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.fetch_entry_ready_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.fetch_entry_valid_o \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.fifo_pos[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.fifo_pos[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.pop_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.pop_i \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.pop_i \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.push_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.usage_o[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.pop_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.push_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.usage_o[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.left_child_result \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.padded_input[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.padded_input[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.popcount_o[0] \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.popcount_o[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.popcount_o[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.popcount_o[0] \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.popcount_o[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.popcount_o[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.popcount_o[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.popcount_o[1] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.popcount_o[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.i_popcount.right_child_result \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.instr_queue_usage[0][0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.instr_queue_usage[1][0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.pop_instr[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.pop_instr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.i_instr_queue.pop_instr[0] \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.i_instr_queue.pop_instr[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.popcount[0] \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.i_instr_queue.popcount[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.popcount[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.popcount[0] \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.i_instr_queue.popcount[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.popcount[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.popcount[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.popcount[1] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.i_instr_queue.popcount[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.push_instr[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.push_instr[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.push_instr_fifo[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.push_instr_fifo[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.shamt \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.i_instr_queue.shamt \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.shamt \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.shamt \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.i_instr_queue.shamt \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.shamt \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.shamt \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.i_instr_queue.taken[0] \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.i_instr_queue.taken[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.taken[0] \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.i_instr_queue.taken[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.i_instr_queue.valid[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.valid[1] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.i_instr_queue.valid[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.valid_i[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_queue.valid_i[1] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.i_instr_queue.valid_i[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_realign.valid_i \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_realign.valid_o[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.i_instr_realign.valid_o[1] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.i_instr_realign.valid_o[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.icache_dreq_i.ready \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.icache_dreq_i.valid \|=> i_frontend.i_instr_queue.consumed_o[0]
unclassified	assert	cex	i_frontend.icache_dreq_i.valid \|=> i_frontend.i_instr_queue.valid[0]
unclassified	assert	cex	i_frontend.icache_dreq_i.valid \|=> i_frontend.i_instr_queue.valid_i[0]
unclassified	assert	cex	i_frontend.icache_dreq_i.valid \|=> i_frontend.i_instr_realign.valid_o[0]
unclassified	assert	cex	i_frontend.icache_dreq_i.valid \|=> i_frontend.icache_dreq_i.ready
unclassified	assert	cex	i_frontend.icache_dreq_i.valid \|=> i_frontend.if_ready
unclassified	assert	cex	i_frontend.icache_dreq_i.valid \|=> i_frontend.instr_queue_consumed[0]
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s1 \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s1 \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s1 \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s1 \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s1 \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.icache_dreq_o.kill_s1 \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.icache_valid_q \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.if_ready \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.instr_queue_consumed[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.instr_queue_consumed[1] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.instr_queue_consumed[1] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.rvi_branch_o
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.read_pointer_q[0]
unclassified	assert	cex	i_frontend.is_branch[0] \|=> i_frontend.rvi_branch[0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_jal_r
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jr_o
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.usage_o[0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.pop_i
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.read_pointer_n[0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.usage_o[0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_n[1]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_q[0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.write_pointer_q[1]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.idx_ds_d[0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.idx_is_d
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.instr_queue_usage[0][0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.instr_queue_usage[1][0]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.i_instr_queue.pop_instr[1]
unclassified	assert	cex	i_frontend.is_jalr[0] \|=> i_frontend.rvc_jr[0]
unclassified	assert	cex	i_frontend.is_jump[0] \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.is_jump[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.is_jump[0] \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.is_jump[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.resolved_branch_i.is_taken \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.resolved_branch_i.is_taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.resolved_branch_i.is_taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.resolved_branch_i.is_taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.resolved_branch_i.is_taken \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.resolved_branch_i.is_taken \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.resolved_branch_i.is_taken \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.resolved_branch_i.valid \|=> i_frontend.i_instr_queue.branch_empty
unclassified	assert	cex	i_frontend.resolved_branch_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.resolved_branch_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.resolved_branch_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.resolved_branch_i.valid \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.gate_clock
unclassified	assert	cex	i_frontend.resolved_branch_i.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[0]
unclassified	assert	cex	i_frontend.resolved_branch_i.valid \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.rvc_jr[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.is_rvc
unclassified	assert	cex	i_frontend.rvc_jump[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.rvc_jump[0] \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.rvi_branch[0] \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.rvi_branch[0] \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.rvi_branch[0] \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.rvi_jump[0] \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.rvi_jump[0] \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.rvi_jump[0] \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.gen_instr_scan[0].i_instr_scan.rvc_jump_o
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.pop_i
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[0].i_fifo_instr_data.usage_o[0]
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.gen_instr_fifo[1].i_fifo_instr_data.empty_o
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.idx_ds_d[1]
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.idx_ds_q[0]
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.idx_is_d
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.idx_is_q
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.instr_queue_empty[1]
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.instr_queue_usage[0][0]
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.i_instr_queue.pop_instr[0]
unclassified	assert	cex	i_frontend.taken_rvc_cf[0] \|=> i_frontend.rvc_jump[0]
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.i_instr_queue.fetch_entry_ready_i
unclassified	assert	cex	i_frontend.taken_rvi_cf[0] \|=> i_frontend.i_instr_queue.fetch_entry_valid_o
unclassified	assert	cex	i_frontend.debug_mode_i \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.debug_mode_i \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.debug_mode_i \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.i_bht.debug_mode_i \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.i_bht.debug_mode_i \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.i_bht.debug_mode_i \|=> i_frontend.i_btb.debug_mode_i
unclassified	assert	cex	i_frontend.i_btb.debug_mode_i \|=> i_frontend.debug_mode_i
unclassified	assert	cex	i_frontend.i_btb.debug_mode_i \|=> i_frontend.i_bht.debug_mode_i
unclassified	assert	cex	i_frontend.i_btb.debug_mode_i \|=> i_frontend.i_btb.debug_mode_i
--

module: ariane create date: May 09 15:27:29 EDT 2026 filter: class in ( unclassified ) and rank = high and type in ( assert ) and progress state in ( new, hole, covered, covered_now_hole, assert, violated, certified_hole, certified_assert )

[Jasper 2026.03] [Platform Linux64] [Version 2026.03 FCS 64 bits] [Build date 2026.03.26 12:48:29 UTC]

Jasper® Apps Behavioral Property SynthesisReport

module: arianecreate date: May 09 15:27:29 EDT 2026filter: class in ( unclassified ) and rank = high and type in ( assert ) and progress state in ( new, hole, covered, covered_now_hole, assert, violated, certified_hole, certified_assert )

DESIGN INFORMATION SUMMARY:

PROPERTY SYNTHESIS SUMMARY:

module: arianecreate date: May 09 15:27:29 EDT 2026filter: class in ( unclassified ) and rank = high and type in ( assert ) and progress state in ( new, hole, covered, covered_now_hole, assert, violated, certified_hole, certified_assert )

[Jasper 2026.03] [Platform Linux64] [Version 2026.03 FCS 64 bits] [Build date 2026.03.26 12:48:29 UTC]

module: ariane create date: May 09 15:27:29 EDT 2026 filter: class in ( unclassified ) and rank = high and type in ( assert ) and progress state in ( new, hole, covered, covered_now_hole, assert, violated, certified_hole, certified_assert )

module: ariane create date: May 09 15:27:29 EDT 2026 filter: class in ( unclassified ) and rank = high and type in ( assert ) and progress state in ( new, hole, covered, covered_now_hole, assert, violated, certified_hole, certified_assert )