Skip to content

Commit 54c44f4

Browse files
mndstrmrmndstrmr
committed
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.
1 parent 2130ec5 commit 54c44f4

File tree

6 files changed

+63
-213
lines changed

6 files changed

+63
-213
lines changed

‎dv/formal/Makefile

-3
Original file line numberDiff line numberDiff line change
@@ -20,8 +20,6 @@ SAIL_SV_FLAGS=-sv -sv-comb -sv-inregs -sv-outregs -sv-nostrings -sv-nopacked -sv
2020

2121
# Use fusesoc to resolve the tree of components, copy all resolved source files into the build/ directory,
2222
# and then generate a filelist for jasper to ingest.
23-
# Finally, apply a number of small RTL patches necessary to make the formal flow work. (see files in patches/)
24-
# (Only patch the duplicated source files that fusesoc has copied into build/fusesoc/src, not the version-controlled originals)
2523
# - Note. we use the 'vcs' fusesoc backend flow to generate the filelist. This is because fusesoc does not currently implement a
2624
# JasperGold backend, but this is not an issue as the file-format generated by the vcs flow is compatible with jasper.
2725
.PHONY: fusesoc
@@ -34,7 +32,6 @@ fusesoc:
3432
--tool vcs \
3533
--setup \
3634
lowrisc:ibex:ibex_formal:0.1
37-
patch -p0 < patches/ibex_top.diff
3835

3936
.PHONY: sv
4037
sv:

‎dv/formal/check/top.sv

-2
Original file line numberDiff line numberDiff line change
@@ -134,8 +134,6 @@ WFIStart: assume property (`IDC.ctrl_fsm_cs == SLEEP |-> (
134134
`CSR.mie_q.irq_timer |
135135
`CSR.mie_q.irq_external
136136
));
137-
// 5. Disable clock gating
138-
TestEn: assume property (test_en_i);
139137
// See protocol/* for further assumptions
140138

141139
///////////////////////////////// Declarations /////////////////////////////////

‎dv/formal/patches/ibex_top.diff

-31
This file was deleted.

‎dv/formal/thm/ibex.proof

+10-8
Original file line numberDiff line numberDiff line change
@@ -13,7 +13,8 @@ lemma ibex
1313
PrivMorUMpp: have ((`CSR.mstatus_q.mpp == PRIV_LVL_U) || (`CSR.mstatus_q.mpp == PRIV_LVL_M))
1414
PrivMorUCur: have ((`CSR.priv_lvl_q == PRIV_LVL_U) || (`CSR.priv_lvl_q == PRIV_LVL_M))
1515

16-
PCBit0: have (~`CR.pc_id[0])
16+
PCBit0: have (`ID.instr_valid_i -> ~`CR.pc_id[0])
17+
MEPCBit0: have (~`CSR.mepc_q[0])
1718
MtvecLow: have (pre_mtvec[7:0] == 8'h01)
1819
NmiMode: have (~`IDC.nmi_mode_q)
1920
EBreakIntoDebug: have (~`IDC.ebreak_into_debug)
@@ -26,7 +27,7 @@ lemma ibex
2627
ReqRequiresInstr: have (data_req_o |-> ex_has_compressed_instr)
2728
ReqRequiresNotIllegal: have (data_req_o |-> ~`CR.illegal_insn_id & ~`CR.illegal_c_insn_id)
2829

29-
AluInstrMatch: have (`CR.instr_rdata_id == `CR.instr_rdata_alu_id)
30+
AluInstrMatch: have (`ID.instr_valid_i |-> `CR.instr_rdata_id == `CR.instr_rdata_alu_id)
3031

