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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #41 from Michael Nolan <mtnolan2640 at gmail.com> ---
(In reply to Cole Poirier from comment #40)

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

No, that is about what I would have written. What I would suggest to you is to
open the trace yosys generated (should be in
proof_bperm_formal/engine_0/trace.vcd) and see why it's not working.


Looking at it on my machine... double check that you're generating the `index`
correctly in the proof.

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