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

[bugzilla-daemon at libre-soc.org]

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

--- Comment #42 from Cole Poirier <colepoirier at gmail.com> ---
(In reply to Michael Nolan from comment #41)
> 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.

When I look at trace.vcd by running 'gtkwave
proof_bperm_formal/engine_0/trace.vcd' and clicking to expose the bperm module
under top, then selecting and adding all the wires, all I see is, what I
presume out of ignorance is the initial state of the wires, and I can advance
to the next edge where the wires are in their 'final' state, and that's it...
I'm assuming since this is a combinatorial single cycle proof that's what I'm
supposed to see? How should I be reading the gtkwave diagram in order to
diagnose that index is not being set correctly in the proof?

Above, you said that doing 'index = rb[i*8:i*8+8]' within a for loop where i
counts from 0 to 7 was what you would have done... is this shown by the vcd
output to now be incorrect? How would I go about discerning that I'm generating
the `index` correctly in the proof? I'm sorry that these are stupid questions
that likely have obvious answers, but I'm struggling to determine them on my
own reading through the gtkwave manual.

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