sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-12-30	use linksem as a package	Shaked Flur

2017-12-05	Update header files on master	Alasdair Armstrong

2017-09-29	fix those build errors	Christopher Pulte

2017-08-02	fix run_with_elf*.ml with changed lem_interp api	Jon French

2017-05-26	fix run_with builds after build_context gained an extra argument.	Robert Norton

2017-05-24	Change types of MEMr_tag, MEMval_tag and co. so that tag is separate from ↵	Robert Norton
	data and invent rmemt and wmvt effects for them. Extend the interpreter context to include lists of tagged memory read and write functions. The memory model must round down the address to the nearest capability aligned address when reading/writing tags. Remove TAGw which is no longer needed as a result.
2017-04-03	Rename TranslateAddress to TranslatePC and remove the accessType argument -- ↵	Robert Norton
	it is only ever used for translating the PC.
2017-03-29	change reqiured to work with little endian interpreter.	Robert Norton

2017-02-03	fix headers	Peter Sewell

2016-12-02	fix interpreter build following refactoring	Robert Norton

2016-10-25	load all segments into prog_mem regardless of x flag (for running cheri ↵	Robert Norton
	tests all memory is equal
2016-10-22	fixes following interface changes (type of instruction, name of barrier)	Robert Norton

2016-10-11	Update run_with_elf* for new linksem sail_interface	Robert Norton

2016-10-11	Update to use sail_impl_base.	Robert Norton

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-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	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-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-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	Make run_with_elf compile again	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-13	Copy run_with_elf to make run_with_elf_cheri and revert run_with_elf to mips ↵	Robert Norton
	version. Temporary 'solution' to building mips and cheri builds until proper factorising can take place.
2016-04-13	cheri supporting run with elf	Kathy Gray

2016-03-08	Start task of setting up tagged memory in sequential interpreter	Kathy Gray

2016-02-03	mips: finish implementing address translation on instruction fetch and ↵	Robert Norton
	remove temporary hack in TranslateAddr.
2016-02-03	mips: add support for LLAddr, a debug register used for ll/sc. Also add ↵	Robert Norton
	missing psuedo-registers in run_with_elf.
2016-02-02	mips.sail: add an 'inBranchDelay' register so that SignalException can set ↵	Robert Norton
	correct state on exception. branchPending does not work because it is cleared before executing the branch delay.
2016-02-02	Print out the address of the instruction running in sequential interpreter	Kathy Gray

2016-02-02	Get mips stuff hooked up with translate address.	Kathy Gray
	Note: this support is rather mips centric at the moment
2016-02-02	add translate_address functionality	Kathy Gray

2016-01-28	Support exit and assert better in sequential interpreter and general ↵	Kathy Gray
	interpreter interface
2016-01-27	Add --max_instruction to sequential interpreter to permit an upper bound on ↵	Kathy Gray
	instructions run
2016-01-27	Add ability to run to a particular instruction execution number	Kathy Gray
	Could later add the ability to run to a particular instruction form (like we had in ppcmem2) or address
2016-01-27	Make mips build again	Kathy Gray
	Make quiet mode for sequential interpreter not print
2016-01-27	start adding breakpoint	Kathy Gray

2016-01-26	fix starting indices for mips initial register values.	Robert Norton

2016-01-26	Fix some bugs in writing registers with slices in the sequential interpreter	Kathy Gray

2016-01-26	print reg dump in correct format for cheri test suite. Reinstate timing of ↵	Robert Norton
	execution.
2016-01-26	dump registers in format expected by cheri test suite when halting. Remove ↵	Robert Norton
	distinction between prog_mem and data_mem at least for now as data_mem was not being populated correctly (wrong elf flags?).
2016-01-22	mips: fix PC update logic so branches might work.	Robert Norton

2016-01-21	mips interpreter successfully executes more than one instruction after some ↵	Robert Norton
	wrangling of integer types
2016-01-21	mips: rename GPRs so that they sort lexicographically for display.	Robert Norton