0001-01-01

Jasper® Apps Behavioral Property SynthesisReport

module: ariane create date: May 09 19:14:14 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	53	0

POI#	Signals
User-defined
	Classification	Type	Status	Property
1	id_stage_i.compressed_decoder_i.illegal_instr_o , id_stage_i.compressed_decoder_i.is_compressed_o , id_stage_i.debug_mode_i , id_stage_i.debug_req_i , id_stage_i.decoded_instruction.ex.valid , id_stage_i.decoded_instruction.is_compressed , id_stage_i.decoded_instruction.use_imm , ...
	unclassified	assert	cex	id_stage_i.decoder_i.ebreak \|=> id_stage_i.debug_mode_i
	unclassified	assert	cex	id_stage_i.decoder_i.ebreak \|=> id_stage_i.decoder_i.debug_mode_i
	unclassified	assert	cex	id_stage_i.decoder_i.fs_i[0] \|=> id_stage_i.decoder_i.fs_i[0]
	unclassified	assert	cex	id_stage_i.decoder_i.fs_i[0] \|=> id_stage_i.decoder_i.fs_i[1]
	unclassified	assert	cex	id_stage_i.decoder_i.fs_i[0] \|=> id_stage_i.fs_i[0]
	unclassified	assert	cex	id_stage_i.decoder_i.fs_i[0] \|=> id_stage_i.fs_i[1]
	unclassified	assert	cex	id_stage_i.decoder_i.fs_i[1] \|=> id_stage_i.decoder_i.fs_i[0]
	unclassified	assert	cex	id_stage_i.decoder_i.fs_i[1] \|=> id_stage_i.decoder_i.fs_i[1]
	unclassified	assert	cex	id_stage_i.decoder_i.fs_i[1] \|=> id_stage_i.fs_i[0]
	unclassified	assert	cex	id_stage_i.decoder_i.fs_i[1] \|=> id_stage_i.fs_i[1]
	unclassified	assert	cex	id_stage_i.fs_i[0] \|=> id_stage_i.decoder_i.fs_i[0]
	unclassified	assert	cex	id_stage_i.fs_i[0] \|=> id_stage_i.decoder_i.fs_i[1]
	unclassified	assert	cex	id_stage_i.fs_i[0] \|=> id_stage_i.fs_i[0]
	unclassified	assert	cex	id_stage_i.fs_i[0] \|=> id_stage_i.fs_i[1]
	unclassified	assert	cex	id_stage_i.fs_i[1] \|=> id_stage_i.decoder_i.fs_i[0]
	unclassified	assert	cex	id_stage_i.fs_i[1] \|=> id_stage_i.decoder_i.fs_i[1]
	unclassified	assert	cex	id_stage_i.fs_i[1] \|=> id_stage_i.fs_i[0]
	unclassified	assert	cex	id_stage_i.fs_i[1] \|=> id_stage_i.fs_i[1]
	unclassified	assert	cex	id_stage_i.issue_entry_o.use_pc \|=> id_stage_i.issue_entry_o.use_imm
	unclassified	assert	cex	id_stage_i.issue_entry_o.use_pc \|=> id_stage_i.issue_n.sbe.use_imm
	unclassified	assert	cex	id_stage_i.issue_entry_o.use_pc \|=> id_stage_i.issue_q.sbe.use_imm
	unclassified	assert	proven	id_stage_i.issue_n.is_ctrl_flow \|=> id_stage_i.is_ctrl_flow_o
	unclassified	assert	proven	id_stage_i.issue_n.is_ctrl_flow \|=> id_stage_i.issue_entry_o.use_imm
	unclassified	assert	proven	id_stage_i.issue_n.is_ctrl_flow \|=> id_stage_i.issue_q.is_ctrl_flow
	unclassified	assert	proven	id_stage_i.issue_n.is_ctrl_flow \|=> id_stage_i.issue_q.sbe.use_imm
	unclassified	assert	proven	id_stage_i.issue_n.sbe.ex.valid \|=> id_stage_i.issue_entry_o.ex.valid
	unclassified	assert	proven	id_stage_i.issue_n.sbe.ex.valid \|=> id_stage_i.issue_entry_o.valid
	unclassified	assert	proven	id_stage_i.issue_n.sbe.ex.valid \|=> id_stage_i.issue_q.sbe.ex.valid
	unclassified	assert	proven	id_stage_i.issue_n.sbe.ex.valid \|=> id_stage_i.issue_q.sbe.valid
	unclassified	assert	proven	id_stage_i.issue_n.sbe.is_compressed \|=> id_stage_i.issue_entry_o.is_compressed
	unclassified	assert	proven	id_stage_i.issue_n.sbe.is_compressed \|=> id_stage_i.issue_q.sbe.is_compressed
	unclassified	assert	proven	id_stage_i.issue_n.sbe.use_imm \|=> id_stage_i.issue_entry_o.use_imm
	unclassified	assert	proven	id_stage_i.issue_n.sbe.use_imm \|=> id_stage_i.issue_q.sbe.use_imm
	unclassified	assert	proven	id_stage_i.issue_n.sbe.use_pc \|=> id_stage_i.issue_entry_o.use_imm
	unclassified	assert	proven	id_stage_i.issue_n.sbe.use_pc \|=> id_stage_i.issue_entry_o.use_pc
	unclassified	assert	cex	id_stage_i.issue_n.sbe.use_pc \|=> id_stage_i.issue_n.sbe.use_imm
	unclassified	assert	proven	id_stage_i.issue_n.sbe.use_pc \|=> id_stage_i.issue_q.sbe.use_imm
	unclassified	assert	proven	id_stage_i.issue_n.sbe.use_pc \|=> id_stage_i.issue_q.sbe.use_pc
	unclassified	assert	proven	id_stage_i.issue_n.sbe.valid \|=> id_stage_i.issue_entry_o.ex.valid
	unclassified	assert	proven	id_stage_i.issue_n.sbe.valid \|=> id_stage_i.issue_entry_o.valid
	unclassified	assert	proven	id_stage_i.issue_n.sbe.valid \|=> id_stage_i.issue_q.sbe.ex.valid
	unclassified	assert	proven	id_stage_i.issue_n.sbe.valid \|=> id_stage_i.issue_q.sbe.valid
	unclassified	assert	proven	id_stage_i.issue_n.valid \|=> id_stage_i.issue_entry_valid_o
	unclassified	assert	proven	id_stage_i.issue_n.valid \|=> id_stage_i.issue_q.valid
	unclassified	assert	cex	id_stage_i.issue_q.sbe.use_pc \|=> id_stage_i.issue_entry_o.use_imm
	unclassified	assert	cex	id_stage_i.issue_q.sbe.use_pc \|=> id_stage_i.issue_n.sbe.use_imm
	unclassified	assert	cex	id_stage_i.issue_q.sbe.use_pc \|=> id_stage_i.issue_q.sbe.use_imm
	unclassified	assert	cex	id_stage_i.decoded_instruction.use_pc \|=> id_stage_i.issue_entry_o.use_imm
	unclassified	assert	cex	id_stage_i.decoded_instruction.use_pc \|=> id_stage_i.issue_q.sbe.use_imm
	unclassified	assert	cex	id_stage_i.debug_mode_i \|=> id_stage_i.debug_mode_i
	unclassified	assert	cex	id_stage_i.debug_mode_i \|=> id_stage_i.decoder_i.debug_mode_i
	unclassified	assert	cex	id_stage_i.decoder_i.debug_mode_i \|=> id_stage_i.debug_mode_i
	unclassified	assert	cex	id_stage_i.decoder_i.debug_mode_i \|=> id_stage_i.decoder_i.debug_mode_i
--

module: ariane create date: May 09 19:14:14 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 19:14:14 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 19:14:14 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 19:14:14 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 19:14:14 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 )