Formal proofs turn out to provide 100% code-coverage if written correctly, whereas standard testbench units tests typically do not, even when dozens, hundreds or tens of thousands are provided. Therefore, to greatly simplify the development and also increase effectiveness of unit tests, formal proofs are to be written on the low-level HDL libraries used in Libre-SOC. this includes nmutil and the SoC code itself. This is *different* from the *high-level* formal correctness proofs (bug #194 and bug #195) https://git.libre-riscv.org/?p=nmutil.git;a=summary https://git.libre-riscv.org/?p=soc.git;a=summary nmutil: * DONE picker #901 * DONE byterev #902 * DONE plru #909 * DONE queue #903 * DONE lut already done as part of bug #745 * DONE pop-count #904 clz already has one soc: * identify any lowlevel modules and move them to nmutil (popcount to be left in soc due to PowerISA-specificity) * https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/logical/formal/proof_main_stage.py;hb=HEAD also update,Copyright, Trademark, and Grant notices. all files.
https://gitlab.com/nmigen/nmigen/-/blob/master/nmigen/lib/fifo.py#L177 https://gitlab.com/nmigen/nmigen/-/blob/master/tests/test_lib_fifo.py#L240 these are the formal proofs of SyncFIFO and Queue is literally and exactly compliant in almost all its modes (i.e. Queue provides more modes than SyncFIFO)
lut formal proof was already completed months ago as part of: https://bugs.libre-soc.org/show_bug.cgi?id=745
correctness proofs of nmutil lowlevel all good.
lkcl: please explain why red gets more than I did even though iirc i did >90% of the work...marking as in-progress because this needs to be addressed before you try and submit RFPs
(In reply to Jacob Lifshay from comment #4) > lkcl: please explain why red gets more than I did even though iirc i did > >90% of the work...marking as in-progress because this needs to be addressed > before you try and submit RFPs lkcl explained this to me privately.