Verif: Formal testbench

scarv / xcrypto

XCrypto: a cryptographic ISE for RISC-V

MIT License

90 stars 10 forks source link

Closed ben-marshall closed 6 years ago

ben-marshall commented 6 years ago

Use the existing ISE model and checker to implement a formal testbench in using Yosys and Z3.

ben-marshall commented 6 years ago

Have had to split "preparation" of the model_ise.v file into a separate stage since it alone takes ~20mins to synthesise, while the entire design is only ~22 mins!
Resulting "prepped" ISE model is created as a dependency of all further formal flow stages.

ben-marshall commented 6 years ago

Managed to generate a 3 million line netlist of the model. I forgot to do any optimisation passes...

ben-marshall commented 6 years ago

Replacing model_do_read_cpr calls with straight up copy-assignments reduced the yosys IR design size from 42K elements to 35K elements! Noticibly faster to process now.

ben-marshall commented 6 years ago

New synthesised model is 42k lines down from 3 million...
New error when re-loading back into yosys the synthesised netlist is: "ERROR: Unsupported expression on dynamic range select on signal `\cop_insn_enc'!"

ben-marshall commented 6 years ago

Changed how model writes / updates CPRS. Use current/next value rather than just direct assignment. Now down to 27K elemnts from 42K.

ben-marshall commented 6 years ago

Problem synthesising netlist in to SMT2: Yosys cannot turn its internal shiftx cell into an SMT2 representation.
Solution was to flatten the design. The synthesiser then picks a different cell type.

ben-marshall commented 6 years ago

Abandoned use of simulation model for dedicated formal model.