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-06-27	Add a new function cycle_limit_reached that returns bool, allowing for ↵	Robert Norton
	graceful exit on reaching cycle limit. This aids coverage and valgrind instrumentation.
2018-06-26	mips: fix duplication of cycle_count call that arose due to git merge.	Robert Norton

2018-06-26	mips: comment out printing of EXCEPTION on every ISA exception.	Robert Norton

2018-06-25	Use getopt rather than argp for Mac compatibility in C runtime	Alasdair Armstrong
	Also further tweaks to Sail library for C and include sail lib files for tracing
2018-06-22	add support for new cycle_limit feature in mips.	Robert Norton

2018-06-21	Remove loading kernel from mips main	Alasdair Armstrong

2018-06-11	More efficient bitfield implementation	Alasdair Armstrong

2018-06-07	Refactor mips main a little to work around apparent bug in c generation. ↵	Robert Norton
	Generated c Works with no gcc optimisation but fails when optimisation is on, implying undefined behaviour. Probably due to control reaching end of non-void function in exception case.
2018-06-04	cheri: print debug trace info to stderr to keep it separate from uart output.	Robert Norton

2018-05-17	build fixes: add back tag effect skips required for mips. Move UART check in ↵	Robert Norton
	to correct place in main.sail. Remove add_atom and sub_atom from prelude as we get them from arith.sail.
2018-05-17	changes to for testing FreeBSD boot on MIPS: allowing loading raw file in ↵	Robert Norton
	ocaml main so that we can have simboot + kernel. Support UART output only.
2018-05-17	Refactor main.sail	Thomas Bauereiss

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

2018-03-27	print IPS after running cheri model.	Robert Norton

2018-03-22	Fix C compilation for CHERI and MIPS	Alasdair Armstrong
	First, the specialisation of option types has been fixed by allowing the specialisation of constructor return types - this essentially means that a constructor, such as Some : 'a -> option('a) can get specialised to int -> option(int), rather than int -> option('a). This means that these constructors are treated like GADTs internally. Since this only happens just before the C translation, I haven't put much effort into making this very robust so far. Second, there was a bug in C compilation for the typing of return expressions in non-unit contexts, which has been fixed. Finally support for vector literals that are non-bitvectors has been added.
2018-03-08	rename mips_new_tc to mips	Robert Norton