Bug 312 - Formal Correctness Proof for CountZero needed (basically PriorityEncoder)
Summary: Formal Correctness Proof for CountZero needed (basically PriorityEncoder)
Alias: None
Product: Libre-SOC's first SoC
Classification: Unclassified
Component: Formal Verification (show other bugs)
Version: unspecified
Hardware: PC Mac OS
: --- enhancement
Assignee: Luke Kenneth Casson Leighton
Depends on:
Blocks: 311
  Show dependency treegraph
Reported: 2020-05-15 15:01 BST by Luke Kenneth Casson Leighton
Modified: 2021-04-20 14:44 BST (History)
1 user (show)

See Also:
NLnet milestone: NLNet.2019.10.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}


Note You need to log in before you can comment on or make changes to this bug.
Description Luke Kenneth Casson Leighton 2020-05-15 15:01:16 BST
a formal correctness proof is needed for POWER countzero.py


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*