sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-11-01	added RISC-V "fence r,r"	Shaked Flur

2017-10-24	fix default cap value on cheri128 following previous changes -- E stored in ↵	Robert Norton
	registers is no longer xored with 48 so need to initialise it. Also use E and T values used by CHERI hw and adjust decoding functions appropriately. Fix shift functions for ocaml shallow embedding which failed to handle shifts greater than vector length.
2017-09-29	fix deep_shallow_convert, stop using interp_interface.instruction for most ↵	Christopher Pulte
	things, SF and CP bugfixing
2017-09-26	fixes	Christopher Pulte

2017-09-21	wib	Shaked Flur

2017-09-19	fix	Christopher Pulte

2017-09-15	reinstate deep/shallow conversion	Christopher Pulte

2017-09-03	added RISC-V strong-acquire/release	Shaked Flur

2017-08-22	and fix that other places	Christopher Pulte

2017-08-22	adapt state.lem to RISCV additions	Christopher Pulte

2017-08-12	Resolve ambiguity between negation of integers and bools	Thomas Bauereiss

2017-07-06	substitute all uses of mod_big_int and div_big_int for Z.rem and Z.div which ↵	Robert Norton
	have correct rounding behaviour. Missed these when changing quot and mod functions.
2017-07-06	implement abs function correctly for ocaml shallow embedding.	Robert Norton

2017-07-06	fix dodgy get_min/max_representable functions. Looks like an attempt at ↵	Robert Norton
	optimisation went wrong.
2017-06-30	add more tests for sail library. Can't compile entire file due to sail ↵	Robert Norton
	performance bug or infinite loop. Add some missing shallow embedding funcitons.
2017-06-22	fix three different copies of the hardware_quot function to do proper ↵	Robert Norton
	trucation towards zero. Previous version was incorrect if result was exact and a<0 and b>0.
2017-06-22	add a 'print' built-in function handy for writing sail tests.	Robert Norton

2017-06-14	Add a work-in-progress version of sail_values.lem	Brian Campbell
	that uses the new Lem machine words library.
2017-06-02	Add tag memory to Lem shallow embedding	Thomas Bauereiss

2017-05-24	fixed missing _tag bits	Shaked Flur

2017-05-24	Merge branch 'master' of bitbucket.org:Peter_Sewell/sail	Shaked Flur
	# Conflicts: # src/lem_interp/interp.lem # src/lem_interp/interp_inter_imp.lem # src/lem_interp/interp_interface.lem # src/parser.mly # src/pretty_print_lem.ml
2017-05-24	added the exmem effect for AArch64 store-exclusive	Shaked Flur

2017-05-24	it turns out that Zarith has a divide function which does truncation towards ↵	Robert Norton
	zero but it is not exposed via Bit_int_Z. Use it instead of rolling our own. Also ocaml / and mod already do the right thing.
2017-05-08	add some missing things in sail_values and make big_int version the default ↵	Robert Norton
	for set_vector_subrange_bit.
2017-04-27	add command line argument for setting undef values to all zero or all one. ↵	Robert Norton
	Some tests intentionally produce undefined values (e.g. divide by zero) and this might be required for them to work.
2017-04-25	optimise to_vec_int because it is used by MEMr to convert each byte to vector.	Robert Norton

2017-04-25	replace memory representation with map of 1MB pages rather than map of ↵	Robert Norton
	bytes. This makes loading binaries much quicker but doesn't seem to make a big difference to execution speed.
2017-04-25	remove unused function.	Robert Norton

2017-04-21	define some big_int literals in sail_values.ml to avoid lots of calls to ↵	Robert Norton
	bit_int_of_int. Likely very little performance benefit but slightly more readable.
2017-04-21	implement to_vec_big using zarith extract for some speedup.	Robert Norton

2017-04-21	suppress register field tracing if not enabled (missed in previous commit)	Robert Norton

2017-04-20	more library optimisation. Implement int_of_bit_array using shift, avoiding ↵	Robert Norton
	need to use power.
2017-04-20	implement vector subrange using Array.sub for approx 10% speedup.	Robert Norton

2017-04-20	attempt to optimise performance if not tracing writes.	Robert Norton

2017-04-20	add missing min and max functions, overriding built-in ocaml ones. Also ↵	Robert Norton
	neq_range.
2017-04-20	add name to register representation and print it on write.	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-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	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-03-30	Make length function return big_int	Robert Norton

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.