diff --git a/dv/formal/thm/ibex.proof b/dv/formal/thm/ibex.proof index cd79f0cb..b0995d57 100644 --- a/dv/formal/thm/ibex.proof +++ b/dv/formal/thm/ibex.proof @@ -23,7 +23,7 @@ lemma ibex WfiKill: have (wbexc_exists & wbexc_is_wfi |-> ex_kill) ErrKill: have (wbexc_exists & wbexc_err |-> ex_kill) - + ReqRequiresInstr: have (data_req_o |-> ex_has_compressed_instr) ReqRequiresNotIllegal: have (data_req_o |-> ~`CR.illegal_insn_id & ~`CR.illegal_c_insn_id) @@ -45,7 +45,7 @@ lemma ibex DecompressionMatchIdEx: have (ex_has_compressed_instr & ~`CR.illegal_insn_id & ~`CR.illegal_c_insn_id |-> decompressed_instr == `CR.instr_rdata_id) DecompressionIllegalWbexc: have (wbexc_exists |-> decompressed_instr_illegal_2 == wbexc_compressed_illegal) DecompressionMatchWbexc: have (wbexc_exists & ~wbexc_illegal & ~wbexc_compressed_illegal |-> decompressed_instr_2 == wbexc_decompressed_instr) - + HasCompressed: have (`CR.instr_valid_id |-> ex_has_compressed_instr) LSUInstrStable: have (`LSU.ls_fsm_cs != 0 |-> $stable(`CR.instr_rdata_id)) @@ -56,14 +56,14 @@ lemma ibex LSUFinishFast: have (`LSU.ls_fsm_cs == 0 && data_gnt_i && `LSU.ls_fsm_ns == 0 |-> instr_will_progress) SndGntReqFstGnt: have (mem_gnt_snd_d |-> mem_gnt_fst_q) - + WBOutstandingNoReq: have (outstanding_mem & ~`LSU.lsu_resp_valid_o |-> ~data_req_o) NotIdleReqDec: have (`LSU.ls_fsm_cs != `LSU.IDLE |-> `ID.lsu_req_dec) NotIdleNoExErr: have (`LSU.ls_fsm_cs != `LSU.IDLE |-> ~ex_err) ProgressNoWbStall: have (instr_will_progress |-> ~`IDC.stall_wb_i) - + NoStoreWb: have (`WBG.wb_instr_type_q == WB_INSTR_STORE |-> ~`WB.rf_we_wb_o) WbInstrDefined: have (`WBG.wb_valid_q |-> `WBG.wb_instr_type_q != 2'b11) @@ -94,7 +94,7 @@ lemma ibex ~`WBG.rf_we_wb_q & (`WBG.wb_instr_type_q != WB_INSTR_LOAD) ) ValidToBranch: have (ex_has_branched_d |-> `CR.instr_valid_id) - + LsuWeq: block Ex: have (`LSU.ls_fsm_cs != `LSU.IDLE && mem_gnt_fst_q |-> ex_is_store_instr == `LSU.data_we_q) / @@ -104,7 +104,7 @@ lemma ibex LSUEmpty: have (`LSU.ls_fsm_cs != `LSU.IDLE |-> ~wbexc_exists & ~ex_kill) / LSUEnd: have (`LSU.lsu_req_done_o |-> instr_will_progress) - + block NoFinishingIRQ: have (wbexc_exists |-> ~wbexc_handling_irq) / @@ -115,7 +115,7 @@ lemma ibex Pmp_cfg:(pmp_cfg) Pmp_addr:(pmp_addr) Mseccfg:(mseccfg) \ Pc:(pc) have (wbexc_exists |-> spec_past_``X == wbexc_post_``X) - + / # This graph induction bounds the number of waiting responses, @@ -168,32 +168,32 @@ lemma ibex node idle idle (`LSU.ls_fsm_cs == `LSU.IDLE && ~`IDG.outstanding_memory_access && (`ID.lsu_req_dec || ~`ID.lsu_req_done_i)) edge idle => idle edge idle -> idle_active - + node idle_active idle_active (`LSU.ls_fsm_cs == `LSU.IDLE && `CR.lsu_req) edge idle_active => wait_rvalid_mis wait_gnt_mis wait_gnt edge idle_active -> step step_fail - + node wait_gnt_mis wait_gnt_mis (`LSU.ls_fsm_cs == `LSU.WAIT_GNT_MIS) edge wait_gnt_mis => wait_gnt_mis wait_rvalid_mis - + node wait_rvalid_mis wait_rvalid_mis (`LSU.ls_fsm_cs == `LSU.WAIT_RVALID_MIS) edge wait_rvalid_mis => wait_rvalid_mis wait_rvalid_mis_gnts_done wait_gnt edge wait_rvalid_mis -> step step_fail - + node wait_gnt wait_gnt (`LSU.ls_fsm_cs == `LSU.WAIT_GNT) edge wait_gnt => wait_gnt edge wait_gnt -> step step_fail - + node wait_rvalid_mis_gnts_done wait_rvalid_mis_gnts_done (`LSU.ls_fsm_cs == `LSU.WAIT_RVALID_MIS_GNTS_DONE) edge wait_rvalid_mis_gnts_done => wait_rvalid_mis_gnts_done edge wait_rvalid_mis_gnts_done -> step step_fail node step step (`LSU.lsu_req_done_o && ~`LSU.pmp_err_d) edge step => wait end - + node step_fail step_fail (`LSU.lsu_req_done_o && `LSU.pmp_err_d) edge step_fail => fail - + node wait wait (`IDG.outstanding_memory_access && ~`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && ~instr_will_progress) edge wait => wait end @@ -201,7 +201,7 @@ lemma ibex edge end -> idle node fail fail (`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && ~data_rvalid_i) - edge fail -> idle + edge fail -> idle / NoMemAccessNoRValid: have (`LSU.lsu_resp_valid_o -> outstanding_mem) StallNoChangeA: have (`LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(`ID.rf_rdata_a_fwd)) @@ -219,12 +219,17 @@ lemma ibex MultEndState: have (instr_will_progress |=> `MULTG.mult_state_q == `MULTG.ALBL) + # Assert that only when multiplying the mult_state_q leaves ALBL mode. This assertion helps remove some state space for DivInstrStable. + DivInstrNotMult: have (~`MULT.mult_en_internal |-> `MULTG.mult_state_q == `MULTG.ALBL) + # When there is an instruction is finished in EX but is blocked from moving to WB then there must be a valid instruction in the WB stage. This is a helper property for DivInstrStable + InstrInWbStage: have (wbexc_exists & ~wbexc_finishing -> `WBG.wb_valid_q) + / - + MemErrKind: have (finishing_executed && wbexc_is_mem_instr && ~wbexc_illegal && wbexc_err |-> `IDC.store_err_q | `IDC.load_err_q) MemErrStructure: have (finishing_executed && wbexc_is_mem_instr && ~wbexc_illegal && wbexc_err |-> $past(instr_will_progress, 2) | $past(data_rvalid_i)) MemNoErrStructure: have (finishing_executed && wbexc_is_mem_instr && ~wbexc_illegal && ~wbexc_err |-> data_rvalid_i) - + WbexcMemErrKindLoad: have (`IDC.load_err_q |-> wbexc_exists & wbexc_is_load_instr) WbexcMemErrKindStore: have (`IDC.store_err_q |-> wbexc_exists & wbexc_is_store_instr) @@ -255,7 +260,7 @@ lemma ibex FirstCycleNoGnt: have (`ID.instr_first_cycle |-> ~mem_gnt_fst_q) MemStartFirstCycle: have (`LSU.ls_fsm_cs == `LSU.IDLE && `CR.lsu_req |-> `ID.instr_first_cycle) - # The below is slow! + DivInstrStable: have (`MULT.md_state_q != `MULT.MD_IDLE |-> $stable(`CR.instr_rdata_id) && `CR.instr_valid_id && (~`ID.stall_multdiv -> `MULT.md_state_q == `MULT.MD_FINISH) && `MULTG.mult_state_q == `MULTG.ALBL && `MULT.div_en_internal && (~wbexc_exists | wbexc_finishing)) InstrReqCount: have ( @@ -263,7 +268,7 @@ lemma ibex (instr_mem_assume.outstanding_reqs_q == 1) == (~`IFP.rdata_outstanding_q[1] && `IFP.rdata_outstanding_q[0]) && (instr_mem_assume.outstanding_reqs_q == 0) == (~`IFP.rdata_outstanding_q[1] && ~`IFP.rdata_outstanding_q[0]) ) - + / MepcEn: have (`CSR.mepc_en |-> instr_will_progress | wbexc_finishing | wbexc_handling_irq) @@ -279,7 +284,7 @@ lemma ibex NormalMainResMatch: have (`ID.instr_valid_i && ~ex_kill && main_mode == MAIN_IDEX |-> spec_api_i.main_result == MAINRES_OK) FetchErrMainResMatch: have (`ID.instr_valid_i && ~ex_kill && main_mode == MAIN_IFERR |-> spec_api_i.main_result == MAINRES_OK) IRQMainResMatch: have (wbexc_handling_irq && main_mode == MAIN_IRQ |-> spec_api_i.main_result == MAINRES_OK) - + / SpecEnUnreach: have (spec_en |-> ~spec_int_err)