Bug 312 - Formal Correctness Proof for CountZero needed (basically PriorityEncoder)
Formal Correctness Proof for CountZero needed (basically PriorityEncoder)
 Status: PAYMENTPENDING FIXED None Libre-SOC's first SoC Unclassified Formal Verification (show other bugs) unspecified PC Mac OS --- enhancement Luke Kenneth Casson Leighton 311 Show dependency tree / graph

 Reported: 2020-05-15 15:01 BST by Luke Kenneth Casson Leighton 2021-04-20 14:44 BST (History) 1 user (show) libre-soc-bugs NLNet.2019.10.Formal 150 150 198 "lkcl"={amount=150, paid=2020-08-21}

Attachments

 Note You need to log in before you can comment on or make changes to this bug.
 Luke Kenneth Casson Leighton 2020-05-15 15:01:16 BST ```a formal correctness proof is needed for POWER countzero.py https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/formal/proof_clz.py;hb=HEAD the majority of that is actually a proof for PriorityEncoder, with the rest taking care of niggles surrounding starting the count from the MSB rather than the LSB, and 64/32 bit mode the basis of the proof is a for-loop: for i in range(64) - or 32 with m.If(result == i): Assert(input[i] == 1) -- assert that the bit in the input is a 1 Assert(input & (1<<(i-1)-1) == 0 -- all bits below must be zero this is basically the count done in a different way, however the important bit about the proof is that it operates "inverted" from the actual computation. it starts from the *result* condition - result == i - and based on that result, analyses (performs Assertions) on the *input*.``` Luke Kenneth Casson Leighton 2020-05-19 17:30:56 BST ```this is now definitely a formal proof for PriorityEncoder because countzero.py is not used, replaced by use of nmutil.clz. however, nmutil.clz *is* PriorityEncoder.```