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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Sun Jan 10 22:18:35 GMT 2021


--- Comment #21 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #18)
> (In reply to Cesar Strauss from comment #17)
> excellent.  yes it should be pretty easy, if abstracted out.  you shouuld be
> able to use python operator class.  operator.eq, etc. just pass that in as a
> parameter and "apply" it to both the PartitionedSignal *and* the Signal to
> assert against.

Done, for all comparison operators.


This proof driver can only accept comparison operators, because it assumes the
output is "predicate-like" (1-bit partitions), and it applies the ripple to its
expected value.

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

More information about the libre-soc-bugs mailing list