0001-01-01

Jasper® Apps Behavioral Property SynthesisReport

module: ariane create date: May 10 20:56:21 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	202	0

POI#	Signals
User-defined
	Classification	Type	Status	Property
1	ex_stage_i.alu_valid_i , ex_stage_i.amo_resp_i.ack , ex_stage_i.amo_valid_commit_i , ex_stage_i.branch_valid_i , ex_stage_i.csr_buffer_i.csr_reg_q.valid , ex_stage_i.csr_commit_i , ex_stage_i.csr_valid_i , ex_stage_i.dcache_req_ports_i[0].data_gnt , ex_stage_i.dcache_req_ports_i[0].data_rvalid , ...
	unclassified	assert	cex	ex_stage_i.alu_valid_i \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.branch_valid_i \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.branch_valid_i \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.csr_valid_i \|=> ex_stage_i.csr_buffer_i.csr_reg_q.valid
	unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_gnt \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_gnt \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_rvalid \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_rvalid \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[2].data_gnt \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.dcache_wbuffer_empty_i \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.debug_mode_i \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.debug_mode_i \|=> ex_stage_i.lsu_ready_o
	unclassified	assert	cex	ex_stage_i.flush_i \|=> ex_stage_i.dcache_wbuffer_empty_i
	unclassified	assert	proven	ex_stage_i.flush_i \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.flush_i \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	proven	ex_stage_i.flush_i \|=> ex_stage_i.lsu_ready_o
	unclassified	assert	cex	ex_stage_i.flush_i \|=> ex_stage_i.no_st_pending_o
	unclassified	assert	cex	ex_stage_i.fpu_valid_i \|=> ex_stage_i.dcache_wbuffer_empty_i
	unclassified	assert	cex	ex_stage_i.fpu_valid_i \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.fpu_valid_i \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.fpu_valid_i \|=> ex_stage_i.lsu_ready_o
	unclassified	assert	cex	ex_stage_i.fpu_valid_i \|=> ex_stage_i.no_st_pending_o
	unclassified	assert	cex	ex_stage_i.fpu_valid_o \|=> ex_stage_i.dcache_wbuffer_empty_i
	unclassified	assert	cex	ex_stage_i.fpu_valid_o \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.fpu_valid_o \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.fpu_valid_o \|=> ex_stage_i.lsu_ready_o
	unclassified	assert	cex	ex_stage_i.fpu_valid_o \|=> ex_stage_i.no_st_pending_o
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.div_res_zero_q \|=> ex_stage_i.i_mult.i_div.div_res_zero_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.div_res_zero_q \|=> ex_stage_i.i_mult.i_div.rem_sel_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.rem_sel_q \|=> ex_stage_i.i_mult.i_div.div_res_zero_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.rem_sel_q \|=> ex_stage_i.i_mult.i_div.rem_sel_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.state_q[0] \|=> ex_stage_i.dcache_wbuffer_empty_i
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.state_q[0] \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.state_q[0] \|=> ex_stage_i.i_mult.i_div.div_res_zero_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.state_q[0] \|=> ex_stage_i.i_mult.i_div.rem_sel_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.state_q[0] \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.state_q[0] \|=> ex_stage_i.lsu_i.lsu_bypass_i.read_pointer_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.state_q[0] \|=> ex_stage_i.lsu_i.lsu_bypass_i.write_pointer_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.state_q[0] \|=> ex_stage_i.lsu_ready_o
	unclassified	assert	cex	ex_stage_i.i_mult.i_div.state_q[0] \|=> ex_stage_i.no_st_pending_o
	unclassified	assert	cex	ex_stage_i.i_mult.i_multiplier.mult_valid_o \|=> ex_stage_i.dcache_wbuffer_empty_i
	unclassified	assert	cex	ex_stage_i.i_mult.i_multiplier.mult_valid_o \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.i_mult.i_multiplier.mult_valid_o \|=> ex_stage_i.i_mult.i_div.div_res_zero_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_multiplier.mult_valid_o \|=> ex_stage_i.i_mult.i_div.rem_sel_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_multiplier.mult_valid_o \|=> ex_stage_i.i_mult.word_op_q
	unclassified	assert	cex	ex_stage_i.i_mult.i_multiplier.mult_valid_o \|=> ex_stage_i.is_compressed_instr_i
	unclassified	assert	cex	ex_stage_i.i_mult.i_multiplier.mult_valid_o \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.i_mult.i_multiplier.mult_valid_o \|=> ex_stage_i.lsu_ready_o
	unclassified	assert	cex	ex_stage_i.i_mult.i_multiplier.mult_valid_o \|=> ex_stage_i.no_st_pending_o
	unclassified	assert	cex	ex_stage_i.i_mult.mul_valid \|=> ex_stage_i.dcache_wbuffer_empty_i
	unclassified	assert	cex	ex_stage_i.i_mult.mul_valid \|=> ex_stage_i.flu_ready_o
	unclassified	assert	cex	ex_stage_i.i_mult.mul_valid \|=> ex_stage_i.i_mult.i_div.div_res_zero_q
	unclassified	assert	cex	ex_stage_i.i_mult.mul_valid \|=> ex_stage_i.i_mult.i_div.rem_sel_q
	unclassified	assert	cex	ex_stage_i.i_mult.mul_valid \|=> ex_stage_i.i_mult.word_op_q
	unclassified	assert	cex	ex_stage_i.i_mult.mul_valid \|=> ex_stage_i.is_compressed_instr_i
	unclassified	assert	cex	ex_stage_i.i_mult.mul_valid \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.i_mult.mul_valid \|=> ex_stage_i.lsu_ready_o
	unclassified	assert	cex	ex_stage_i.i_mult.mul_valid \|=> ex_stage_i.no_st_pending_o
	unclassified	assert	cex	ex_stage_i.i_mult.word_op_q \|=> ex_stage_i.i_mult.i_div.div_res_zero_q
	unclassified	assert	cex	ex_stage_i.i_mult.word_op_q \|=> ex_stage_i.i_mult.i_div.rem_sel_q
	unclassified	assert	cex	ex_stage_i.i_mult.word_op_q \|=> ex_stage_i.i_mult.word_op_q
	unclassified	assert	cex	ex_stage_i.load_valid_o \|=> ex_stage_i.lsu_commit_ready_o
	unclassified	assert	cex	ex_stage_i.load_valid_o \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[1] \|=> ex_stage_i.i_mult.i_div.div_res_zero_q
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[1] \|=> ex_stage_i.i_mult.i_div.rem_sel_q
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[1] \|=> ex_stage_i.i_mult.word_op_q
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[1] \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[2].valid
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[1] \|=> ex_stage_i.lsu_i.lsu_bypass_i.mem_q[0].valid
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[1] \|=> ex_stage_i.lsu_i.lsu_bypass_i.mem_q[1].valid
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[1] \|=> ex_stage_i.lsu_i.lsu_bypass_i.read_pointer_q
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[1] \|=> ex_stage_i.lsu_i.lsu_bypass_i.status_cnt_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[1] \|=> ex_stage_i.lsu_i.lsu_bypass_i.write_pointer_q
unclassified	assert	cex	ex_stage_i.mult_valid_i \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.mult_valid_i \|=> ex_stage_i.flu_valid_o
unclassified	assert	cex	ex_stage_i.mult_valid_i \|=> ex_stage_i.i_mult.i_div.div_res_zero_q
unclassified	assert	cex	ex_stage_i.mult_valid_i \|=> ex_stage_i.i_mult.i_div.rem_sel_q
unclassified	assert	cex	ex_stage_i.mult_valid_i \|=> ex_stage_i.lsu_commit_ready_o
unclassified	assert	cex	ex_stage_i.mult_valid_i \|=> ex_stage_i.lsu_ready_o
unclassified	assert	cex	ex_stage_i.mult_valid_i \|=> ex_stage_i.no_st_pending_o
unclassified	assert	proven	ex_stage_i.no_st_pending_o \|=> ex_stage_i.lsu_commit_ready_o
unclassified	assert	cex	ex_stage_i.resolve_branch_o \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.resolve_branch_o \|=> ex_stage_i.lsu_commit_ready_o
unclassified	assert	cex	ex_stage_i.resolved_branch_o.is_mispredict \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.resolved_branch_o.is_mispredict \|=> ex_stage_i.lsu_commit_ready_o
unclassified	assert	cex	ex_stage_i.resolved_branch_o.is_mispredict \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.resolved_branch_o.is_taken \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.resolved_branch_o.is_taken \|=> ex_stage_i.lsu_commit_ready_o
unclassified	assert	cex	ex_stage_i.alu_valid_i \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.branch_valid_i \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.branch_valid_i \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.csr_buffer_i.csr_reg_q.valid \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.csr_buffer_i.csr_reg_q.valid \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.csr_commit_i \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.csr_commit_i \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.csr_valid_i \|=> ex_stage_i.csr_commit_i
unclassified	assert	cex	ex_stage_i.csr_valid_i \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_gnt \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_gnt \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_gnt \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_rvalid \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_rvalid \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_rvalid \|=> ex_stage_i.load_valid_o
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[1].data_rvalid \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[2].data_gnt \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[2].data_gnt \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.dcache_req_ports_i[2].data_gnt \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.flu_valid_o \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.icache_areq_i.fetch_req \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.is_compressed_instr_i \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.is_compressed_instr_i \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.load_valid_o \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.load_valid_o \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.load_valid_o \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_commit_i \|=> ex_stage_i.dcache_req_ports_i[2].data_gnt
unclassified	assert	cex	ex_stage_i.lsu_commit_i \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.lsu_commit_i \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_commit_i \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_commit_i \|=> ex_stage_i.icache_areq_i.fetch_req
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[0] \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[0] \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[0] \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[0] \|=> ex_stage_i.lsu_commit_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.state_q[0] \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[0].valid \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[0].valid \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[0].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[0]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[0].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[0]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[0].valid \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[1].valid \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[1].valid \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[1].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[1].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[1].valid \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[2].valid \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[2].valid \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[2].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[0]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[2].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[2].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[0]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[2].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[2].valid \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[3].valid \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[3].valid \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[3].valid \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[0].valid \|=> ex_stage_i.dcache_req_ports_i[2].data_gnt
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[0].valid \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[0].valid \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[0].valid \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[0].valid \|=> ex_stage_i.icache_areq_i.fetch_req
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[0].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[0].valid
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[0].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[0]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[0].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[0]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[1].valid \|=> ex_stage_i.dcache_req_ports_i[2].data_gnt
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[1].valid \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[1].valid \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[1].valid \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[1].valid \|=> ex_stage_i.icache_areq_i.fetch_req
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[1].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[1].valid
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[1].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[1].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.dcache_req_ports_i[2].data_gnt
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.icache_areq_i.fetch_req
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[2].valid
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[0]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[0]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[2].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[3].valid \|=> ex_stage_i.dcache_req_ports_i[2].data_gnt
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[3].valid \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[3].valid \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[3].valid \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[3].valid \|=> ex_stage_i.icache_areq_i.fetch_req
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[3].valid \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[3].valid
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[0] \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[0]
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[1] \|=> ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[1]
unclassified	assert	cex	ex_stage_i.lsu_i.lsu_bypass_i.read_pointer_q \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.lsu_bypass_i.write_pointer_q \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_valid_i \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.lsu_valid_i \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_valid_i \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.lsu_valid_i \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.resolve_branch_o \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.resolve_branch_o \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.resolved_branch_o.is_mispredict \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.resolved_branch_o.is_taken \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.resolved_branch_o.is_taken \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.store_valid_o \|=> ex_stage_i.dcache_wbuffer_empty_i
unclassified	assert	cex	ex_stage_i.store_valid_o \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.store_valid_o \|=> ex_stage_i.flu_ready_o
unclassified	assert	cex	ex_stage_i.store_valid_o \|=> ex_stage_i.lsu_commit_i
unclassified	assert	cex	ex_stage_i.store_valid_o \|=> ex_stage_i.no_st_pending_o
unclassified	assert	cex	ex_stage_i.debug_mode_i \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[3].valid \|=> ex_stage_i.lsu_i.lsu_bypass_i.read_pointer_q
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.commit_queue_q[3].valid \|=> ex_stage_i.lsu_i.lsu_bypass_i.write_pointer_q
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[3].valid \|=> ex_stage_i.lsu_i.lsu_bypass_i.read_pointer_q
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_queue_q[3].valid \|=> ex_stage_i.lsu_i.lsu_bypass_i.write_pointer_q
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[0] \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_read_pointer_q[1] \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[0] \|=> ex_stage_i.debug_mode_i
unclassified	assert	cex	ex_stage_i.lsu_i.i_store_unit.store_buffer_i.speculative_write_pointer_q[1] \|=> ex_stage_i.debug_mode_i
--

module: ariane create date: May 10 20:56:21 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 10 20:56:21 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 10 20:56:21 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 10 20:56:21 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 10 20:56:21 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 )