mirror of
https://github.com/lowRISC/ibex.git
synced 2025-06-27 17:00:41 -04:00
[dv,formal] Remove patches, better proof script
The old patchfile disabled clock gating and set ResetAll = 1. We don't need either of these things any more with some minor invariant tweaks. This also improves the proof script, which should be faster now.
This commit is contained in:
mndstrmr
Marno van der Maas
parent
10270b6e9a
commit
50e7331f42
6 changed files with 64 additions and 214 deletions
|
|
@ -20,8 +20,6 @@ SAIL_SV_FLAGS=-sv -sv-comb -sv-inregs -sv-outregs -sv-nostrings -sv-nopacked -sv
|
|||
|
||||
# Use fusesoc to resolve the tree of components, copy all resolved source files into the build/ directory,
|
||||
# and then generate a filelist for jasper to ingest.
|
||||
# Finally, apply a number of small RTL patches necessary to make the formal flow work. (see files in patches/)
|
||||
# (Only patch the duplicated source files that fusesoc has copied into build/fusesoc/src, not the version-controlled originals)
|
||||
# - Note. we use the 'vcs' fusesoc backend flow to generate the filelist. This is because fusesoc does not currently implement a
|
||||
# JasperGold backend, but this is not an issue as the file-format generated by the vcs flow is compatible with jasper.
|
||||
.PHONY: fusesoc
|
||||
|
|
@ -34,7 +32,6 @@ fusesoc:
|
|||
--tool vcs \
|
||||
--setup \
|
||||
lowrisc:ibex:ibex_formal:0.1
|
||||
patch -p0 < patches/ibex_top.diff
|
||||
|
||||
.PHONY: sv
|
||||
sv:
|
||||
|
|
|
|||
|
|
@ -134,8 +134,6 @@ WFIStart: assume property (`IDC.ctrl_fsm_cs == SLEEP |-> (
|
|||
`CSR.mie_q.irq_timer |
|
||||
`CSR.mie_q.irq_external
|
||||
));
|
||||
// 5. Disable clock gating
|
||||
TestEn: assume property (test_en_i);
|
||||
// See protocol/* for further assumptions
|
||||
|
||||
///////////////////////////////// Declarations /////////////////////////////////
|
||||
|
|
|
|||
|
|
@ -1,31 +0,0 @@
|
|||
--- build/fusesoc/rtl/ibex_top.sv 2024-08-25 12:49:31.975238123 +0100
|
||||
+++ build/fusesoc/rtl/ibex_top.sv 2024-08-25 12:51:45.786743599 +0100
|
||||
@@ -142,7 +142,7 @@
|
||||
);
|
||||
|
||||
localparam bit Lockstep = SecureIbex;
|
||||
- localparam bit ResetAll = Lockstep;
|
||||
+ localparam bit ResetAll = 1;
|
||||
localparam bit DummyInstructions = SecureIbex;
|
||||
localparam bit RegFileECC = SecureIbex;
|
||||
localparam bit RegFileWrenCheck = SecureIbex;
|
||||
@@ -236,12 +236,13 @@
|
||||
|
||||
assign core_sleep_o = ~clock_en;
|
||||
|
||||
- prim_clock_gating core_clock_gate_i (
|
||||
- .clk_i (clk_i),
|
||||
- .en_i (clock_en),
|
||||
- .test_en_i(test_en_i),
|
||||
- .clk_o (clk)
|
||||
- );
|
||||
+ assign clk = clk_i;
|
||||
+ // prim_clock_gating core_clock_gate_i (
|
||||
+ // .clk_i (clk_i),
|
||||
+ // .en_i (clock_en),
|
||||
+ // .test_en_i(test_en_i),
|
||||
+ // .clk_o (clk)
|
||||
+ // );
|
||||
|
||||
////////////////////////
|
||||
// Core instantiation //
|
||||
|
|
@ -13,7 +13,8 @@ lemma ibex
|
|||
PrivMorUMpp: have ((`CSR.mstatus_q.mpp == PRIV_LVL_U) || (`CSR.mstatus_q.mpp == PRIV_LVL_M))
|
||||
PrivMorUCur: have ((`CSR.priv_lvl_q == PRIV_LVL_U) || (`CSR.priv_lvl_q == PRIV_LVL_M))
|
||||
|
||||
PCBit0: have (~`CR.pc_id[0])
|
||||
PCBit0: have (`ID.instr_valid_i -> ~`CR.pc_id[0])
|
||||
MEPCBit0: have (~`CSR.mepc_q[0])
|
||||
MtvecLow: have (pre_mtvec[7:0] == 8'h01)
|
||||
NmiMode: have (~`IDC.nmi_mode_q)
|
||||
EBreakIntoDebug: have (~`IDC.ebreak_into_debug)
|
||||
|
|
@ -26,7 +27,7 @@ lemma ibex
|
|||
ReqRequiresInstr: have (data_req_o |-> ex_has_compressed_instr)
|
||||
ReqRequiresNotIllegal: have (data_req_o |-> ~`CR.illegal_insn_id & ~`CR.illegal_c_insn_id)
|
||||
|
||||
AluInstrMatch: have (`CR.instr_rdata_id == `CR.instr_rdata_alu_id)
|
||||
AluInstrMatch: have (`ID.instr_valid_i |-> `CR.instr_rdata_id == `CR.instr_rdata_alu_id)
|
||||
|
||||
IdExNotReq: have (~ex_is_mem_instr -> ~data_req_o)
|
||||
IdExNotMemMuteIncr: have (`CR.instr_valid_id & ~ex_is_mem_instr -> ~`ID.lsu_addr_incr_req_i & ~`ID.lsu_req_done_i)
|
||||
|
|
@ -64,7 +65,7 @@ lemma ibex
|
|||
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_instr_type_q != 2'b11)
|
||||
WbInstrDefined: have (`WBG.wb_valid_q |-> `WBG.wb_instr_type_q != 2'b11)
|
||||
|
||||
RfWriteWb: have (`CR.rf_write_wb & wbexc_finishing |-> `WB.rf_we_wb_o)
|
||||
|
||||
|
|
@ -125,7 +126,8 @@ lemma ibex
|
|||
Memory: graph_induction +rev
|
||||
inv idle (
|
||||
~`LSU.handle_misaligned_q &&
|
||||
`CR.lsu_resp_valid == outstanding_mem
|
||||
`CR.lsu_resp_valid == outstanding_mem &&
|
||||
data_mem_assume.outstanding_reqs == data_gnt_i
|
||||
)
|
||||
inv idle_active (
|
||||
data_mem_assume.outstanding_reqs == data_gnt_i &&
|
||||
|
|
@ -163,7 +165,7 @@ lemma ibex
|
|||
|
||||
entry ($rose(rst_ni)) -> idle
|
||||
|
||||
node idle idle (`LSU.ls_fsm_cs == `LSU.IDLE && data_mem_assume.outstanding_reqs == data_gnt_i)
|
||||
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
|
||||
|
||||
|
|
@ -192,7 +194,7 @@ lemma ibex
|
|||
node step_fail step_fail (`LSU.lsu_req_done_o && `LSU.pmp_err_d)
|
||||
edge step_fail => fail
|
||||
|
||||
node wait wait (has_resp_waiting_q && ~`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && ~instr_will_progress)
|
||||
node wait wait (`IDG.outstanding_memory_access && ~`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && ~instr_will_progress)
|
||||
edge wait => wait end
|
||||
|
||||
node end end (`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && data_rvalid_i)
|
||||
|
|
@ -248,8 +250,8 @@ lemma ibex
|
|||
|
||||
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)
|
||||
LoadNotSpecWrite: have (`ID.instr_valid_i & ex_is_pres_load_instr |-> ~spec_mem_write)
|
||||
StoreNotSpecRead: have (`ID.instr_valid_i & ex_is_pres_store_instr |-> ~spec_mem_read)
|
||||
|
||||
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)
|
||||
|
|
|
|||
|
|
@ -138,7 +138,7 @@ lemma mem
|
|||
lemma load
|
||||
cond (ex_is_pres_load_instr)
|
||||
|
||||
NoWe: have (spec_mem_read |-> ~data_we_o)
|
||||
NoWe: have (spec_mem_read & data_req_o |-> ~data_we_o)
|
||||
En: have (data_req_o |-> spec_mem_read)
|
||||
/
|
||||
SndEn: have (mem_req_snd_d |-> spec_mem_read_snd)
|
||||
|
|
@ -154,7 +154,7 @@ lemma load
|
|||
lemma store
|
||||
cond (ex_is_pres_store_instr)
|
||||
|
||||
We: have (spec_mem_write |-> data_we_o)
|
||||
We: have (spec_mem_write & data_req_o |-> data_we_o)
|
||||
En: have (data_req_o |-> spec_mem_write)
|
||||
/
|
||||
SndEn: have (mem_req_snd_d |-> spec_mem_write_snd)
|
||||
|
|
|
|||
|
|
@ -7,6 +7,8 @@
|
|||
# Original author: Louis-Emile Ploix
|
||||
# SPDX-License-Identifier: Apache-2.0
|
||||
|
||||
clear -all
|
||||
|
||||
set_prove_cache_path jgproofs
|
||||
set_prove_cache on
|
||||
set_prove_cache_mode coi
|
||||
|
|
@ -55,185 +57,67 @@ custom_engine -add -code hT3NZbhP9fmY2AbBQnsjfOxn6c+6e6yL+/e8fZFmaQrnlgEA
|
|||
|
||||
# prove -bg -all -covers
|
||||
|
||||
proc enter_stopat {} {
|
||||
stopat -reset {*}
|
||||
}
|
||||
|
||||
proc exit_stopat {} {
|
||||
stopat -reset -clear
|
||||
}
|
||||
|
||||
proc skip_mtypes {} {
|
||||
proc disable_mtypes {} {
|
||||
assert -disable {Step10::top.MType_*_Data}
|
||||
}
|
||||
|
||||
proc prove_lemmas {} {
|
||||
skip_mtypes
|
||||
proc prove_hps {task regex} {
|
||||
set props [get_property_list -task $task -include "disabled 0 type assert name $regex" -exclude "status proven"]
|
||||
set len [llength $props]
|
||||
for {set i 0} {$i <[llength $props]} {incr i 10} {
|
||||
for {set j 0} {$j < 10 && ($i + $j) < $len} {incr j} {
|
||||
set idx [expr {$i + $j}]
|
||||
prove -bg -property [lindex $props $idx] -engine_mode Hp
|
||||
}
|
||||
prove -wait
|
||||
}
|
||||
}
|
||||
|
||||
# TODO: Add liveness checking
|
||||
proc prove_no_liveness {} {
|
||||
disable_mtypes
|
||||
|
||||
prove -task Step0
|
||||
report -task Step0
|
||||
|
||||
prove -task Step1
|
||||
report -task Step1
|
||||
|
||||
prove -task Step2
|
||||
report -task Step2
|
||||
|
||||
prove -task Step3
|
||||
report -task Step3
|
||||
|
||||
prove -task Step4
|
||||
report -task Step4
|
||||
|
||||
prove -task Step5
|
||||
report -task Step5
|
||||
|
||||
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
|
||||
|
||||
prove -task Step7
|
||||
report -task Step7
|
||||
|
||||
prove -task Step8
|
||||
report -task Step8
|
||||
|
||||
prove -property {Step9::top.Arith_I_Fast Step9::top.Arith_R_Fast Step9::top.Arith_Shift_Fast Step9::top.CSR_Fast Step9::top.BType_FinishFirstCycle Step9::top.BType_Fast Step9::top.JType_FinishFirstCycle Step9::top.UType_Lui_Fast Step9::top.UType_Auipc_Fast Step9::top.Fence_Fence_Fast Step9::top.Fence_FenceI_Fast Step9::top.Special_ECall_Fast Step9::top.Special_EBreak_Fast Step9::top.Special_MRet_Fast Step9::top.WFI_Fast}
|
||||
prove -property {Step9::top.Mem_MemSpec_Initial Step9::top.Mem_MemSpec_Initial_IdleActive Step9::top.Mem_MemSpec_WaitRvalidMis_Step Step9::top.Mem_MemSpec_WaitRvalidMis_WaitRvalidMis_Inv Step9::top.Mem_MemSpec_WaitRvalidMis_WaitRvalidMisGntsDone_Inv Step9::top.Mem_MemSpec_WaitRvalidMis_WaitGntSplit_Inv Step9::top.Mem_MemSpec_WaitRvalidMis_Step_Inv Step9::top.Mem_MemSpec_WaitGntSplit_Step Step9::top.Mem_MemSpec_WaitGntSplit_WaitGntSplit_Inv Step9::top.Mem_MemSpec_WaitGntSplit_Step_Inv Step9::top.Mem_MemSpec_WaitGnt_Step Step9::top.Mem_MemSpec_WaitGnt_WaitGnt_Inv Step9::top.Mem_MemSpec_WaitGnt_Step_Inv Step9::top.Mem_MemSpec_WaitRvalidMisGntsDone_Step Step9::top.Mem_MemSpec_WaitRvalidMisGntsDone_WaitRvalidMisGntsDone_Inv Step9::top.Mem_MemSpec_WaitRvalidMisGntsDone_Step_Inv Step9::top.Mem_MemSpec_IdleActive_Step Step9::top.Mem_MemSpec_IdleActive_WaitRvalidMis_Inv Step9::top.Mem_MemSpec_IdleActive_WaitGntMis_Inv Step9::top.Mem_MemSpec_IdleActive_WaitGnt_Inv Step9::top.Mem_MemSpec_IdleActive_Step_Inv Step9::top.Mem_MemSpec_WaitGntMis_Step Step9::top.Mem_MemSpec_WaitGntMis_WaitGntMis_Inv Step9::top.Mem_MemSpec_WaitGntMis_WaitRvalidMis_Inv}
|
||||
prove -property {Step9::top.IRQ_PC Step9::top.IRQ_CSR}
|
||||
prove -property {Step9::top.Illegal_Fast Step9::top.FetchErr_Fast}
|
||||
prove -bg -task Step1
|
||||
prove -bg -task Step2
|
||||
prove -wait
|
||||
prove -bg -task Step3
|
||||
prove -bg -task Step4
|
||||
prove -bg -task Step5
|
||||
prove -wait
|
||||
prove -bg -property {Step6::*SpecStable*} -engine_mode Hp
|
||||
prove -bg -property {Step6::top.Ibex_FetchErrRoot}
|
||||
prove -bg -property {Step6::top.Ibex_PreNextPcMatch}
|
||||
prove -wait
|
||||
prove -bg -task Step6
|
||||
prove -bg -task Step7
|
||||
prove -bg -task Step8
|
||||
prove -wait
|
||||
prove_hps Step9 *MemSpec*
|
||||
prove_hps Step9 *CapFsm*
|
||||
prove -property {Step9::*.Mem_*}
|
||||
prove -task Step9
|
||||
report -task Step9
|
||||
|
||||
prove -property {Step10::top.Arith_I_NoErr Step10::top.Arith_R_NoErr Step10::top.Arith_Shift_NoErr Step10::top.CSR_Addr_NotErr Step10::top.CSR_Data_NotErr Step10::top.CSR_CSR_NotErr Step10::top.CSR_PC_NotErr Step10::top.CSR_Addr_Err Step10::top.CSR_Data_Err Step10::top.CSR_CSR_Err Step10::top.CSR_PC_Err}
|
||||
prove -property {Step10::top.BType_BInd_Initial Step10::top.BType_BInd_Initial_Stall Step10::top.BType_BInd_Initial_Oma Step10::top.BType_BInd_Initial_Progress Step10::top.BType_BInd_Stall_Step Step10::top.BType_BInd_Stall_Stall_Inv Step10::top.BType_BInd_Stall_Progress_Inv Step10::top.BType_BInd_Oma_Step_0 Step10::top.BType_BInd_Oma_Oma_Inv_0 Step10::top.BType_BInd_Oma_Progress_Inv_0 Step10::top.BType_BInd_Oma_Step_1 Step10::top.BType_BInd_Oma_Oma_Inv_1 Step10::top.BType_BInd_Oma_Progress_Inv_1}
|
||||
prove -property {Step10::top.JType_JInd_Initial Step10::top.JType_JInd_Initial_Stall Step10::top.JType_JInd_Initial_Oma Step10::top.JType_JInd_Initial_Progress Step10::top.JType_JInd_Stall_Step Step10::top.JType_JInd_Stall_Stall_Inv Step10::top.JType_JInd_Stall_Progress_Inv Step10::top.JType_JInd_Oma_Step Step10::top.JType_JInd_Oma_Oma_Inv Step10::top.JType_JInd_Oma_Progress_Inv}
|
||||
prove -property {Step10::top.UType_Lui_Addr Step10::top.UType_Lui_Data Step10::top.UType_Lui_CSR Step10::top.UType_Lui_PC Step10::top.UType_Auipc_Addr Step10::top.UType_Auipc_Data Step10::top.UType_Auipc_CSR Step10::top.UType_Auipc_PC}
|
||||
prove -property {Step10::top.Fence_Fence_Addr Step10::top.Fence_Fence_Data Step10::top.Fence_Fence_CSR Step10::top.Fence_Fence_PC Step10::top.Fence_FenceI_Addr Step10::top.Fence_FenceI_Data Step10::top.Fence_FenceI_CSR Step10::top.Fence_FenceI_PC}
|
||||
prove -property {Step10::top.Special_ECall_Addr Step10::top.Special_ECall_Data Step10::top.Special_ECall_CSR Step10::top.Special_ECall_PC Step10::top.Special_EBreak_Addr Step10::top.Special_EBreak_Data Step10::top.Special_EBreak_CSR Step10::top.Special_EBreak_PC Step10::top.Special_MRet_Addr Step10::top.Special_MRet_Data Step10::top.Special_MRet_CSR Step10::top.Special_MRet_PC}
|
||||
prove -property {Step10::top.WFI_Addr_NotErr Step10::top.WFI_Data_NotErr Step10::top.WFI_PC_NotErr Step10::top.WFI_CSR_NotErr}
|
||||
prove -property {Step10::top.WFI_Addr_Err Step10::top.WFI_Data_Err Step10::top.WFI_PC_Err Step10::top.WFI_CSR_Err}
|
||||
prove -property {Step10::top.Mem_MemSpec_IdleActive_Rev Step10::top.Mem_MemSpec_WaitGntMis_Rev Step10::top.Mem_MemSpec_WaitRvalidMis_Rev Step10::top.Mem_MemSpec_WaitGntSplit_Rev Step10::top.Mem_MemSpec_WaitGnt_Rev Step10::top.Mem_MemSpec_WaitRvalidMisGntsDone_Rev Step10::top.Mem_MemSpec_Step_Rev}
|
||||
prove -property {Step10::top.Illegal_Addr Step10::top.Illegal_Data Step10::top.Illegal_PC Step10::top.Illegal_CSR}
|
||||
prove -property {Step10::top.FetchErr_Addr Step10::top.FetchErr_Data Step10::top.FetchErr_PC Step10::top.FetchErr_CSR}
|
||||
prove -property {Step10::top.MType_Mul_Addr Step10::top.MType_Mul_CSR Step10::top.MType_Mul_PC Step10::top.MType_MulH_Addr Step10::top.MType_MulH_CSR Step10::top.MType_MulH_PC Step10::top.MType_MulHSH_Addr Step10::top.MType_MulHSH_CSR Step10::top.MType_MulHSH_CSR Step10::top.MType_MulHSH_PC Step10::top.MType_MulHU_Addr Step10::top.MType_MulHU_CSR Step10::top.MType_MulHU_PC}
|
||||
prove -property {Step10::top.MType_Div_Addr Step10::top.MType_Div_CSR Step10::top.MType_Div_PC Step10::top.MType_DivU_Addr Step10::top.MType_DivU_CSR Step10::top.MType_DivU_PC Step10::top.MType_Rem_Addr Step10::top.MType_Rem_CSR Step10::top.MType_Rem_PC Step10::top.MType_RemU_Addr Step10::top.MType_RemU_CSR Step10::top.MType_RemU_PC}
|
||||
prove -task Step10
|
||||
report -task Step10
|
||||
|
||||
prove -property {Step11::top.Arith_I_Addr Step11::top.Arith_I_Data Step11::top.Arith_I_CSR Step11::top.Arith_I_PC}
|
||||
prove -property {Step11::top.Arith_R_Addr Step11::top.Arith_R_Data Step11::top.Arith_R_CSR Step11::top.Arith_R_PC}
|
||||
prove -property {Step11::top.Arith_Shift_Addr Step11::top.Arith_Shift_Data Step11::top.Arith_Shift_CSR Step11::top.Arith_Shift_PC}
|
||||
prove -property {Step11::top.BType_BInd_Stall_Rev Step11::top.BType_BInd_Oma_Rev_0 Step11::top.BType_BInd_Oma_Rev_1 Step11::top.BType_BInd_Progress_Rev Step11::top.JType_JInd_Progress_Rev Step11::top.JType_JInd_Stall_Rev Step11::top.JType_JInd_Oma_Rev}
|
||||
prove -property {Step11::top.Mem_MemSpec_IdleActive Step11::top.Mem_MemSpec_WaitGntMis Step11::top.Mem_MemSpec_WaitRvalidMis Step11::top.Mem_MemSpec_WaitGntSplit Step11::top.Mem_MemSpec_WaitGnt Step11::top.Mem_MemSpec_WaitRvalidMisGntsDone Step11::top.Mem_MemSpec_Step}
|
||||
prove -task Step11
|
||||
report -task Step11
|
||||
|
||||
prove -property {Step10::*.BType_* Step10::*.JType_*}
|
||||
prove -property {Step10::*.Mem_*}
|
||||
prove_hps Step10 *
|
||||
prove -property {Step11::*.BType_* Step11::*.JType_* Step11::*.Mem_*}
|
||||
prove_hps Step11 *
|
||||
prove -task Step12
|
||||
report -task Step12
|
||||
|
||||
prove -task Step13
|
||||
report -task Step13
|
||||
|
||||
prove_hps Step14 *BType*
|
||||
prove -task Step14
|
||||
report -task Step14
|
||||
|
||||
prove_hps Step15 *JType*
|
||||
prove -task Step15
|
||||
report -task Step15
|
||||
|
||||
prove -task Step16
|
||||
report -task Step16
|
||||
|
||||
prove -task Step17
|
||||
report -task Step17
|
||||
|
||||
prove -task Step18
|
||||
report -task Step18
|
||||
|
||||
prove -property {Step19::top.Mem_L_*_Err}
|
||||
prove -property {Step19::top.Mem_L_*_NoErr}
|
||||
prove -property {Step19::top.Mem_L_*}
|
||||
prove -property {Step19::top.Mem_S_*_Err}
|
||||
prove -property {Step19::top.Mem_S_*_NoErr}
|
||||
prove -property {Step19::top.Mem_S_*}
|
||||
prove -task Step19
|
||||
report -task Step19
|
||||
}
|
||||
|
||||
proc prove_no_liveness {} {
|
||||
prove_lemmas
|
||||
|
||||
prove -bg -task Step16
|
||||
prove -bg -task Step17
|
||||
prove -bg -task Step18
|
||||
prove -wait
|
||||
prove_hps Step19 *
|
||||
prove -task Step20
|
||||
report -task Step20
|
||||
|
||||
prove -task Step21 -engine_mode D
|
||||
report -task Step21
|
||||
|
||||
prove -task Step22
|
||||
report -task Step22
|
||||
|
||||
prove -task Step23
|
||||
report -task Step23
|
||||
}
|
||||
|
||||
# TODO fix step numbers in here
|
||||
proc prove_liveness {} {
|
||||
prove_lemmas
|
||||
|
||||
prove -property {Step18::top.Liveness_*}
|
||||
prove -task Step18
|
||||
report -task Step18
|
||||
|
||||
prove -property Step19::top.Liveness_DivStart
|
||||
prove -property Step19::top.Liveness_DivMiddle
|
||||
prove -property Step19::top.Liveness_DivEnd
|
||||
prove -property Step19::top.Liveness_WFIStart
|
||||
prove -property Step19::top.Liveness_WFIMiddle
|
||||
prove -property Step19::top.Liveness_WFIEnd
|
||||
prove -property Step19::top.Liveness_NewProgNormal
|
||||
prove -property Step19::top.Liveness_NewProgMem
|
||||
prove -property Step19::top.Liveness_ProgReadyNormal
|
||||
prove -property Step19::top.Liveness_ProgReadyWFI
|
||||
prove -property Step19::top.Liveness_KillReady
|
||||
prove -property Step19::top.Liveness_ReadyNew
|
||||
prove -property Step19::top.Liveness_Initial
|
||||
prove -property Step19::top.Liveness_FlushedNoKill
|
||||
prove -task Step19
|
||||
report -task Step19
|
||||
|
||||
prove -task Step20
|
||||
report -task Step20
|
||||
|
||||
prove -task Step21
|
||||
report -task Step21
|
||||
|
||||
prove -task Step22
|
||||
report -task Step22
|
||||
|
||||
prove -task Step23
|
||||
report -task Step23
|
||||
|
||||
prove -task Step24
|
||||
report -task Step24
|
||||
|
||||
prove -task Step25
|
||||
report -task Step25
|
||||
|
||||
prove -task Step26
|
||||
report -task Step26
|
||||
|
||||
prove -task Step27
|
||||
report -task Step27
|
||||
|
||||
prove -task Step28
|
||||
report -task Step28
|
||||
|
||||
prove -task Step29
|
||||
report -task Step29
|
||||
|
||||
prove -property Step30::top.Live
|
||||
prove -task Step30 -engine_mode D
|
||||
report -task Step30
|
||||
prove_hps Step21 *
|
||||
prove -bg -task Step22
|
||||
prove -bg -task Step23
|
||||
prove -wait
|
||||
}
|
||||
|
||||
source build/psgen.tcl
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue