sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2014-11-26	Fix neg	Kathy Gray

2014-11-25	more changes to quot and mod	Kathy Gray

2014-11-25	another carry out attempt	Kathy Gray

2014-11-25	improved division	Kathy Gray

2014-11-25	wib	Kathy Gray

2014-11-25	carry out is computed	Kathy Gray

2014-11-25	another mod and quot definition	Kathy Gray

2014-11-25	refine quot and mod	Kathy Gray

2014-11-24	Add new quot and mod operators	Kathy Gray

2014-11-24	don't to_num a num...	Kathy Gray

2014-11-24	Give a better answer on overflow with two vectors of unknowns (i.e. unknown ↵	Kathy Gray
	instead of 0)
2014-11-24	Correctly cast between 1 and a single bit	Kathy Gray

2014-11-24	Missing patterns in pattern matches	Kathy Gray

2014-11-24	Updated library	Kathy Gray

2014-11-24	wib	Kathy Gray

2014-11-24	Signed and unsigned comparisons	Kathy Gray

2014-11-23	coerce better between a single bit and a bit vector of one bit	Kathy Gray

2014-11-23	maybe best not to die at the first sign of an undef...	Kathy Gray

2014-11-23	properly name division operators in lib	Kathy Gray

2014-11-23	make interpreter now builds	Kathy Gray
	and I think that I'm making vectors of unknowns in all the necessary places now.
2014-11-22	signed multiplication and quot	Kathy Gray

2014-11-22	add new function for overflow arithmetic instructions	Kathy Gray

2014-11-21	Support signed and unsigned arithmetic	Kathy Gray

2014-11-21	Print out default values for underspecified vectors instead of leaving them ↵	Kathy Gray
	and letting them turn into undefineds
2014-11-20	look for sub matches of registers on exhaustive mode	Kathy Gray

2014-11-18	Fix various pattern match bugs; add a few functions	Kathy Gray

2014-11-16	Add some missing functions	Kathy Gray

2014-11-16	Add overflow checking arithmetic operations. Fix various bugs that this exposed	Kathy Gray
	Of note: Interp_lib.to_num now takes an Unsigned or a Signed constructor, rather than a boolean
2014-11-05	Correct bug treating unsigned values as signed in arith operations	Kathy Gray

2014-10-30	Add case to neg for interp_lib	Kathy Gray

2014-10-28	Allow tracking of unknowns in interp library, removing the P hacks.	Kathy Gray
	Add a function from instruction to istate
2014-10-28	hacks on taint tracking	Peter Sewell

2014-10-22	Update printing for testing, fix some bugs found along the way	Kathy Gray

2014-10-16	bug fixes to run test from Christopher's tests	Kathy Gray

2014-10-14	Iron out bugs in running new executable with branching; add new executable ↵	Kathy Gray
	as well.
2014-09-04	Make exhaust run from the first breakpoint in the interactive interpreter	Kathy Gray
	(I still think this is a silly place to run exhaust from, but it no longer finds errors or crashes)
2014-08-27	Changes to get another (slightly larger) executable running;	Kathy Gray
	adding executable as a test as well
2014-08-20	Add ability to track register dependencies in interactive stepper; thus ↵	Kathy Gray
	testing register tracking/tainting
2014-08-13	Update library functions	Kathy Gray

2014-07-30	working dec vectors	Kathy Gray

2014-07-01	Update case of EXTS	Gabriel Kerneis

2014-06-25	Add support for actions that read just a slice or single bit of a register	Kathy Gray

2014-06-24	Get enumerations working in interpreter	Kathy Gray
	(plus a few other small related corrections)
2014-06-24	Get vector length for to_inc_vec and to_dec_vec from the type system after ↵	Kathy Gray
	constraint solving (instead of hardcoding 64 as the default).
2014-06-19	Add mod:vec->range->vec	Gabriel Kerneis

2014-06-18	Fix mod_vec in library	Gabriel Kerneis

2014-06-18	Add definition of mod to lib	Kathy Gray

2014-06-12	Interpret when an unknown is inserted into the program by interp_exhaustive	Kathy Gray
	Short version of below; ready to hook interp_exhaustive up to something to test, but haven't yet. If an unknown value influences a pattern match within an expression, each passing pattern is found and the bodies strung together into a block with let expressions to bind the variables. In a function call, the cases are all collected but the support is not in place at the moment to evaluate them. If an unknown is the result of the cond expression in an if, the then and else case become a block. Unknowns within the interpreter propagate to more Unknowns; also for some but not all library functions yet.
2014-06-11	Equality between range and bit vector	Gabriel Kerneis
	The type-constraints are inspired from those for (+). They seem to work but I am not sure they make sense. The vector is interpreted as unsigned.
2014-06-11	Improve error message for missing library functions	Gabriel Kerneis