summaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2018-02-01Clean up riscv_duopod sail and add make targets for ocaml and Isabelle.Robert Norton
2018-02-01Add c.addi4spn.Prashanth Mundkur
2018-02-01Fix encoding for compressed ILLEGAL.Prashanth Mundkur
2018-02-01Initial top-level support for compression instructions.Prashanth Mundkur
2018-01-31Try to make bitvector pattern rewriting more robustThomas Bauereiss
2018-01-31Fix bug in bitvector pattern rewritingThomas Bauereiss
2018-01-31More updates to C backend - matching and tuplesAlasdair Armstrong
2018-01-31Added test case for decode patterns that are currently failingAlasdair Armstrong
2018-01-31Find buried set constraints in assertsBrian Campbell
2018-01-31Fix mono continue away optionBrian Campbell
2018-01-31Export arithmetic shift right from Lem libraryThomas Bauereiss
2018-01-31Add Lem operator wrappers for bitlistsThomas Bauereiss
2018-01-31Add wrappers around Lem operators using bitvector type classThomas Bauereiss
2018-01-31Split base definitions of Lem monads and further built-ins (e.g. loop combina...Thomas Bauereiss
2018-01-31add very stripped down 2-instruction RISCV example with add and load.Robert Norton
2018-01-31add some elf files from riscv test suite and run them on riscv model.Robert Norton
2018-01-30Handle 'N == 1 | 'N == 2 | ... style set constraints in monoBrian Campbell
2018-01-30Optionally give *all* monomorphisation errors at onceBrian Campbell
2018-01-30Fix monomorphisation analysis to detect type variables which need to beBrian Campbell
2018-01-30Fix failing Lem testsAlasdair Armstrong
2018-01-30Updates to C backendAlasdair Armstrong
2018-01-30riscv prelude: add a to_bits function for converting ints to bits of given le...Robert Norton
2018-01-30Generate functions from enums to numbers and vice versaAlasdair Armstrong
2018-01-29Fix Lem generation for RISC-VThomas Bauereiss
2018-01-29Add rreg effect to _reg_deref in fix_val_specs rewriteThomas Bauereiss
2018-01-29Output a few more type annotations for LemThomas Bauereiss
2018-01-29Add a fixme for unhandled fences but allow them to execute.Prashanth Mundkur
2018-01-29Initial handling of CSR reads/writes.Prashanth Mundkur
2018-01-29Add satp to CSR dummy implemented predicate. Also direct the illegal instruc...Prashanth Mundkur
2018-01-29use check target in makefile when checking riscv spec.Robert Norton
2018-01-29riscv: fix warnings about incomplete patterns. Add a check target in Makefile...Robert Norton
2018-01-29Sync mono rewrites definitions with libraryBrian Campbell
2018-01-29Look through let expressions when constructing nconstraintsBrian Campbell
2018-01-29Leave pure if-conditions in place instead of pulling out let-bindingsBrian Campbell
2018-01-29Set maximum split size to work with aarch64 no vectorBrian Campbell
2018-01-29Get typechecking to resolve overriding in remove numeral patterns rewriteBrian Campbell
2018-01-29Move subst to ast_util, use for guarded clauses rewriteBrian Campbell
2018-01-29Add some initial exception handling to the riscv execution loop.Prashanth Mundkur
2018-01-29Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Robert Norton
2018-01-29riscv: remove break from main loop and place val spec in prelude.Robert Norton
2018-01-29riscv: add tracing of register writes.Robert Norton
2018-01-29add tohost to value.mlRobert Norton
2018-01-29implement shift primitives in sail_lib.mlRobert Norton
2018-01-29Further updates to C backendAlasdair Armstrong
2018-01-29Added ecall/mret and exception support.Prashanth Mundkur
2018-01-29Fix a bug where structs containing unions would generate bad to_string functionsAlasdair Armstrong
2018-01-29Merge branch 'sail2' of https://bitbucket.org/Peter_Sewell/sail into sail2Alasdair Armstrong
2018-01-29Shaked removing generation of now-uncessary uint dependencyPeter Sewell
2018-01-29Linksem does not use uint anymoreShaked Flur
2018-01-29Fix error in RISCV: SLLI and SRLI were swapped...Robert Norton