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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Tue May 19 00:12:02 BST 2020


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

More information about the libre-riscv-dev mailing list