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

[bugzilla-daemon@libre-soc.org]

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

--- Comment #43 from Michael Nolan <mtnolan2640@gmail.com> ---
(In reply to Cole Poirier from comment #42)
> (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?

For a combinatorial circuit like this one, the inputs (rs and rb) are set to
their initial values, and the outputs (ra) are set to whatever the circuit
calculates from the inputs.

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


In the proof, you're generating the index from rb, but in the actual module and
the Power spec, it's generated from rs. That's why the proof fails. If you look
at the index variables (for me it's index 6), you'll notice that one is less
than 64 - that's how I figured it out.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
_______________________________________________
libre-riscv-dev mailing list
libre-riscv-dev@lists.libre-riscv.org
http://lists.libre-riscv.org/mailman/listinfo/libre-riscv-dev