sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-09-21	Remove cheri and mips specs -- they now have their own repository.	Robert Norton

2018-07-11	Update CHERI code extraction from Isabelle	Thomas Bauereiss
	Also use zero-initialised memory. Apparently some tests access unitialised memory, and the default behaviour of the Lem shallow embedding is to fail in this case.
2018-07-09	Simplify treating of undefined_bool in Lem library	Thomas Bauereiss
	Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list.
2018-06-25	Support bitlist representation in Sail2_string	Thomas Bauereiss

2018-06-22	Fix Lem build of MIPS/CHERI	Thomas Bauereiss

2018-05-09	Add tests for Isabelle->OCaml generation for CHERI and AArch64	Thomas Bauereiss

2018-04-18	Move a few printing functions to sail_values.lem	Thomas Bauereiss
	They are used in various specs and test cases.
2018-03-21	Fix Lem generation for MIPS	Thomas Bauereiss

2018-03-14	Fix Lem generation for CHERI-MIPS and Aarch64	Thomas Bauereiss
	- Update Lem bindings and extras files - Rewrite Nexp_var's if they are bound to a constant, similar to Nexp_id's (used for cap_size in the CHERI spec) - Add Lem and Isabelle Makefile targets for CHERI
2018-03-14	Add address to Write_tag outcome	Thomas Bauereiss
	The state monad currently assumes that tags are written to and read from properly aligned addresses (since it does not know the capability size used in the Sail model). This change allows the Sail model to pass in the aligned address(es) even if data is written to an unaligned address. There might be better ways to model tag writing, but this approach seems rather general.
2018-03-08	rename mips_new_tc to mips	Robert Norton

2018-03-08	Remove files in mips directory prior to copying in files from mips_new_tc. ↵	Robert Norton
	Hopefully thiis will help git to spot the rename and hence preserve history.
2017-11-30	match what rmem (ppcmem2) expects from ISA Makefiles	Shaked Flur

2017-07-26	mips_extras.lem: fix references to Interp.V_foo	Jon French

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-03-23	the interpreter/shallow expects little-endian memory-values	Shaked Flur

2016-11-30	add new barrier kind for MIPS (only one for now).	Robert Norton

2016-10-22	fixes following interface changes (type of instruction, name of barrier)	Robert Norton

2016-10-06	move type definitions that both interpreter and shallow embedding use to ↵	Christopher Pulte
	sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome
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-04-13	add tagr and tagw in mips_extras (will need to change these to make tag ↵	Robert Norton
	writes atomic)
2016-02-03	mips_extras.lem: fix typo in spelling of MEM_sync.	Robert Norton

2015-12-17	First bit of gluing mips onto interpreter and eventually ppcmem infrastructure	Kathy Gray