[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 #24 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #22)
> PartitionedSignal.all() should also be returning a predicate-like
> (partition-like) signal.  

> or... just a number of args are passed in (1,2,3) and it's a list
> rather than a,b, it's arglist=[] then use self.op(*arglist)

It works! The proof driver can now accept unary operations (returning a
partition-like result).

PartitionedSignal.all() passes. Congratulations!

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

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