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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Mon Jan 11 00:09:52 GMT 2021


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

fantastic.  could you try PartitionedSignal.all() as well?


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

wait.. wheer.... how come you can use Repl() on the LSB, at line 380, and it
produces the right answer? :)

i thought that PS.Ge/Le/Eq was returning 0b000001/0b00000 rather than

ah well :)

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

PartitionedSignal.all() should also be returning a predicate-like
(partition-like) signal.  

it's one op - there is a way to detect the number of arguments a function can


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)

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

More information about the libre-soc-bugs mailing list