sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-07-25	auto coerce to bit vector from bit	Kathy Gray
	pretty print lret effects into lem
2016-07-24	Make sure that all type constructors with unit type have a type union with ↵	Kathy Gray
	just an id (hopefully fixes Christopher issue).
2016-07-23	Add effect annotation for return, and actually keep a return after type check.	Kathy Gray

2016-07-23	Add a return exp form to Sail, supported in type checker and in interpreter.	Kathy Gray
	TODO: add an event for a return so that rewriters can find and remove them as needed for OCaml and Lem
2016-07-20	Make rewriter understand type abbreviations for removing internal_exp instances	Kathy Gray

2016-07-13	fixes	Christopher

2016-07-12	sail-to-lem and lem library fixes	Christopher

2016-07-01	Add missing case to arith_op_no0	Kathy Gray
	Add type refinement to arm spec
2016-06-20	Fix error in type checker that put some constraints wrongly into conditional ↵	Kathy Gray
	constraints, breaking power. Also improve reporting of contract constraints, but then turn them off :( to allow power to compile.
2016-06-07	Fix issue in accessing fields and slices of registers during translate address	Kathy Gray

2016-06-07	add a test for failing TLB translation during instruction fetch.	Robert Norton

2016-06-06	remove mips test elf files no longer expected to work due to having ↵	Robert Norton
	incorrect LMA values (since sail interpreter now translates PC addresses).
2016-06-06	add test for failing tlb translation using current sail.	Robert Norton

2016-06-03	Fix bug exposed/introduced by properly handling vector starts in the type ↵	Kathy Gray
	checker
2016-06-03	Change path inside sail Makefile to look for sail directory instead of l2	Kathy Gray

2016-06-03	turn off debug print statements	Kathy Gray

2016-06-03	Mips file: removed some unnecessary parenthesis	Kathy Gray
	Interp: trying to add some debugging to isolate bug
2016-06-03	Add test demonstrating recently introduced regression where tlb match fail.	Robert Norton

2016-06-02	Fix most_significant case omission	Kathy Gray

2016-06-02	Get widening right now that it matters	Kathy Gray

2016-06-02	improve constraint range checking	Kathy Gray

2016-05-27	Fix parsing of sizeof and some printing issues with let	Kathy Gray

2016-05-27	small change to comment printing	Kathy Gray

2016-05-27	Add sizeof to sail. Documentation to follow	Kathy Gray

2016-05-26	add makery for mips/cheir LOC count.	Robert Norton

2016-05-25	add support for capability load/store bits in TLB	Robert Norton

2016-05-20	Add missing CP0BadVaddr in run_with_elfs.	Robert Norton

2016-05-18	Implement 8-entry software-managed TLB.	Robert Norton

2016-05-12	Implement count/compare registers for timer interrupts and rdhwr instruction.	Robert Norton

2016-05-10	Initialise CP0Status BEV bit.	Robert Norton

2016-05-09	fix mips build by copying across run_with_elf_cheri.ml and removing cheri parts.	Robert Norton

2016-05-09	Reverse the list of events to respect their order	Kathy Gray

2016-05-09	commit test which fails due to not writing C31.offset in TranslateAddress.	Robert Norton

2016-05-09	Add more debugging information for vector concatenation	Kathy Gray

2016-05-06	rewrite fde_loop to make it easier to understand and fix some tests. still ↵	Robert Norton
	requires some clean up (currently one huge function).
2016-05-05	Factor out get_opcode	Robert Norton

2016-05-04	Correct register field/slice reading for decreasing reads for ↵	Kathy Gray
	decode/translate_address/exhaustive. (Was previously correct for full register reads)
2016-05-03	List registers required to handle exception during instruction fetch. ↵	Robert Norton
	Attempt to get correct behaviour wrt nextpC on instruction fetch exception (prob. still wrong).
2016-05-03	actually read next_pc twice when handling a translate_address exception	Kathy Gray

2016-05-03	write all or part of fields out of translate_address (instead of just all)	Kathy Gray
	fix bug in interp_to_value_helper
2016-05-03	Change decode and translate_address to support writing register events ↵	Kathy Gray
	(although decode isn't pushed through yet). Note: this will break all builds
2016-04-27	slightly simplify set_next_instruction_address -- no need to read convert ↵	Robert Norton
	then reconvert delayedPC
2016-04-27	expand supported patterns for most_significant	Kathy Gray

2016-04-27	Make run_with_elf compile again	Kathy Gray

2016-04-27	cheri: add translation and bounds checking of PC via PCC. Slightly clunky ↵	Robert Norton
	implementation for now and exceptions not properly handled.
2016-04-26	Add more cases for translate_address to support enums	Kathy Gray

2016-04-26	print error case on translate address	Kathy Gray

2016-04-25	make pretty printer keep up with parser changes	Kathy Gray

2016-04-25	Make interpreter able to read registers during translate address and decode.	Kathy Gray
	This is not yet connected to any model and not yet tested. Also, reduce the number of parentheses needed by the parser. Namely, register declarations should no longer need parens around the types and let expressions should need fewer instances of parens around the expression (i.e. let a = exp ).
2016-04-21	Introduce wrapper function around MEMw* so that we can clear tags on ↵	Robert Norton
	non-capability writes on cheri.