| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-01 | Add support for read_tag and write_tag in sail_lib.ml. and support for ↵ | Robert Norton | |
| intialising and dumping CHERI state. Somewhat working cheri sail2 model. | |||
| 2018-02-27 | Get MIPS translated to Lem | Thomas Bauereiss | |
| 2018-02-23 | Fix some bugs in C compilation | Alasdair Armstrong | |
| Fixed an issue with pattern matching on enums Fixed an issue whereby fix_early_returns would cause memory leaks Added optimizations for some of the builtins used in the decode function. Optimizations are turned on with the -O flag. | |||
| 2018-02-23 | Some tidy up of sail library - use extract_num from Big_int to implement ↵ | Robert Norton | |
| to_get_slice_int in less confusing way. Add arithmetic shift right. | |||
| 2018-02-15 | Update duopod spec so it has no address translation | Alasdair Armstrong | |
| Also update the main aarch64 (no_vector) spec with latest asl_parser | |||
| 2018-02-13 | Support for large bitvector literals in C backend | Alasdair Armstrong | |
| 2018-02-06 | fix backwards arguments to pow2. | Robert Norton | |
| 2018-02-02 | Add M extension to RISCV. Slightly inelegant implementation for now but ↵ | Robert Norton | |
| passing tests. | |||
| 2018-01-29 | Add some initial exception handling to the riscv execution loop. | Prashanth Mundkur | |
| 2018-01-29 | implement shift primitives in sail_lib.ml | Robert Norton | |
| 2018-01-24 | Fixed riscv ocaml compilation | Alasdair Armstrong | |
| 2018-01-22 | Added rewriter that specializes all function calls in a specification. | Alasdair Armstrong | |
| This removes all type polymorphism, so we can generate optimized bitvector code and compile to languages without parametric polymorphism. | |||
| 2018-01-22 | Update and fix test suite | Alasdair Armstrong | |
| 2018-01-18 | Modified ocaml backend to use ocamlfind for linksem and lem | Alasdair Armstrong | |
| Fixed test cases for ocaml backend and interpreter | |||
| 2018-01-12 | OCaml interactive mode can now run full aarch64 examples, and ocaml test cases. | Alasdair Armstrong | |
| 2018-01-11 | Ocaml semantics can now run aarch64 hello world example using octapod | Alasdair Armstrong | |
| New testcase for bitfield syntax Updated to work with latest lem and linksem | |||
| 2018-01-05 | Added sail_lib file | Alasdair Armstrong | |
| 2017-07-21 | Everything moved to new typechecker | Alasdair Armstrong | |
| Modified initial_check.ml so it no longer requires type_internal. It's still needs cleaned up in a few ways. Most of the things it's trying to do could be done nicer if we took some time to re-factor it, and some of the things should just be handled by the main typechecker, leaving it as a think layer between the parse_ast and the ast. Now that's done everything can be switched to the new typechecker and the _new suffixes were deleted from everything except the monomorphisation pass because I don't know the status of that. | |||
| 2017-02-03 | fix headers | Peter Sewell | |
| 2015-12-14 | Adding new location constructor for location of generated terms | Kathy Gray | |
| 2014-07-29 | A file can now declare that a default order is either inc or dec, and this ↵ | Kathy Gray | |
| will be reflected in short hand type syntax, inc is still the default if undeclared So: default order dec register bit[32] t (* Declares t as a decreasing vector, starting at 31 on the left and decreasing to 0 *) default order inc register bit[32] o (* Declares o as an increasing vector, starting at 0 on the left and increasing to 31 *) It is presently possible to change the default mid-file; this is almost certainly bad and I will turn it into an error soon. | |||
| 2014-07-04 | Force end-of-input when parsing expression list | Gabriel Kerneis | |
| 2014-07-03 | Parse list of expressions in Sail_lib | Gabriel Kerneis | |
| 2014-07-03 | Introduce a Sail library | Gabriel Kerneis | |
| Used by the Power XML extraction tool. | |||
 |
index : sail | |
| Formal specification language for ISAs |
| summaryrefslogtreecommitdiff |