[acl2/acl2] 08a2a7: A preliminary partial model of the RISC-V ISA.

[Alessandro Coglio]

Branch: refs/heads/testing-user-01
Home: https://github.com/acl2/acl2
Commit: 08a2a7ad08b0d429524e690bdc1ad7b383844249
https://github.com/acl2/acl2/commit/08a2a7ad08b0d429524e690bdc1ad7b383844249
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2022-07-31 (Sun, 31 Jul 2022)

Changed paths:
A books/kestrel/risc-v/README.md
A books/kestrel/risc-v/acl2-customization.lsp
A books/kestrel/risc-v/bytes.lisp
A books/kestrel/risc-v/cert.acl2
A books/kestrel/risc-v/decoding.lisp
A books/kestrel/risc-v/examples.lisp
A books/kestrel/risc-v/execution.lisp
A books/kestrel/risc-v/instructions.lisp
A books/kestrel/risc-v/library-extensions.lisp
A books/kestrel/risc-v/package.lsp
A books/kestrel/risc-v/portcullis.acl2
A books/kestrel/risc-v/portcullis.lisp
A books/kestrel/risc-v/semantics.lisp
A books/kestrel/risc-v/state.lisp
A books/kestrel/risc-v/top.lisp
M books/kestrel/top.lisp

Log Message:
-----------
A preliminary partial model of the RISC-V ISA.

This is very preliminary -- literally a weekend's work (done a couple of years
ago), including studying the relevant RISC-V documentation. It is barely
documented and tested. Yet, it seems useful to put it in the community books,
even in this form.


Commit: aab6ba51eb54482026d57992f58fe97708d05256
https://github.com/acl2/acl2/commit/aab6ba51eb54482026d57992f58fe97708d05256
Author: Alessandro Coglio <cog...@kestrel.edu>
Date: 2022-07-31 (Sun, 31 Jul 2022)

Changed paths:
M books/acl2s/ccg/ccg.lisp
M books/acl2s/cgen/prove-cgen.lisp
M books/doc/relnotes.lisp
M books/kestrel/apt/simplify-defun-impl.lisp
M books/kestrel/apt/simplify-defun-tests.lisp
M books/kestrel/axe/prove-with-stp-tests.lisp
M books/kestrel/axe/rewriter.lisp
M books/kestrel/axe/x86/lifter.lisp
M books/kestrel/axe/x86/unroll-x86-code.lisp
R books/kestrel/bv/bv-tests.lisp
M books/kestrel/bv/defs.lisp
A books/kestrel/bv/tests.lisp
M books/kestrel/bv/top.lisp
M books/kestrel/doc.lisp
M books/kestrel/fty/defresult.lisp
A books/kestrel/htclient/acl2-customization.lsp
A books/kestrel/htclient/cert.acl2
A books/kestrel/htclient/package.lsp
A books/kestrel/htclient/portcullis.acl2
A books/kestrel/htclient/portcullis.lisp
A books/kestrel/htclient/post-logic.lisp
A books/kestrel/htclient/post-raw.lsp
A books/kestrel/htclient/post.lisp
A books/kestrel/htclient/top.lisp
M books/kestrel/json-parser/parse-json-tests.lisp
M books/kestrel/json-parser/parse-json.lisp
M books/kestrel/top.lisp
M books/kestrel/x86/package.lsp
M books/misc/expander.lisp
M books/misc/simplify-defuns.lisp
M books/projects/codewalker/simplify-under-hyps.lisp
M books/quicklisp/base-raw.lsp
A books/quicklisp/dexador-raw.lsp
A books/quicklisp/dexador.lisp
M books/system/doc/acl2-doc.lisp
M books/tools/prove-dollar.lisp
M books/tools/rewrite-dollar.lisp
M books/tools/stobj-frame.lisp
M books/workshops/2003/kaufmann/support/tool/simplify-defuns.lisp
M doc.lisp
M doc/acl2-code-size.txt
M doc/home-page.html
M proof-builder-b.lisp
M prove.lisp
M rewrite.lisp

Log Message:
-----------
Merge.


Compare: https://github.com/acl2/acl2/compare/75aa25c0126d...aab6ba51eb54

[Alessandro Coglio]

Branch: refs/heads/master

[Alessandro Coglio]

Branch: refs/heads/testing-kestrel

[Alessandro Coglio]

Branch: refs/heads/testing