[Libre-soc-bugs] [Bug 565] Improve formal verification on PartitionedSignal

[bugzilla-daemon at libre-soc.org]

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

--- Comment #28 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #27)
> (In reply to Luke Kenneth Casson Leighton from comment #26)
> > done some() - worked! - Cesar could you take a look at the (new)
> > PartitionedXOR?
> > under bug #176.  it may need inverting of the input, or it may need
> > RippleMSB.
> 
> It needed both, RippleLSB (not RippleMSB) and inverting the output (not the
> input). 

wow that's very cool that it worked based on "guessing" :)

> Also, formally verifying it on 8-bit partitions seemed to take a
> really long time, but it quickly passed with 4-bit partitions.

fascinating.  that may be worthwhile looking at the ilang file in yosys
"show top", to see what the gate level looks like.

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