[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 #30 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #29)

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

ah true.

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

fantastic.  that's a great addition (pun intended).  neg is the next obvious
one, and "or", "and", "not" and "implies" should be trivial but important to
add for completeness.

shift: likewise, but these are expected to take a looong time, it may be better
to add them as separate independent unit tests.

oh.  one important code-path: RHS (operand 2) as:

* Const
* Signal
* PartitionedSignal

Shift in particular is commmpletely different when passed in a global Const or
a global (nonpartitioned) Signal.

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