diff options
| -rw-r--r-- | riscv/Makefile | 6 | ||||
| -rw-r--r-- | riscv/riscv_prelude.h | 19 |
2 files changed, 22 insertions, 3 deletions
diff --git a/riscv/Makefile b/riscv/Makefile index e5e21709..20ff8160 100644 --- a/riscv/Makefile +++ b/riscv/Makefile @@ -32,10 +32,10 @@ coverage: _sbuild/coverage.native mkdir bisect && mv bisect*.out bisect/ mkdir coverage && bisect-ppx-report -html coverage/ -I _sbuild/ bisect/bisect*.out -riscv.c: $(SAIL_SRCS) main.sail Makefile - $(SAIL) -O -memo_z3 -c $(SAIL_SRCS) main.sail 1> $@ +riscv.c: $(SAIL_SRCS) main.sail Makefile riscv_prelude.h + $(SAIL) -O -memo_z3 -c -c_include "riscv_prelude.h" $(SAIL_SRCS) main.sail 1> $@ -riscv_c: riscv.c +riscv_c: riscv.c Makefile gcc -O2 riscv.c ../lib/*.c -lgmp -lz -I ../lib -o riscv_c latex: $(SAIL_SRCS) Makefile diff --git a/riscv/riscv_prelude.h b/riscv/riscv_prelude.h new file mode 100644 index 00000000..94f02b83 --- /dev/null +++ b/riscv/riscv_prelude.h @@ -0,0 +1,19 @@ +#include "sail.h" +#include "rts.h" + +void string_append(sail_string *dst, sail_string s1, sail_string s2); +bool string_startswith(sail_string s, sail_string prefix); +void string_length(sail_int *len, sail_string s); +void string_drop(sail_string *dst, sail_string s, sail_int len); +unit print_string(sail_string prefix, sail_string msg); + +void add_vec(sail_bits *dst, sail_bits s1, sail_bits s2); +void add_vec_int(sail_bits *dst, sail_bits src, sail_int i); + +void sub_vec(sail_bits *dst, sail_bits s1, sail_bits s2); +void sub_vec_int(sail_bits *dst, sail_bits src, sail_int i); + +void not_vec(sail_bits *dst, sail_bits src); +void xor_vec(sail_bits *dst, sail_bits s1, sail_bits s2); + + |