git.libre-soc.org Git - soc.git/history - src/soc/fu/shift_rot/formal/proof_main

[soc.git] / src / soc / fu / shift_rot / formal / proof_main_stage.py

2023-09-12	Jacob Lifshay	remove grev, leaving tests for later use with grevlut	blob \| commitdiff \| raw
2022-02-24	Jacob Lifshay	add running instructions	blob \| commitdiff \| raw \| diff to current
2022-02-24	Jacob Lifshay	add formal proof for shift/rot o.ok	blob \| commitdiff \| raw \| diff to current
2022-02-24	Jacob Lifshay	clean up code	blob \| commitdiff \| raw \| diff to current
2022-02-24	Jacob Lifshay	add formal proof for OP_RLCR	blob \| commitdiff \| raw \| diff to current
2022-02-24	Jacob Lifshay	add formal proof for OP_RLCL	blob \| commitdiff \| raw \| diff to current
2022-02-24	Jacob Lifshay	add formal proof for OP_RLC	blob \| commitdiff \| raw \| diff to current
2022-02-22	Jacob Lifshay	speed up shift/rot formal proof by running stuff in...	blob \| commitdiff \| raw \| diff to current
2022-02-18	Jacob Lifshay	add grev	blob \| commitdiff \| raw \| diff to current
2021-12-10	Jacob Lifshay	add ternlogi to shift_rot formal test	blob \| commitdiff \| raw \| diff to current
2021-12-10	Jacob Lifshay	fix shift_rot formal proof	blob \| commitdiff \| raw \| diff to current
2021-12-09	Jacob Lifshay	add parent_pspec everywhere	blob \| commitdiff \| raw \| diff to current
2021-12-09	Jacob Lifshay	format code	blob \| commitdiff \| raw \| diff to current
2021-04-23	Luke Kenneth Casso...	more openpower-isa conversion	blob \| commitdiff \| raw \| diff to current
2021-04-23	Luke Kenneth Casso...	move over to from openpower imports	blob \| commitdiff \| raw \| diff to current
2020-09-07	Luke Kenneth Casso...	whoops truncated the mb and me fields	blob \| commitdiff \| raw \| diff to current
2020-08-21	Cole Poirier	Merge branch 'master' of git.libre-soc.org:soc	blob \| commitdiff \| raw \| diff to current
2020-08-19	Luke Kenneth Casso...	rename and document fields in shift_rot proof	blob \| commitdiff \| raw \| diff to current
2020-08-03	Samuel A. Falvo II	WIP: check MB > ME and select mask appropriately	blob \| commitdiff \| raw \| diff to current
2020-08-01	Luke Kenneth Casso...	line-length / whitespace	blob \| commitdiff \| raw \| diff to current
2020-08-01	Luke Kenneth Casso...	expand out for-loop setting up input record subset	blob \| commitdiff \| raw \| diff to current
2020-07-31	Samuel A. Falvo II	WIP: more debugging signals for inspection	blob \| commitdiff \| raw \| diff to current
2020-07-30	Samuel A. Falvo II	WIP: rlwinm/rlwnm/rlwimi-type proofs	blob \| commitdiff \| raw \| diff to current
2020-07-28	Jacob Lifshay	Merge remote-tracking branch 'origin/master'	blob \| commitdiff \| raw \| diff to current
2020-07-28	Luke Kenneth Casso...	use ctx.op compare (and muxid) in shiftrot proof	blob \| commitdiff \| raw \| diff to current
2020-07-14	Luke Kenneth Casso...	set up masks for OP_RL* formal proof	blob \| commitdiff \| raw \| diff to current
2020-07-13	Luke Kenneth Casso...	formal proof of OP_EXTSWSLI	blob \| commitdiff \| raw \| diff to current
2020-07-13	Luke Kenneth Casso...	comments	blob \| commitdiff \| raw \| diff to current
2020-07-13	Luke Kenneth Casso...	attempting formal proof of OP_EXTSWSLI	blob \| commitdiff \| raw \| diff to current
2020-07-13	Luke Kenneth Casso...	add EXTSWSLI "pass" to formal shift_rot proof	blob \| commitdiff \| raw \| diff to current
2020-07-12	Luke Kenneth Casso...	rename InternalOp to MicrOp	blob \| commitdiff \| raw \| diff to current
2020-06-04	Luke Kenneth Casso...	use copy of FHDLTestCase	blob \| commitdiff \| raw \| diff to current
2020-05-27	Luke Kenneth Casso...	check reg output Data.ok in shift_rot formal proof	blob \| commitdiff \| raw \| diff to current
2020-05-22	Luke Kenneth Casso...	add TODO and link to SHIFT_ROT formal bugreport	blob \| commitdiff \| raw \| diff to current
2020-05-22	Luke Kenneth Casso...	remove xer.so from ShiftRot formal proof	blob \| commitdiff \| raw \| diff to current
2020-05-22	Luke Kenneth Casso...	create common input pipe spec to avoid code-duplication	blob \| commitdiff \| raw \| diff to current
2020-05-20	Luke Kenneth Casso...	correct XER variable names	blob \| commitdiff \| raw \| diff to current
2020-05-18	Luke Kenneth Casso...	mass-rename of modules to soc.fu.*	blob \| commitdiff \| raw \| diff to current
2020-05-18	Luke Kenneth Casso...	rename pipe to fu	blob \| commitdiff \| raw \| diff to current

RSS Atom