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

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

2020-07-24	Samuel A. Falvo II	WIP: SC properties more closely match doc'd behavior	blob \| commitdiff \| raw
2020-07-24	Samuel A. Falvo II	WIP: addressing code review, restoring proofs, etc.	blob \| commitdiff \| raw \| diff to current
2020-07-24	Luke Kenneth Casso...	code review comments for trap and proof	blob \| commitdiff \| raw \| diff to current
2020-07-24	Samuel A. Falvo II	Refactorin of common code	blob \| commitdiff \| raw \| diff to current
2020-07-24	Samuel A. Falvo II	Address code review comments	blob \| commitdiff \| raw \| diff to current
2020-07-22	Luke Kenneth Casso...	whoops forgot field accessor	blob \| commitdiff \| raw \| diff to current
2020-07-22	Luke Kenneth Casso...	whoops typo, 63-start not 3-start (doh)	blob \| commitdiff \| raw \| diff to current
2020-07-22	Luke Kenneth Casso...	field number ordering wrong way round?	blob \| commitdiff \| raw \| diff to current
2020-07-22	Luke Kenneth Casso...	syntax error	blob \| commitdiff \| raw \| diff to current
2020-07-22	Luke Kenneth Casso...	add comment headings with spec page numbers	blob \| commitdiff \| raw \| diff to current
2020-07-22	Luke Kenneth Casso...	comment on op.insn ordering	blob \| commitdiff \| raw \| diff to current
2020-07-22	Luke Kenneth Casso...	code-shuffle, add comments	blob \| commitdiff \| raw \| diff to current
2020-07-22	Luke Kenneth Casso...	inline comments in trap proof	blob \| commitdiff \| raw \| diff to current
2020-07-22	Samuel A. Falvo II	Complete FV properties for OP_TRAP instructions.	blob \| commitdiff \| raw \| diff to current
2020-07-22	Samuel A. Falvo II	PEP8 compliance	blob \| commitdiff \| raw \| diff to current
2020-07-21	Samuel A. Falvo II	Completed SC FV properties	blob \| commitdiff \| raw \| diff to current
2020-07-21	Samuel A. Falvo II	Refine properties to comply with spec	blob \| commitdiff \| raw \| diff to current
2020-07-21	Samuel A. Falvo II	Fix where msr_i gets its value from	blob \| commitdiff \| raw \| diff to current
2020-07-21	Samuel A. Falvo II	Merge in recent updates to TRAP FV properties.	blob \| commitdiff \| raw \| diff to current
2020-07-21	Luke Kenneth Casso...	corrections to trap proof see	blob \| commitdiff \| raw \| diff to current
2020-07-21	Luke Kenneth Casso...	use alias for msr_i in trap proof	blob \| commitdiff \| raw \| diff to current
2020-07-20	Samuel A. Falvo II	Rework SC properties to conform to style	blob \| commitdiff \| raw \| diff to current
2020-07-20	Samuel A. Falvo II	Formal properties for RFID.	blob \| commitdiff \| raw \| diff to current
2020-07-18	Luke Kenneth Casso...	add comment and copy of pseudo-code for OP_RFID into...	blob \| commitdiff \| raw \| diff to current
2020-07-18	Samuel A. Falvo II	WIP: FV failing for unknown reasons.	blob \| commitdiff \| raw \| diff to current
2020-07-18	Jacob Lifshay	Merge branch 'master' of ssh://git.libre-riscv.org...	blob \| commitdiff \| raw \| diff to current
2020-07-18	Samuel A. Falvo II	Failing test: fast1/fast2 vs srr0/srr1? on trap pipe	blob \| commitdiff \| raw \| diff to current
2020-07-18	Samuel A. Falvo II	forgot to clean up workspace in source	blob \| commitdiff \| raw \| diff to current
2020-07-18	Samuel A. Falvo II	FV props for SC instruction	blob \| commitdiff \| raw \| diff to current
2020-07-17	Samuel A. Falvo II	First FV property for trap unit	blob \| commitdiff \| raw \| diff to current

RSS Atom