sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2016-09-30	add Robert's DIA typeclass instances	Christopher Pulte

2016-09-30	fixes, update isntruction_analysis for NIAs and DIA	Christopher Pulte

2016-09-19	remove conflict message	Christopher Pulte

2016-09-16	make vector concatenation pattern removal deal with vector patterns of ↵	Christopher Pulte
	unknown length (in the last item)
2016-09-14	Add memory kind for concurrent tag reads and writes	Kathy Gray

2016-09-13	Add optional address to memv events	Kathy Gray

2016-09-13	add show functions, fix	Christopher Pulte

2016-09-09	minor fixes	Kathy Gray

2016-09-09	update instruction_analysis to support nias and instruction kind	Christopher Pulte

2016-09-02	Extend type checking so that patterns with vector concatenation don't permit ↵	Kathy Gray
	under specified vector lengths (at least for function patterns) Extend interpreter interface to have a function for Christopher's instruction analysis
2016-08-18	move register_base_name and slice_of_reg_name from ppcmem thread semantics ↵	Christopher
	to interp_interface, fix reg_name comparison and equality
2016-08-06	Add duplicate_bits to lib	Kathy Gray
	Pull Peter's changes to interp_interface back into the primary repo
2016-05-03	Change decode and translate_address to support writing register events ↵	Kathy Gray
	(although decode isn't pushed through yet). Note: this will break all builds
2016-04-25	Make interpreter able to read registers during translate address and decode.	Kathy Gray
	This is not yet connected to any model and not yet tested. Also, reduce the number of parentheses needed by the parser. Namely, register declarations should no longer need parens around the types and let expressions should need fewer instances of parens around the expression (i.e. let a = exp ).
2016-04-18	More fixes to interp with regards to warnings and debugging info	Kathy Gray

2016-03-08	Return undefined value on reads of uninitialised memory	Kathy Gray

2016-03-08	Start task of setting up tagged memory in sequential interpreter	Kathy Gray

2016-02-02	add translate_address functionality	Kathy Gray

2016-01-29	fix typo in kathy's last commit.	Robert Norton

2016-01-29	Put correct tags on to_vec calls	Kathy Gray

2016-01-28	Support exit and assert better in sequential interpreter and general ↵	Kathy Gray
	interpreter interface
2016-01-26	Fix some bugs in writing registers with slices in the sequential interpreter	Kathy Gray

2015-11-10	Make first half of sequential interpreter driver compile again	Kathy Gray

2015-07-24	Merge branch 'master' of bitbucket.org:Peter_Sewell/l2	Shaked Flur

2015-07-24	added signed_integer	Shaked Flur

2015-07-24	Begin doing better analysis on case splits over unknowns	Kathy Gray

2015-07-19	abbreviate printing of memory values <=9	Peter Sewell

2015-07-01	Go on despite the presence of an exit in exhaustive mode	Kathy Gray

2015-06-24	Add new outcomes/events separating effective address and value for memory writes	Kathy Gray

2015-06-19	one more end flag for memory_value functions	Kathy Gray

2015-06-18	Add more end_flag parameters	Kathy Gray

2015-06-17	Extend mode and external memory functions with endian flag	Kathy Gray

2015-06-16	Incorporate comments from Peter.	Kathy Gray
	Add a flag type for endian, not used yet
2015-06-09	Fix error in building register values	Kathy Gray
	(make one function to do it instead of almost the same function multiple times) Fix lost nexp variable in constraints, removing another undefined
2015-06-02	changes to compare and equality instances to make lem generate isabelle output	cp526

2015-06-02	Fix errors around ARM not being able to decode due to instruction_extractor ↵	Kathy Gray
	being very power-specific. Note: slight interface change to instruction_extractor
2015-05-18	Add equality check for addresses	Kathy Gray
	And fix match failure problem (hopefully)
2015-05-18	Add comparison for address	Kathy Gray

2015-05-16	Fix bug where undef was blown up to fill the full register on a field assignment	Kathy Gray

2015-05-13	Add dynamic footprint dependency check event/outcome	Kathy Gray
	Also fix type checker bug in not reporting modifications to parameter values
2015-05-01	Change interpreter interface to support ppcmem2's view of vectors as always ↵	Kathy Gray
	increasing while supporting inc and dec views to the interpreter and in printing Fix bugs exposed by running idlarm several instructions (after fixing above)
2015-03-19	added constructors for aarch64 read_kind and write_kind	Shaked Flur

2015-03-15	Many changes:	Kathy Gray
	Split out specification specific memory and external functions Reduce the presence of big_int Reduce the use of inc direction, instead using a default from the spec. Still a few places need to be parameterised over direction Also some bug fixes exposed by above and running ARM second instruction
2015-02-27	Fix a series of errors leading to the first ARM instruction not running.	Kathy Gray
	Including: Correct loss of constraints between declared constraints, pattern constraints and expression body constraints Handle insertion of dependent parameters in the case of unit parameters Add a case to how ifields are translated to permit numbers as well as bits and bitvectors Expand interpreter to actually handle user-defined functions on the left had side of the assignment expression.
2015-01-16	more for loop corrections, as well as pattern match error	Kathy Gray

2014-11-23	fix register-from-address start int	Peter Sewell

2014-11-23	some Ord instance classes	Kathy Gray

2014-11-23	wib	Peter Sewell

2014-11-23	wib	Peter Sewell
	Merge branch 'master' of bitbucket.org:Peter_Sewell/l2 Conflicts: src/lem_interp/interp_interface.lem
2014-11-23	wib	Peter Sewell