summaryrefslogtreecommitdiff
path: root/riscv/Makefile
diff options
context:
space:
mode:
authorRobert Norton2018-02-01 15:23:14 +0000
committerRobert Norton2018-02-01 15:23:27 +0000
commitda1d186e16fa4dc0419acf7a0fd59101da993de6 (patch)
treefd5a27c88974ae601fdbe2ef2cd13445f7da6048 /riscv/Makefile
parent0a9e8c4bf32f1b470d32031496dd1cb90adb6888 (diff)
Clean up riscv_duopod sail and add make targets for ocaml and Isabelle.
Diffstat (limited to 'riscv/Makefile')
-rw-r--r--riscv/Makefile14
1 files changed, 14 insertions, 0 deletions
diff --git a/riscv/Makefile b/riscv/Makefile
index 7f52dde7..aeba80ef 100644
--- a/riscv/Makefile
+++ b/riscv/Makefile
@@ -11,6 +11,19 @@ check: $(SAIL_SRCS) main.sail
riscv: $(SAIL_SRCS) main.sail
$(SAIL_DIR)/sail -ocaml -o riscv $^
+riscv_duopod_ocaml: prelude.sail riscv_duopod.sail
+ $(SAIL_DIR)/sail -ocaml -o $@ $^
+
+riscv_duopod_embed_sequential.lem: prelude.sail riscv_duopod.sail
+ $(SAIL_DIR)/sail -lem -lem_sequential -lem_mwords -lem_lib Riscv_extras_embed -o riscv_duopod $^
+Riscv_duopod_embed_sequential.thy: riscv_duopod_embed_sequential.lem riscv_extras_embed_sequential.lem
+ lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
+ riscv_extras_embed_sequential.lem \
+ riscv_duopod_embed_types_sequential.lem \
+ riscv_duopod_embed_sequential.lem
+
+riscv_duopod: riscv_duopod_ocaml Riscv_duopod_embed_sequential.thy
+
Riscv_embed_sequential.thy: riscv_embed_sequential.lem riscv_extras_embed_sequential.lem
lem -isa -outdir . -lib ../src/lem_interp -lib ../src/gen_lib \
riscv_extras_embed_sequential.lem \
@@ -25,3 +38,4 @@ clean:
-rm -f riscv_embed_sequential.lem riscv_embed_types_sequential.lem
-rm -f Riscv_embed_sequential.thy Riscv_embed_types_sequential.thy \
Riscv_extras_embed_sequential.thy
+ -rm -f Riscv_duopod_embed_sequential.thy Riscv_duopod_embed_types_sequential.thy riscv_duopod_embed_sequential.lem riscv_duopod_embed_types_sequential.lem