diff options
| -rw-r--r-- | Makefile | 2 | ||||
| -rw-r--r-- | model/riscv_termination_duo.sail | 1 |
2 files changed, 2 insertions, 1 deletions
@@ -289,7 +289,7 @@ riscv_coq_build: generated_definitions/coq/$(ARCH)/riscv.vo $(addprefix generated_definitions/coq/$(ARCH)/,riscv.v riscv_types.v): $(SAIL_COQ_SRCS) Makefile mkdir -p generated_definitions/coq/$(ARCH) $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv -coq_lib riscv_extras $(SAIL_COQ_SRCS) -$(addprefix generated_definitions/coq/$(ARCH)/,riscv_duopod.v riscv_duopod_types.v): $(PRELUDE_SRCS) model/riscv_duopod.sail +$(addprefix generated_definitions/coq/$(ARCH)/,riscv_duopod.v riscv_duopod_types.v): $(PRELUDE_SRCS) model/riscv_duopod.sail model/riscv_termination_duo.sail mkdir -p generated_definitions/coq/$(ARCH) $(SAIL) $(SAIL_FLAGS) -dcoq_undef_axioms -coq -coq_output_dir generated_definitions/coq/$(ARCH) -o riscv_duopod -coq_lib riscv_extras $^ diff --git a/model/riscv_termination_duo.sail b/model/riscv_termination_duo.sail new file mode 100644 index 0000000..74ee253 --- /dev/null +++ b/model/riscv_termination_duo.sail @@ -0,0 +1 @@ +termination_measure n_leading_spaces s = string_length(s) |