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*.

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.