git.libre-soc.org Git - ieee754fpu.git/history - src/ieee754/part/formal/proof

[ieee754fpu.git] / src / ieee754 / part / formal / proof_partition.py

2021-01-23	Cesar Strauss	Use z3 solver instead of yices2 when convenient	blob \| commitdiff \| raw
2021-01-20	Cesar Strauss	Add tests for bitwise logical operators	blob \| commitdiff \| raw \| diff to current
2021-01-17	Cesar Strauss	Fix PartitionedSignal.neg and its test case	blob \| commitdiff \| raw \| diff to current
2021-01-17	Cesar Strauss	Allow the proof driver to check operations with integer...	blob \| commitdiff \| raw \| diff to current
2021-01-16	Cesar Strauss	Use RipleLSB in PartitionedXOR, and invert outputs ls180-24jan2020	blob \| commitdiff \| raw \| diff to current
2021-01-16	Luke Kenneth Casso...	add first cut at formal proof for PartitionedXOR	blob \| commitdiff \| raw \| diff to current
2021-01-16	Cesar Strauss	Check PartitionedSignal.any().	blob \| commitdiff \| raw \| diff to current
2021-01-16	Cesar Strauss	Allow a variable number of operands in the proof driver	blob \| commitdiff \| raw \| diff to current
2021-01-10	Cesar Strauss	Implement checks for all the rest of the comparison...	blob \| commitdiff \| raw \| diff to current
2021-01-10	Cesar Strauss	Generate and check expected values for all possible...	blob \| commitdiff \| raw \| diff to current
2021-01-10	Cesar Strauss	Generate shifted down input and outputs	blob \| commitdiff \| raw \| diff to current
2021-01-10	Cesar Strauss	Use styles in write_gtkw to simplify the trace description	blob \| commitdiff \| raw \| diff to current
2021-01-10	Cesar Strauss	Add the Gate Generator to the ComparisonOpDriver	blob \| commitdiff \| raw \| diff to current
2021-01-10	Cesar Strauss	Factor-out the code to make equally spaced partition...	blob \| commitdiff \| raw \| diff to current
2021-01-10	Cesar Strauss	Start proof for PartitionedSignal equals operator	blob \| commitdiff \| raw \| diff to current
2021-01-08	Cesar Strauss	Calculate the expected value, test and assert	blob \| commitdiff \| raw \| diff to current
2021-01-08	Cesar Strauss	Split-out the gate generator from the proof	blob \| commitdiff \| raw \| diff to current
2021-01-07	Cesar Strauss	Compare the expected output for all partition sizes	blob \| commitdiff \| raw \| diff to current
2021-01-06	Cesar Strauss	Generate shifted down outputs	blob \| commitdiff \| raw \| diff to current
2021-01-05	Cesar Strauss	Generate the bit pattern of gates corresponding to...	blob \| commitdiff \| raw \| diff to current
2021-01-04	Cesar Strauss	Work only with nibbles on the ascending cascade	blob \| commitdiff \| raw \| diff to current
2021-01-04	Cesar Strauss	Fill the second nibble of the pattern	blob \| commitdiff \| raw \| diff to current
2021-01-04	Cesar Strauss	Restart the pattern at partition boundaries	blob \| commitdiff \| raw \| diff to current
2021-01-04	Cesar Strauss	Start work on improving formal verification of Partitio...	blob \| commitdiff \| raw \| diff to current

RSS Atom