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

https://git.libre-soc.org/?p=ieee754fpu.git;a=blob;f=src/ieee754/part/formal/proof_partition.py;h=f257d0243b897456d4aded6de62b5d12cae2e1db;hb=HEAD#l459

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.