[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 #29 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #28)
> (In reply to Cesar Strauss from comment #27)
> > 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.

I suspect it has to do with the search space. On an OR-cascade (PartitionedEQ),
as soon as one bit equals one, the result becomes independent of the other
bits, and the search tree can be pruned. With an XOR-cascade (PartitionedXOR)
there is no such opportunity, it must follow every branch.

In other news: the proof driver now can also handle operations which give
arithmetic outputs. Addition and subtraction (without carry-in or out) passes.

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