Move to building untracked files in subdirectories to improve cleaning
This commit is contained in:
2
.gitignore
vendored
Normal file
2
.gitignore
vendored
Normal file
@@ -0,0 +1,2 @@
|
|||||||
|
build/
|
||||||
|
counterexamples/
|
||||||
39
Makefile
39
Makefile
@@ -13,30 +13,37 @@ ifeq ($(ARCH), RISCV)
|
|||||||
BSCFLAGS += -D RISCV
|
BSCFLAGS += -D RISCV
|
||||||
endif
|
endif
|
||||||
|
|
||||||
BSV_VERILOG_WRAPPERS_DIR ?= $(CURDIR)
|
BSV_VERILOG_WRAPPERS_DIR ?= $(CURDIR)/build/
|
||||||
BSCFLAGS += -vdir $(BSV_VERILOG_WRAPPERS_DIR)
|
BUILD_DIR = $(BSV_VERILOG_WRAPPERS_DIR)
|
||||||
|
COUNTEREXAMPLE_DIR = $(CURDIR)/counterexamples/
|
||||||
|
BSCFLAGS += -bdir $(BUILD_DIR)
|
||||||
|
|
||||||
all: verilog-wrappers blarney-wrappers
|
all: verilog-wrappers blarney-wrappers
|
||||||
|
|
||||||
verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv
|
$(BUILD_DIR):
|
||||||
bsc $(BSCFLAGS) -verilog -u $<
|
mkdir -p $@
|
||||||
|
|
||||||
verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv
|
$(COUNTEREXAMPLE_DIR):
|
||||||
bsc $(BSCFLAGS) -verilog -u $<
|
mkdir -p $@
|
||||||
|
|
||||||
check-prop: assertions.sv verilog-wrappers verilog-props
|
verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR)
|
||||||
sby -f check.sby
|
bsc $(BSCFLAGS) -vdir $(BSV_VERILOG_WRAPPERS_DIR) -verilog -u $<
|
||||||
|
|
||||||
blarney-wrappers: CHERICapWrap.py verilog-wrappers
|
verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR) $(COUNTEREXAMPLE_DIR)
|
||||||
./CHERICapWrap.py -o CHERIBlarneyWrappers *.v
|
bsc $(BSCFLAGS) -vdir $(COUNTEREXAMPLE_DIR) -verilog -u $<
|
||||||
|
|
||||||
.PHONY: clean clean-verilog-wrappers
|
check-prop: assertions.sv verilog-props $(COUNTEREXAMPLE_DIR)
|
||||||
|
sby --prefix $(COUNTEREXAMPLE_DIR) -f check.sby
|
||||||
|
|
||||||
clean-verilog-wrappers: clean
|
blarney-wrappers: CHERICapWrap.py verilog-wrappers $(BUILD_DIR)
|
||||||
rm -f *.v
|
./CHERICapWrap.py -o $(BUILD_DIR)/CHERIBlarneyWrappers $(BUILD_DIR)/*.v
|
||||||
|
|
||||||
clean-blarney-wrappers: clean
|
.PHONY: clean clean-counterexamples full-clean
|
||||||
rm -f *.hs
|
|
||||||
|
clean-counterexamples:
|
||||||
|
rm -rf $(COUNTEREXAMPLE_DIR)
|
||||||
|
|
||||||
clean:
|
clean:
|
||||||
rm -f *.bo
|
rm -rf $(BUILD_DIR)
|
||||||
|
|
||||||
|
full-clean: clean clean-counterexamples
|
||||||
|
|||||||
18
check.sby
18
check.sby
@@ -39,12 +39,12 @@ prop_fromToMem: prep -top assert_prop_fromToMem
|
|||||||
|
|
||||||
[files]
|
[files]
|
||||||
assertions.sv
|
assertions.sv
|
||||||
module_prop_unique.v
|
counterexamples/module_prop_unique.v
|
||||||
module_prop_exact.v
|
counterexamples/module_prop_exact.v
|
||||||
module_prop_exactConditions.v
|
counterexamples/module_prop_exactConditions.v
|
||||||
module_prop_getBase.v
|
counterexamples/module_prop_getBase.v
|
||||||
module_prop_getTop.v
|
counterexamples/module_prop_getTop.v
|
||||||
module_prop_getLength.v
|
counterexamples/module_prop_getLength.v
|
||||||
module_prop_isInBounds.v
|
counterexamples/module_prop_isInBounds.v
|
||||||
module_prop_setAddr.v
|
counterexamples/module_prop_setAddr.v
|
||||||
module_prop_fromToMem.v
|
counterexamples/module_prop_fromToMem.v
|
||||||
|
|||||||
Reference in New Issue
Block a user