sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-07-09	Simplify treating of undefined_bool in Lem library	Thomas Bauereiss
	Use nondeterministic choice by default instead of a deterministic bitstream generator in the state, which is slightly awkward to reason about, because every use of undefined_boolS changes the state. The previous behaviour can be implemented as Sail code, if desired. Also add a default implementation of internal_pick that nondeterministically chooses an element from a list.
2018-06-12	Prove test_raw_add theorem for init_state	Ramana Kumar
	It can be proved almost entirely by symbolic execution (in <15s) _if_ the right definitions are in the compset. It took a lot of interactive stumbling about to discover that LUPDATE was missing from the standard list compset.
2018-06-12	Make progress on HOL4 test_raw_add	Ramana Kumar
	The proof now gets through simulation of the first instruction of the test.
2018-06-12	Work on HOL symbolic evaluation of installing code	Ramana Kumar

2018-06-12	Experimentation with PrePost for test_raw_add	Ramana Kumar

2018-06-12	Speculation on executing a CHERI test in HOL4	Ramana Kumar