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