../
Jasper® Apps Behavioral Property SynthesisReport
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 |
| User-defined | |||||
| POI# | Signals | Critical Values | |||
|---|---|---|---|---|---|
| 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 ) |