Jasper® Apps Behavioral Property SynthesisReport

module: ariane create date: May 10 22:28:27 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	40	0

POI#	Signals
User-defined
	Classification	Type	Status	Property
1	commit_stage_i.amo_resp_i.ack , commit_stage_i.amo_valid_commit_o , commit_stage_i.commit_ack_o[0] , commit_stage_i.commit_ack_o[1] , commit_stage_i.commit_csr_o , commit_stage_i.commit_instr_i[0].ex.valid , commit_stage_i.commit_instr_i[0].is_compressed , ...
	unclassified	assert	cex	commit_stage_i.commit_instr_i[0].ex.valid \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[0].ex.valid \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[0].use_pc \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].ex.valid \|=> commit_stage_i.commit_instr_i[1].use_imm
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].ex.valid \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].ex.valid \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].use_pc \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.csr_write_fflags_o \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.csr_write_fflags_o \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.dirty_fp_state_o \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.dirty_fp_state_o \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.exception_o.valid \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.exception_o.valid \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.fence_i_o \|=> commit_stage_i.commit_instr_i[0].use_imm
	unclassified	assert	cex	commit_stage_i.fence_i_o \|=> commit_stage_i.commit_instr_i[1].use_imm
	unclassified	assert	proven	commit_stage_i.fence_i_o \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.fence_i_o \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	proven	commit_stage_i.fence_o \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.fence_o \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	proven	commit_stage_i.no_st_pending_i \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.we_fpr_o[0] \|=> commit_stage_i.commit_lsu_ready_i
	unclassified	assert	cex	commit_stage_i.we_fpr_o[0] \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.commit_ack_o[1] \|=> commit_stage_i.commit_instr_i[1].use_imm
	unclassified	assert	cex	commit_stage_i.commit_ack_o[1] \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[0].is_compressed \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[0].use_pc \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].is_compressed \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].use_pc \|=> commit_stage_i.commit_instr_i[0].use_imm
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].use_pc \|=> commit_stage_i.commit_instr_i[1].use_imm
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].use_pc \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].valid \|=> commit_stage_i.commit_instr_i[1].use_imm
	unclassified	assert	cex	commit_stage_i.commit_instr_i[1].valid \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.fence_o \|=> commit_stage_i.commit_instr_i[0].use_imm
	unclassified	assert	cex	commit_stage_i.fence_o \|=> commit_stage_i.commit_instr_i[1].use_imm
	unclassified	assert	cex	commit_stage_i.we_gpr_o[1] \|=> commit_stage_i.commit_instr_i[1].use_imm
	unclassified	assert	cex	commit_stage_i.we_gpr_o[1] \|=> commit_stage_i.no_st_pending_i
	unclassified	assert	cex	commit_stage_i.commit_instr_i[0].ex.valid \|=> commit_stage_i.commit_instr_i[0].use_imm
	unclassified	assert	cex	commit_stage_i.commit_instr_i[0].ex.valid \|=> commit_stage_i.commit_instr_i[1].use_imm
	unclassified	assert	cex	commit_stage_i.exception_o.valid \|=> commit_stage_i.commit_instr_i[0].use_imm
	unclassified	assert	cex	commit_stage_i.exception_o.valid \|=> commit_stage_i.commit_instr_i[1].use_imm
--

module: ariane create date: May 10 22:28:27 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 22:28:27 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 22:28:27 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 22:28:27 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 22:28:27 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 )