3132
IdExNotReq: have (~ex_is_mem_instr -> ~data_req_o)
3233
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
6465
ProgressNoWbStall: have (instr_will_progress |-> ~`IDC.stall_wb_i)
6566

6667
NoStoreWb: have (`WBG.wb_instr_type_q == WB_INSTR_STORE |-> ~`WB.rf_we_wb_o)
67-
WbInstrDefined: have (`WBG.wb_instr_type_q != 2'b11)
68+
WbInstrDefined: have (`WBG.wb_valid_q |-> `WBG.wb_instr_type_q != 2'b11)
6869

6970
RfWriteWb: have (`CR.rf_write_wb & wbexc_finishing |-> `WB.rf_we_wb_o)
7071

@@ -125,7 +126,8 @@ lemma ibex
125126
Memory: graph_induction +rev
126127
inv idle (
127128
~`LSU.handle_misaligned_q &&
128-
`CR.lsu_resp_valid == outstanding_mem
129+
`CR.lsu_resp_valid == outstanding_mem &&
130+
data_mem_assume.outstanding_reqs == data_gnt_i
129131
)
130132
inv idle_active (
131133
data_mem_assume.outstanding_reqs == data_gnt_i &&
@@ -163,7 +165,7 @@ lemma ibex
163165

164166
entry ($rose(rst_ni)) -> idle
165167

166-
node idle idle (`LSU.ls_fsm_cs == `LSU.IDLE && data_mem_assume.outstanding_reqs == data_gnt_i)
168+
node idle idle (`LSU.ls_fsm_cs == `LSU.IDLE && ~`IDG.outstanding_memory_access && (`ID.lsu_req_dec || ~`ID.lsu_req_done_i))
167169
edge idle => idle
168170
edge idle -> idle_active
169171

@@ -192,7 +194,7 @@ lemma ibex
192194
node step_fail step_fail (`LSU.lsu_req_done_o && `LSU.pmp_err_d)
193195
edge step_fail => fail
194196

195-
node wait wait (has_resp_waiting_q && ~`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && ~instr_will_progress)
197+
node wait wait (`IDG.outstanding_memory_access && ~`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && ~instr_will_progress)
196198
edge wait => wait end
197199

198200
node end end (`CR.lsu_resp_valid && `LSU.ls_fsm_cs == `LSU.IDLE && data_rvalid_i)
@@ -248,8 +250,8 @@ lemma ibex
248250

249251
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)
250252

251-
LoadNotSpecWrite: have (ex_is_pres_load_instr |-> ~spec_mem_write)
252-
StoreNotSpecRead: have (ex_is_pres_store_instr |-> ~spec_mem_read)
253+
LoadNotSpecWrite: have (`ID.instr_valid_i & ex_is_pres_load_instr |-> ~spec_mem_write)
254+
StoreNotSpecRead: have (`ID.instr_valid_i & ex_is_pres_store_instr |-> ~spec_mem_read)
253255

254256
FirstCycleNoGnt: have (`ID.instr_first_cycle |-> ~mem_gnt_fst_q)
255257
MemStartFirstCycle: have (`LSU.ls_fsm_cs == `LSU.IDLE && `CR.lsu_req |-> `ID.instr_first_cycle)

‎dv/formal/thm/mem.proof

+2-2
Original file line numberDiff line numberDiff line change
@@ -138,7 +138,7 @@ lemma mem
138138
lemma load
139139
cond (ex_is_pres_load_instr)
140140

141-
NoWe: have (spec_mem_read |-> ~data_we_o)
141+
NoWe: have (spec_mem_read & data_req_o |-> ~data_we_o)
142142
En: have (data_req_o |-> spec_mem_read)
143143
/
144144
SndEn: have (mem_req_snd_d |-> spec_mem_read_snd)
@@ -154,7 +154,7 @@ lemma load
154154
lemma store
155155
cond (ex_is_pres_store_instr)
156156

157-
We: have (spec_mem_write |-> data_we_o)
157+
We: have (spec_mem_write & data_req_o |-> data_we_o)
158158
En: have (data_req_o |-> spec_mem_write)
159159
/
160160
SndEn: have (mem_req_snd_d |-> spec_mem_write_snd)

‎dv/formal/verify.tcl

+51-167
Original file line numberDiff line numberDiff line change
@@ -7,6 +7,8 @@
77
# Original author: Louis-Emile Ploix
88
# SPDX-License-Identifier: Apache-2.0
99

10+
clear -all
11+
1012
set_prove_cache_path jgproofs
1113
set_prove_cache on
1214
set_prove_cache_mode coi
@@ -55,185 +57,67 @@ custom_engine -add -code hT3NZbhP9fmY2AbBQnsjfOxn6c+6e6yL+/e8fZFmaQrnlgEA
5557

5658
# prove -bg -all -covers
5759

58-
proc enter_stopat {} {
59-
stopat -reset {*}
60-
}
61-
62-
proc exit_stopat {} {
63-
stopat -reset -clear
60+
proc disable_mtypes {} {
61+
assert -disable {Step10::top.MType_*_Data}
6462
}
6563

66-
proc skip_mtypes {} {
67-
assert -disable {Step10::top.MType_*_Data}
64+
proc prove_hps {task regex} {
65+
set props [get_property_list -task $task -include "disabled 0 type assert name $regex" -exclude "status proven"]
66+
set len [llength $props]
67+
for {set i 0} {$i <[llength $props]} {incr i 10} {
68+
for {set j 0} {$j < 10 && ($i + $j) < $len} {incr j} {
69+
set idx [expr {$i + $j}]
70+
prove -bg -property [lindex $props $idx] -engine_mode Hp
71+
}
72+
prove -wait
73+
}
6874
}
6975

70-
proc prove_lemmas {} {
71-
skip_mtypes
76+
# TODO: Add liveness checking
77+
proc prove_no_liveness {} {
78+
disable_mtypes
7279

7380
prove -task Step0
74-
report -task Step0
75-
76-
prove -task Step1
77-
report -task Step1
78-
79-
prove -task Step2
80-
report -task Step2
81-
82-
prove -task Step3
83-
report -task Step3
84-
85-
prove -task Step4
86-
report -task Step4
87-
88-
prove -task Step5
89-
report -task Step5
90-
91-
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
92-
prove -task Step6
93-
report -task Step6
94-
95-
prove -task Step7
96-
report -task Step7
97-
98-
prove -task Step8
99-
report -task Step8
100-
101-
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}
102-
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}
103-
prove -property {Step9::top.IRQ_PC Step9::top.IRQ_CSR}
104-
prove -property {Step9::top.Illegal_Fast Step9::top.FetchErr_Fast}
81+
prove -bg -task Step1
82+
prove -bg -task Step2
83+
prove -wait
84+
prove -bg -task Step3
85+
prove -bg -task Step4
86+
prove -bg -task Step5
87+
prove -wait
88+
prove -bg -property {Step6::*SpecStable*} -engine_mode Hp
89+
prove -bg -property {Step6::top.Ibex_FetchErrRoot}
90+
prove -bg -property {Step6::top.Ibex_PreNextPcMatch}
91+
prove -wait
92+
prove -bg -task Step6
93+
prove -bg -task Step7
94+
prove -bg -task Step8
95+
prove -wait
96+
prove_hps Step9 *MemSpec*
97+
prove_hps Step9 *CapFsm*
98+
prove -property {Step9::*.Mem_*}
10599
prove -task Step9
106-
report -task Step9
107-
108-
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}
109-
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}
110-
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}
111-
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}
112-
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}
113-
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}
114-
prove -property {Step10::top.WFI_Addr_NotErr Step10::top.WFI_Data_NotErr Step10::top.WFI_PC_NotErr Step10::top.WFI_CSR_NotErr}
115-
prove -property {Step10::top.WFI_Addr_Err Step10::top.WFI_Data_Err Step10::top.WFI_PC_Err Step10::top.WFI_CSR_Err}
116-
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}
117-
prove -property {Step10::top.Illegal_Addr Step10::top.Illegal_Data Step10::top.Illegal_PC Step10::top.Illegal_CSR}
118-
prove -property {Step10::top.FetchErr_Addr Step10::top.FetchErr_Data Step10::top.FetchErr_PC Step10::top.FetchErr_CSR}
119-
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}
120-
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}
121-
prove -task Step10
122-
report -task Step10
123-
124-
prove -property {Step11::top.Arith_I_Addr Step11::top.Arith_I_Data Step11::top.Arith_I_CSR Step11::top.Arith_I_PC}
125-
prove -property {Step11::top.Arith_R_Addr Step11::top.Arith_R_Data Step11::top.Arith_R_CSR Step11::top.Arith_R_PC}
126-
prove -property {Step11::top.Arith_Shift_Addr Step11::top.Arith_Shift_Data Step11::top.Arith_Shift_CSR Step11::top.Arith_Shift_PC}
127-
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}
128-
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}
129-
prove -task Step11
130-
report -task Step11
131-
100+
prove -property {Step10::*.BType_* Step10::*.JType_*}
101+
prove -property {Step10::*.Mem_*}
102+
prove_hps Step10 *
103+
prove -property {Step11::*.BType_* Step11::*.JType_* Step11::*.Mem_*}
104+
prove_hps Step11 *
132105
prove -task Step12
133-
report -task Step12
134-
135106
prove -task Step13
136-
report -task Step13
137-
107+
prove_hps Step14 *BType*
138108
prove -task Step14
139-
report -task Step14
140-
109+
prove_hps Step15 *JType*
141110
prove -task Step15
142-
report -task Step15
143-
144-
prove -task Step16
145-
report -task Step16
146-
147-
prove -task Step17
148-
report -task Step17
149-
150-
prove -task Step18
151-
report -task Step18
152-
153-
prove -property {Step19::top.Mem_L_*_Err}
154-
prove -property {Step19::top.Mem_L_*_NoErr}
155-
prove -property {Step19::top.Mem_L_*}
156-
prove -property {Step19::top.Mem_S_*_Err}
157-
prove -property {Step19::top.Mem_S_*_NoErr}
158-
prove -property {Step19::top.Mem_S_*}
159-
prove -task Step19
160-
report -task Step19
161-
}
162-
163-
proc prove_no_liveness {} {
164-
prove_lemmas
165-
166-
prove -task Step20
167-
report -task Step20
168-
169-
prove -task Step21 -engine_mode D
170-
report -task Step21
171-
172-
prove -task Step22
173-
report -task Step22
174-
175-
prove -task Step23
176-
report -task Step23
177-
}
178-
179-
# TODO fix step numbers in here
180-
proc prove_liveness {} {
181-
prove_lemmas
182-
183-
prove -property {Step18::top.Liveness_*}
184-
prove -task Step18
185-
report -task Step18
186-
187-
prove -property Step19::top.Liveness_DivStart
188-
prove -property Step19::top.Liveness_DivMiddle
189-
prove -property Step19::top.Liveness_DivEnd
190-
prove -property Step19::top.Liveness_WFIStart
191-
prove -property Step19::top.Liveness_WFIMiddle
192-
prove -property Step19::top.Liveness_WFIEnd
193-
prove -property Step19::top.Liveness_NewProgNormal
194-
prove -property Step19::top.Liveness_NewProgMem
195-
prove -property Step19::top.Liveness_ProgReadyNormal
196-
prove -property Step19::top.Liveness_ProgReadyWFI
197-
prove -property Step19::top.Liveness_KillReady
198-
prove -property Step19::top.Liveness_ReadyNew
199-
prove -property Step19::top.Liveness_Initial
200-
prove -property Step19::top.Liveness_FlushedNoKill
201-
prove -task Step19
202-
report -task Step19
203-
111+
prove -bg -task Step16
112+
prove -bg -task Step17
113+
prove -bg -task Step18
114+
prove -wait
115+
prove_hps Step19 *
204116
prove -task Step20
205-
report -task Step20
206-
207-
prove -task Step21
208-
report -task Step21
209-
210-
prove -task Step22
211-
report -task Step22
212-
213-
prove -task Step23
214-
report -task Step23
215-
216-
prove -task Step24
217-
report -task Step24
218-
219-
prove -task Step25
220-
report -task Step25
221-
222-
prove -task Step26
223-
report -task Step26
224-
225-
prove -task Step27
226-
report -task Step27
227-
228-
prove -task Step28
229-
report -task Step28
230-
231-
prove -task Step29
232-
report -task Step29
233-
234-
prove -property Step30::top.Live
235-
prove -task Step30 -engine_mode D
236-
report -task Step30
117+
prove_hps Step21 *
118+
prove -bg -task Step22
119+
prove -bg -task Step23
120+
prove -wait
237121
}
238122

239123
source build/psgen.tcl

0 commit comments

Comments
 (0)