[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 #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/partsig.py;h=53561d4bcc97c0dca31981261428b48d2e69dfff;hb=0bbad62934298fa33b05b655e9b34a4ab7d58bc0#l286

> 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
ob111111/0b00000

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
take.
https://stackoverflow.com/questions/847936/how-can-i-find-the-number-of-arguments-of-a-python-function

blech.

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.