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

[dv,formal] FirstFetchNoInstr helper property for FetchErrRoot

Browse source 
FetchErrRoot is very slow to prove, and via SST I discovered that it
was exploring the state space where ctrl FSM is in FIRST_FETCH, and
there was a memory load instruction latched by IF, and it causes the stall
logic to think there is a memory-induced stall.

This is unreachable state because in FIRST_FETCH there can't be instructions
latched, so add a helper property to aid the proof.

Signed-off-by: Gary Guo <gary.guo@lowrisc.org>
This commit is contained in:
Gary Guo 2025-04-25 21:13:26 +01:00 • committed by Marno van der Maas
parent f79e858c81
commit 2c2dc5040f
2 changed files with 7 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -209,6 +209,10 @@ lemma ibex
BecameDecodeIsEmptyWbexc: have (`IDC.ctrl_fsm_cs == `IDC.DECODE && !$stable(`IDC.ctrl_fsm_cs) |-> ~wbexc_exists)
FetchErrIsErr: have (wbexc_fetch_err & wbexc_exists |-> wbexc_err & `IDC.instr_fetch_err)
# If control FSM is in `FIRST_FETCH`, then there shouldn't be an instruction that is already fetched by IF but not consumed by ID.
# This helps to prove FetchErrRoot.
FirstFetchNoInstr: have (`IDC.ctrl_fsm_ns == `IDC.FIRST_FETCH |-> ~`IF.instr_valid_id_q)
MemOpRequiresValid: have (`LSU.ls_fsm_cs != `LSU.IDLE || `CR.lsu_req |-> `ID.instr_valid_i)
MultEndState: have (instr_will_progress |=> `MULTG.mult_state_q == `MULTG.ALBL)
@ -242,6 +246,8 @@ lemma ibex
SpecStableStoreData: have (ex_is_pres_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write_fst_wdata))
SpecStableStoreSndData: have (ex_is_pres_store_instr && `LSU.ls_fsm_cs != `LSU.IDLE && ($past(`LSU.ls_fsm_cs) != `LSU.IDLE || $past(`LSU.lsu_req_i)) |-> $stable(spec_mem_write_snd_wdata))
FetchErrRoot: have (`ID.instr_valid_i && (`IDC.ctrl_fsm_cs == `IDC.FLUSH -> ~$past(`IDC.csr_pipe_flush)) |-> spec_fetch_err == `ID.instr_fetch_err_i)
LoadNotSpecWrite: have (ex_is_pres_load_instr |-> ~spec_mem_write)
StoreNotSpecRead: have (ex_is_pres_store_instr |-> ~spec_mem_read)
@ -256,8 +262,6 @@ lemma ibex
(instr_mem_assume.outstanding_reqs_q == 0) == (~`IFP.rdata_outstanding_q[1] && ~`IFP.rdata_outstanding_q[0])
)
# Slow!
FetchErrRoot: have (`ID.instr_valid_i && (`IDC.ctrl_fsm_cs == `IDC.FLUSH -> ~$past(`IDC.csr_pipe_flush)) |-> spec_fetch_err == `ID.instr_fetch_err_i)
/
MepcEn: have (`CSR.mepc_en |-> instr_will_progress | wbexc_finishing | wbexc_handling_irq)

3
dv/formal/verify.tcl
View file

@ -88,8 +88,7 @@ proc prove_lemmas {} {
prove -task Step5
report -task Step5
prove -property Step6::top.Ibex_FetchErrRoot
prove -property {Step6::top.Ibex_SpecStableLoad Step6::top.Ibex_SpecStableLoadSnd Step6::top.Ibex_SpecStableLoadAddr Step6::top.Ibex_SpecStableLoadSndAddr Step6::top.Ibex_SpecStableStore Step6::top.Ibex_SpecStableStoreSnd Step6::top.Ibex_SpecStableStoreAddr Step6::top.Ibex_SpecStableStoreSndAddr Step6::top.Ibex_SpecStableStoreData Step6::top.Ibex_SpecStableStoreSndData} -engine_mode Hp
prove -property {Step6::top.Ibex_SpecStableLoad Step6::top.Ibex_SpecStableLoadSnd Step6::top.Ibex_SpecStableLoadAddr Step6::top.Ibex_SpecStableLoadSndAddr Step6::top.Ibex_SpecStableStore Step6::top.Ibex_SpecStableStoreSnd Step6::top.Ibex_SpecStableStoreAddr Step6::top.Ibex_SpecStableStoreSndAddr Step6::top.Ibex_SpecStableStoreData Step6::top.Ibex_SpecStableStoreSndData Step6::top.Ibex_FetchErrRoot} -engine_mode Hp
prove -task Step6
report -task Step6