github-mirrors/ibex
1
0
Fork 0
mirror of https://github.com/lowRISC/ibex.git synced 2025-06-28 01:12:02 -04:00
Code Issues Projects Releases Packages Wiki Activity Actions

[dv/formal] Helpers for DivInstrStable

Browse source 
To make the proof of DivInstrStable, this commit adds two helper
properties in the previous step. One that when an instruction is not a
multiply that the multiplier state must never leave ALBL and one that
the writeback stage must have a valid instruction in it if it is
blocking an instruction from proceeding from EX to WB. This allow
DivInstrStable to be proven with Hp 2.
This commit is contained in:
Marno van der Maas 2025-05-09 16:22:44 +01:00 • committed by Harry Callahan
parent 4fe6b7d53f
commit 0b718c5eac
1 changed files with 25 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

45
dv/formal/thm/ibex.proof
View file

@ -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)