[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 #23 from Cesar Strauss <cestrauss at gmail.com> ---
(In reply to Luke Kenneth Casson Leighton from comment #22)
> (In reply to Cesar Strauss from comment #21)
> > 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.  
> 
> 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)

Sure, sounds like a good idea.

Also good is the idea you mentioned of defining an op_all(obj) function that
returns obj.all().

More parameters can be added as needed to the driver, to cover more cases, like
whether the output is arithmetic or boolean, if it has carry or not (like
add_op and sub_op), and whether the shift operation is scalar or dynamic.

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