Bug 312

Summary: Formal Correctness Proof for CountZero needed (basically PriorityEncoder)
Product: Libre-SOC's first SoC Reporter: Luke Kenneth Casson Leighton <lkcl>
Component: Formal VerificationAssignee: Luke Kenneth Casson Leighton <lkcl>
Status: PAYMENTPENDING FIXED    
Severity: enhancement CC: libre-soc-bugs
Priority: ---    
Version: unspecified   
Hardware: PC   
OS: Mac OS   
See Also: https://bugs.libre-soc.org/show_bug.cgi?id=311
https://bugs.libre-soc.org/show_bug.cgi?id=326
NLnet milestone: NLNet.2019.10.032.Formal total budget (EUR) for completion of task and all subtasks: 150
budget (EUR) for this task, excluding subtasks' budget: 150 parent task for budget allocation: 198
child tasks for budget allocation: The table of payments (in EUR) for this task; TOML format:
"lkcl"={amount=150, paid=2020-08-21}
Bug Depends on:    
Bug Blocks: 311    

Description 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*.
Comment 1 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.