aboutsummaryrefslogtreecommitdiffstats
path: root/Makefile
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-08-30 14:03:40 +0100
committerYann Herklotz <git@yannherklotz.com>2020-08-30 14:03:40 +0100
commitec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a (patch)
treeaba30758bbbf10ab3d975367f48a695b81afb179 /Makefile
parent9d6979baa0e4b505862bcedee1dfd075f36579c3 (diff)
downloadvericert-ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a.tar.gz
vericert-ec319c9ec0acc975fcdfbfa2e378b82c9be9ab0a.zip
Add RTLBlock intermediate language
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile7
1 files changed, 4 insertions, 3 deletions
diff --git a/Makefile b/Makefile
index 2935c7f..e1a93f6 100644
--- a/Makefile
+++ b/Makefile
@@ -9,8 +9,9 @@ endif
COMPCERTRECDIRS := lib common x86_32 x86 backend cfrontend driver flocq exportclight \
MenhirLib cparser
-COQINCLUDES := -R src/common vericert.common -R src/verilog vericert.verilog \
- -R src/extraction vericert.extraction -R src/translation vericert.translation \
+COQINCLUDES := -R src/common vericert.common \
+ -R src/extraction vericert.extraction \
+ -R src/hls vericert.hls \
-R src vericert \
$(foreach d, $(COMPCERTRECDIRS), -R lib/CompCert/$(d) compcert.$(d))
@@ -19,7 +20,7 @@ COQMAKE := $(COQBIN)coq_makefile
COQDOCFLAGS := --no-lib-name -l
-VS := src/Compiler.v src/Simulator.v $(foreach d, translation common verilog, src/$(d)/*.v)
+VS := src/Compiler.v src/Simulator.v $(foreach d, common hls, src/$(d)/*.v)
PREFIX ?= .