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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Sat Jan 9 18:06:49 GMT 2021


https://bugs.libre-soc.org/show_bug.cgi?id=565

--- Comment #18 from Luke Kenneth Casson Leighton <lkcl at lkcl.net> ---
(In reply to Cesar Strauss from comment #17)

> Done!
> 
> It was very similar to PartitionedEq, just a few more lines to check the
> different opcodes.

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.

> By the way, I'm testing the full 64-bit width, 8 times 8-bit partitions. The
> run-time is still just a few seconds

cool!

> I will now proceed to work on the remaining operations.

shift and mul will be extremely long, thus is just normal.

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


More information about the libre-soc-bugs mailing list