diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..10a199a
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1,2 @@
+build/
+counterexamples/
diff --git a/Makefile b/Makefile
index a98e422..ac2af28 100644
--- a/Makefile
+++ b/Makefile
@@ -13,30 +13,37 @@ ifeq ($(ARCH), RISCV)
 BSCFLAGS += -D RISCV
 endif
 
-BSV_VERILOG_WRAPPERS_DIR ?= $(CURDIR)
-BSCFLAGS += -vdir $(BSV_VERILOG_WRAPPERS_DIR)
+BSV_VERILOG_WRAPPERS_DIR ?= $(CURDIR)/build/
+BUILD_DIR = $(BSV_VERILOG_WRAPPERS_DIR)
+COUNTEREXAMPLE_DIR = $(CURDIR)/counterexamples/
+BSCFLAGS += -bdir $(BUILD_DIR)
 
 all: verilog-wrappers blarney-wrappers
 
-verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv
-	bsc $(BSCFLAGS) -verilog -u $<
+$(BUILD_DIR):
+	mkdir -p $@
 
-verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv
-	bsc $(BSCFLAGS) -verilog -u $<
+$(COUNTEREXAMPLE_DIR):
+	mkdir -p $@
 
-check-prop: assertions.sv verilog-wrappers verilog-props
-	sby -f check.sby
+verilog-wrappers: CHERICapWrap.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR)
+	bsc $(BSCFLAGS) -vdir $(BSV_VERILOG_WRAPPERS_DIR) -verilog -u $<
 
-blarney-wrappers: CHERICapWrap.py verilog-wrappers
-	./CHERICapWrap.py -o CHERIBlarneyWrappers *.v
+verilog-props: CHERICapProps.bsv CHERICap.bsv CHERICC_Fat.bsv $(BUILD_DIR) $(COUNTEREXAMPLE_DIR)
+	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
-	rm -f *.v
+blarney-wrappers: CHERICapWrap.py verilog-wrappers $(BUILD_DIR)
+	./CHERICapWrap.py -o $(BUILD_DIR)/CHERIBlarneyWrappers $(BUILD_DIR)/*.v
 
-clean-blarney-wrappers: clean
-	rm -f *.hs
+.PHONY: clean clean-counterexamples full-clean
+
+clean-counterexamples:
+	rm -rf $(COUNTEREXAMPLE_DIR)
 
 clean:
-	rm -f *.bo
+	rm -rf $(BUILD_DIR)
+
+full-clean: clean clean-counterexamples
diff --git a/check.sby b/check.sby
index 9e26204..2f9058e 100644
--- a/check.sby
+++ b/check.sby
@@ -39,12 +39,12 @@ prop_fromToMem: prep -top assert_prop_fromToMem
 
 [files]
 assertions.sv
-module_prop_unique.v
-module_prop_exact.v
-module_prop_exactConditions.v
-module_prop_getBase.v
-module_prop_getTop.v
-module_prop_getLength.v
-module_prop_isInBounds.v
-module_prop_setAddr.v
-module_prop_fromToMem.v
+counterexamples/module_prop_unique.v
+counterexamples/module_prop_exact.v
+counterexamples/module_prop_exactConditions.v
+counterexamples/module_prop_getBase.v
+counterexamples/module_prop_getTop.v
+counterexamples/module_prop_getLength.v
+counterexamples/module_prop_isInBounds.v
+counterexamples/module_prop_setAddr.v
+counterexamples/module_prop_fromToMem.v