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

bugzilla-daemon at libre-soc.org bugzilla-daemon at libre-soc.org
Fri Jan 8 18:47:00 GMT 2021


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

--- Comment #8 from Cesar Strauss <cestrauss at gmail.com> ---
The story so far:

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

* Implemented a partitioned pattern generator
* Implemented a prover, using the above as a test case

Next:

* Make the prover generic, avoiding repetition on the next proofs
* Implement proofs of the remaining partitioned operations

This code assumes equally spaced partition points. Otherwise it would have to
loop over all possible start and end points, instead of just the possible
widths, making it O(n^3).

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


More information about the libre-soc-bugs mailing list