sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2017-03-23	the interpreter/shallow expects little-endian memory-values	Shaked Flur

2017-03-02	tweak comments	Peter Sewell

2017-02-03	fix headers	Peter Sewell

2017-01-14	changes to enable interpreter exhaustive analysis in ppcmem again	Christopher Pulte

2016-12-01	move interpreter-specific types from Sail_impl_base to Interp_interface	Christopher Pulte

2016-11-27	make outcome_s contain the instruction state pretty print rather than the ↵	Christopher Pulte
	instruction state, factor out interpreter/shallow embedding value conversion
2016-11-09	move decode_error type back to Sail_impl_base for now	Christopher Pulte

2016-11-08	fixes	Christopher Pulte

2016-11-05	fixes	Christopher Pulte

2016-10-21	shallow embedding progress	Christopher Pulte

2016-10-06	move type definitions that both interpreter and shallow embedding use to ↵	Christopher Pulte
	sail_impl_base, add sail_impl_base.outcome, add interp_inter_imp auxiliary functions, make prompt use sail_impl_base.outcome
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