sail - Formal specification language for ISAs

Age	Commit message (Collapse)	Author
2018-02-15	Rebase state monad onto prompt monad	Thomas Bauereiss
	Generate only one Lem model based on the prompt monad (instead of two models with different monads), and add a lifting from prompt to state monad. Add some Isabelle lemmas about the monad lifting. Also drop the "_embed" and "_sequential" suffixes from names of generated files.
2018-02-15	Re-engineer prompt monad of Lem shallow embedding	Thomas Bauereiss
	- Use simplified monad type (e.g., without the with_aux constructors that are not needed by the shallow embedding). - Add support for registers with arbitrary types (e.g., records, enumerations, vectors of vectors). Instead of using bit lists as the common representation of register values at the monad interface, use a register_value type that is generated per spec as a union of all register types that occur in the spec. Conversion functions between register_value and concrete types are generated. - Use the same representation of register references as the state monad, in preparation of rebasing the state monad onto the prompt monad. - Split out those types from sail_impl_base.lem that are used by the shallow embedding into a new module sail_instr_kinds.lem, and import that. Removing the dependency on Sail_impl_base from the shallow embedding avoids name clashes between the different monad types. Not yet done: - Support for reading/writing register slices. Currently, a rewriting pass pushes register slices in l-expressions to the right-hand side, turning a write to a register slice into a read-modify-write. For interfacing with the concurreny model, we will want to be more precise than that (in particular since some specs represent register files as big single registers containing a vector of bitvectors). - Lemmas about the conversion functions to/from register_value should be generated automatically.
2018-02-07	Add some printing functions to Lem shallow embedding	Thomas Bauereiss

2018-01-31	Add wrappers around Lem operators using bitvector type class	Thomas Bauereiss
	Makes bitvector typeclass instance dictionaries disappear from generated Isabelle output.
2018-01-31	Split base definitions of Lem monads and further built-ins (e.g. loop ↵	Thomas Bauereiss
	combinators) Add Isabelle-specific theories imported directly after monad definitions, but before other combinators. These theories contain lemmas that tell the function package how to deal with monadic binds in function definitions.
2018-01-29	Fix Lem generation for RISC-V	Thomas Bauereiss

2018-01-22	Update Lem shallow embedding to Sail2	Thomas Bauereiss
	- Remove vector start indices - Library refactoring: Definitions in sail_operators.lem now use Bitvector type class and work for both bit list and machine word representations - Add Lem bindings to AArch64 and RISC-V preludes TODO: Merge specialised machine word operations from sail_operators_mwords into sail_operators.