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] Performance improvement for divide PC

Browse source 
The MType_{Div,DivU,Rem,RemU}_PC properties were proving very slow
before this. They were proving with Hp 45, which was very slow. This
change groups them together so that the engines can help each other out,
the N engine helps with proving these properties much faster than with
Hp alone. In the long-term it is better to capture a relavant assumption
in the proof files instead of putting this in the TCL script.
This commit is contained in:
Marno van der Maas 2025-05-08 17:26:12 +02:00 • committed by Marno van der Maas
parent 8a3d46f095
commit 4fe6b7d53f
1 changed files with 1 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

1
dv/formal/verify.tcl
View file

@ -99,6 +99,7 @@ proc prove_no_liveness {} {
prove -task Step9
prove -property {Step10::*.BType_* Step10::*.JType_*}
prove -property {Step10::*.Mem_*}
prove -property {Step10::top.MType_Div*_Addr Step10::top.MType_Div*_CSR Step10::top.MType_Div*_PC Step10::top.MType_Rem*_Addr Step10::top.MType_Rem*_CSR Step10::top.MType_Rem*_PC}
prove_hps Step10 *
prove -property {Step11::*.BType_* Step11::*.JType_* Step11::*.Mem_*}
prove_hps Step11 *