RoaLogic
Add Formal Verification and Fix Bug
Good day,
I added formal verification using the open source symbiyosys. There was a bug found: when the overall parity bit itself is corrupted, the sb_err flag is not triggered. The updated code fixed this error on ecc_dec.sv.
The formal verification can be run by just running ./run_formal.sh inside the ./formal directory. Just make sure the symbiyosys tool is installed on your system (recommended way is to install the OSS-CAD-SUITE : https://github.com/YosysHQ/oss-cad-suite-build/releases). Shown below is the summary report at the end:
The formal verification runs a set of tasks (shown on ecc.sby), where K is 8, 16,32, and 64. Proof for K=64 takes the longest time reaching almost one and a half hour.
The actual formal properties are very simple and is elaborated on ecc_formal.v. Basically, the main rule is that the information input received by ecc_enc must be the same as the information output from ecc_dec (in case of 0 or 1 flipped bits). If 2 flipped bits, then the db_err must be high.
I also added cover statement so we can have a sample waveform of this working design.
Thank you!
Kind regards, Angelo
ps: Awesome project by the way! The design is very simple but flexible! I'm planning to use this ECC for my open source DDR3 controller UberDDR3: https://github.com/AngeloJacobo/UberDDR3
ps: Included on these commits are the same ones from my PR: Fix failing VIvado Simulation since that PR is not yet accepted
