sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
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-06-21	Pretty-print bitvector expressions	Thomas Bauereiss
	- Add case distinctions between bitvector types and vectors of other element types (e.g. registers) and use the corresponding operations (i.e. "bvslice", "bvaccess", etc for the former, and "slice", "access", etc for the latter) when pretty-printing expressions - Add type annotations to expressions when the type includes bitvectors with concretely known length - Update state.lem to use bitvectors (in the interface, at least; internally, bitvectors are still stored as bit lists for now, since that makes it easier to support storing different registers with different lengths) This has been tested with the CHERI-MIPS model with some success, but some things are still missing: - Bitvector patterns are not handled yet - Some bitvector length monomorphisation is needed in a few places of the model - Some type annotations are missing, because the (old) Sail type checker does not infer bitvector lengths in some instances where one would hope it to do that; this should be checked with the new type checker
2017-06-02	Add tag memory to Lem shallow embedding	Thomas Bauereiss

2017-05-24	fixed missing _tag bits	Shaked Flur

2017-05-10	Add stubs for TAGw	Thomas Bauereiss
	Tagged memory seems to be currently missing in the Lem shallow embedding of (CHERI-)MIPS.
2017-03-23	the interpreter/shallow expects little-endian memory-values	Shaked Flur

2016-12-09	sail changes for making lem embedding Isabelle-friendlier	Christopher Pulte

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

2016-11-28	make sail produce prompt and state version of shallow embedding files at the ↵	Christopher Pulte
	same time with the types both have in common factored out into separate file, rename one mips shallow embedding _extras file as required by this