sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-04-18	make ocaml embedding of foreach use (now universal) big_ints.	Robert Norton

2017-04-18	fix definition of mask -- Vregister and VvectorR were swapped.	Robert Norton

2017-04-18	Implement return using an exception caught in the function body. Polymorphic ↵	Robert Norton
	exceptions are not permitted so a local mutable variable, ret, is used in ocaml to store the return value. This avoids having to define a new exception type for each function. Ocaml infers the type of the option when it is assigned at the return site.
2017-04-18	Generate runtime error for L_undef. Existing code was broken except for type ↵	Robert Norton
	bit (specifically it caused generated ocaml to fail to type check for an undef number.
2017-04-18	added transactional memory support	Shaked Flur

2017-04-07	fix error in generated ocaml where writing single bit of register was not ↵	Robert Norton
	taking account of register direction.
2017-04-07	implement quot and mod with truncation towards zero which is not the ocaml ↵	Robert Norton
	way but standard for C and most hw.
2017-04-07	simplify xor using ocaml <> operator which also has the advantage of being ↵	Robert Norton
	more correct
2017-04-06	use set_register when writing element of vector of registers to avoid ↵	Robert Norton
	accidentally replacing Vregister with Vvalue or Vregister... Seems to work for MIPS but not sure if might encounter vector of something other than bit or register. A more specific value type would have made this a compile-time error rather than run-time.
2017-04-06	add support for address translation and exit handling in mips ocaml shallow ↵	Robert Norton
	embedding test setup.
2017-04-06	minor changes in sail_values.ml to aid debugging	Robert Norton

2017-04-06	fix incorrect use of == in eq	Robert Norton

2017-04-06	implement exts and extz as manipulations on bit vectors rather than ↵	Robert Norton
	converting to integers, allowing them to work on vectors containing undef.
2017-04-06	Implement exit by raising Sail_exit exception	Robert Norton

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-30	Make length function return big_int	Robert Norton

2017-03-29	change reqiured to work with little endian interpreter.	Robert Norton

2017-03-29	Factor out pretty printers into separate files. Hopefully this will make ↵	Robert Norton
	searching easier.
2017-03-28	temporary fix for problem duplicate (lack of direction) -- assume decreasing ↵	Robert Norton
	for mips compatibility.
2017-03-28	Fix erroneous bitwise xor.	Robert Norton

2017-03-27	fix bitshift operators. I think these should be independent of vector order...	Robert Norton

2017-03-27	Fix broken to_vec of negative values. Old code was a bit confused. Probably ↵	Robert Norton
	possible to rewrite using arithmetic on big_int which might be faster.
2017-03-25	endianness fix	Shaked Flur

2017-03-24	fixed endianness	Shaked Flur

2017-03-24	Checkpoint work-in-progress mips sequential interpreter using ocaml shallow ↵	Robert Norton
	embedding.
2017-03-24	changes to ocaml pp to allow mips->ocaml to compile	Robert Norton

2017-03-24	Christopher, Peter: make "run_interp_model.ml" build again (endianness)	Peter Sewell

2017-03-24	Print tracking information for V_track, hopefully fix extern_vector_value, ↵	Christopher Pulte
	fix sail_values bug.
2017-03-23	the interpreter/shallow expects little-endian memory-values	Shaked Flur

2017-03-02	tweak comments	Peter Sewell

2017-02-14	remove the -i option	Peter Sewell

2017-02-14	tidy command-line options	Peter Sewell

2017-02-09	wib	Peter Sewell

2017-02-09	group initial type environment into meaningful sections; pretty-print in ↵	Peter Sewell
	user-readable way
2017-02-09	tweak pp of initial type environment and l2.ott comments	Peter Sewell

2017-02-08	put back the header into Sail_impl_base	Christopher Pulte

2017-02-08	pull in Shaked's type class instance changes, fix Ord and Eq instances	Christopher Pulte

2017-02-05	command-line option to dump initial type environment	Peter Sewell

2017-02-03	replace bit vector return types in getCapX functions with equivalent integer ↵	Robert Norton
	range types. This removes quite a few uses of unsigned() in cheri intsruction pseudocode. Could potentially take things furter.
2017-02-03	fix headers	Peter Sewell

2017-02-03	licensing	Peter Sewell

2017-02-01	document coercions	Peter Sewell

2017-02-01	fix up uint type bounds	Kathy Gray

2017-01-31	Kathy, Peter: pp of initial type environment	Peter Sewell

2017-01-27	fix right shift	Kathy Gray

2017-01-27	failing test with c128	Robert Norton

2017-01-26	c128: xor E with 48 when storing in memory so that null cap is all zeros but ↵	Robert Norton
	has non-zero E (latest spec.)
2017-01-26	christopher, kathy, peter: hacky experiment on nias_of_instruction	Peter Sewell

2017-01-25	Merge branch 'master' of https://bitbucket.org/Peter_Sewell/sail	Kathy Gray

2017-01-25	Make interpreter a little more flexible on the format of a register type to ↵	Kathy Gray
	match ASL; add missing functions/cases to library