search

riscv / riscv-bitmanip

Working draft of the proposed RISC-V Bitmanipulation extension
https://jira.riscv.org/browse/RVG-122
Creative Commons Attribution 4.0 International
206 stars 66 forks source link

Update Sail RISC-V model for BitManip #85

Open kdockser opened 3 years ago

kdockser commented 3 years ago

The Sail model needs to be updated to include the proposed bitmanip instructions. This needs to be done in such a way so as to enable the generation of emulators (OCaml and C) as well as theorem prover definitions.

ben-marshall commented 3 years ago

If it helps - I extended the parse_opcodes.py script from riscv-opcodes to generate lots of SAIL boilerplate. This is what I've used for the WIP crypto SAIL models. See riscv-crypto/bin/parse_opcodes.py for the script. I'm not proud of it, but it saved me a lot of time.

Example usage:

cat <bitmanip opcodes text file> | python3 ./bin/parse_opcodes.py -sail-boilerplate

Some disclaimers - it doesn't necessarily generate SAIL in the same way that the sail-riscv repository structures it. It generates a single AST entry per instruction from an opcodes-* file, rather than one AST for multiple instructions like the handwritten code does. It's easy enough to bash the generated output into this shape though. The most useful part of it is to very quickly generate the encode/decode/disassembly clauses.