[libre-riscv-dev] [Bug 316] bperm TODO

[bugzilla-daemon at libre-soc.org]

https://bugs.libre-soc.org/show_bug.cgi?id=316

--- Comment #40 from Cole Poirier <colepoirier at gmail.com> ---
Hi Michael, I have finally run the formal proof 'proof_bperm.py' and gotten a
failure with the following in its output:

```
SBY 15:20:39 [proof_bperm_formal] engine_0: ##   0:00:00  BMC failed!
SBY 15:20:39 [proof_bperm_formal] engine_0: ##   0:00:00  Value for anyconst in
top (proof_bperm.py:56): 15481123719086080
SBY 15:20:39 [proof_bperm_formal] engine_0: ##   0:00:00  Value for anyconst in
top (proof_bperm.py:57): 36028797018963968
SBY 15:20:39 [proof_bperm_formal] engine_0: ##   0:00:00  Assert failed in top:
proof_bperm.py:93
```

I feel like I have misunderstood your directions for proving property #2, am I
extracting the indices incorrectly? Or am I making a different fundamental
mistake?

  84         # Now we need to prove property #2. I'm going to leave this to
  85         # you Cole. I'd start by writing a for loop and extracting the
  86         # 8 indices into signals. Then I'd write an if statement
  87         # checking if the index is >= 64 (it's hardware, so use an
  88         # m.If()). Finally, I'd add an assert that checks whether
  89         # ra[i] is equal to 0
  90         for i in range(8):
  91             index = rb[i*8:i*8+8]
  92             with m.If(index >= 64):
  93                 comb += Assert(ra[i] == 0)
  94 
  95 
  96         return m

-- 
You are receiving this mail because:
You are on the CC list for the bug.