sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-09-19	remove conflict message	Christopher Pulte

2016-09-16	make vector concatenation pattern removal deal with vector patterns of ↵	Christopher Pulte
	unknown length (in the last item)
2016-09-14	Switch mips/cheri over to using memory ea/val for writes. Tag is now first ↵	Robert Norton
	byte of value for capability writes. Still need TAGw for now but should kill eventually.
2016-09-14	Add memory kind for concurrent tag reads and writes	Kathy Gray

2016-09-14	Change reading and writing of tag memory to report the tag/look for the tag ↵	Kathy Gray
	as the first byte of the byte list on tagged memory operations
2016-09-13	Support memea and memv in sequential interpreter	Kathy Gray

2016-09-13	Add optional address to memv events	Kathy Gray

2016-09-13	add show functions, fix	Christopher Pulte

2016-09-13	extern slice for instruction analysis	Kathy Gray

2016-09-12	add list append function	Kathy Gray

2016-09-09	minor fixes	Kathy Gray

2016-09-09	update instruction_analysis to support nias and instruction kind	Christopher Pulte

2016-09-02	Extend type checking so that patterns with vector concatenation don't permit ↵	Kathy Gray
	under specified vector lengths (at least for function patterns) Extend interpreter interface to have a function for Christopher's instruction analysis
2016-08-18	move register_base_name and slice_of_reg_name from ppcmem thread semantics ↵	Christopher
	to interp_interface, fix reg_name comparison and equality
2016-08-17	tuple assignment now implemented so (a,b) := foo() will now work	Kathy Gray

2016-08-17	Fix pattern match bug in interp where vector accesses were using the wrong ↵	Kathy Gray
	start index
2016-08-14	Add missing case to replicate	Kathy Gray

2016-08-10	Missing case in lib	Kathy Gray

2016-08-06	Add duplicate_bits to lib	Kathy Gray
	Pull Peter's changes to interp_interface back into the primary repo
2016-07-28	Banish exit from the mips/cheri sail except at end of SignalException ↵	Robert Norton
	function. There is a plan to replace this syntax with something more understandable. Should make no functional difference using sequential interpretor but will need to do some work on exception functions when integrating with ppcmem so that it know register writes are exceptional etc.
2016-07-26	Fix incomplete match warning in run_with*	Robert Norton

2016-07-26	Increase size of TLB to 64 entries. In theory this should improve FreeBSD ↵	Robert Norton
	boot time by reducing TLB misses but an apparent reduction in IPS counteracts this. Makes use of foreach and return to implement tlbSearch.
2016-07-26	And fix abbrev oversite in interpreter	Kathy Gray

2016-07-26	Add minimal support for emulated Altera JTAG UART.	Robert Norton

2016-07-26	Add support for loading a raw binary file at given location in memory prior ↵	Robert Norton
	to sequential simulation. This is needed for booting FreeBSD where a minimal bootloader (simboot.elf) runs before jumping into the kernel loaded in memory.
2016-07-25	win	Kathy Gray

2016-07-25	one more go	Kathy Gray

2016-07-25	Actually fix stack for return	Kathy Gray

2016-07-25	Fix stack for return	Kathy Gray

2016-07-25	Support return in interpreter pretty printer (also fix typo for default case)	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-01	Add missing case to arith_op_no0	Kathy Gray
	Add type refinement to arm spec
2016-06-07	Fix issue in accessing fields and slices of registers during translate address	Kathy Gray

2016-06-03	Fix bug exposed/introduced by properly handling vector starts in the type ↵	Kathy Gray
	checker
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-02	Fix most_significant case omission	Kathy Gray

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	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