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