Refactor cdc_2phase_clearable and extend its tests

.gitignore

@@ -9,6 +9,8 @@ build
 formal/fifo
 formal/counter
 formal/fall_through_register
+formal/cdc_reset_ctrlr_half
+formal/cdc_reset_ctrlr_composed
 *.check
 *.vcd
 obj_dir/

formal/Makefile

@@ -1,21 +1,28 @@
-# Copyright (c) 2019 ETH Zurich, University of Bologna
+# Copyright 2019 ETH Zurich and University of Bologna.
 #
 # Copyright and related rights are licensed under the Solderpad Hardware
 # License, Version 0.51 (the "License"); you may not use this file except in
-# compliance with the License.  You may obtain a copy of the License at
+# compliance with the License. You may obtain a copy of the License at
 # http://solderpad.org/licenses/SHL-0.51. Unless required by applicable law
 # or agreed to in writing, software, hardware and materials distributed under
 # this License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR
 # CONDITIONS OF ANY KIND, either express or implied. See the License for the
 # specific language governing permissions and limitations under the License.
 
-# Author: Robert Balas <balasr@iis.ee.ethz.ch>
+# Authors:
+# - Robert Balas <balasr@iis.ee.ethz.ch>
+# - Philippe Sauter <phsauter@iis.ee.ethz.ch>
+#
+# Description: Formal Verification Targets
+# Dispatch SymbiYosys proof runs for common_cells formal properties, including
+# reset-controller half and composed CDC clear-sequencing checks.
 
 YOSYS	?= yosys
 SBY	?= sby
 RM	?= rm
 
-all: fifo.check counter.check fall_through_register.check
+all: fifo.check counter.check fall_through_register.check cdc_reset_ctrlr_half.check \
+	cdc_reset_ctrlr_composed.check
 
 fifo.check: fifo.sby ../src/cc_fifo.sv cc_fifo_properties.sv
 	$(SBY) -f $<
@@ -34,9 +41,24 @@ fall_through_register.check: fall_through_register.sby ../src/cc_fall_through_re
 	$(SBY) -f $<
 	touch $@
 
+cdc_reset_ctrlr_half.check: cdc_reset_ctrlr_half.sby cc_cdc_reset_ctrlr_half_properties.sv \
+				../src/cc_cdc_reset_ctrlr.sv ../src/cc_cdc_4phase.sv \
+				../src/cc_sync.sv ../src/cc_pkg.sv
+	./run_cdc_reset_ctrlr_half.sh
+	touch $@
+
+cdc_reset_ctrlr_composed.check: cdc_reset_ctrlr_composed.sby cc_cdc_reset_ctrlr_properties.sv \
+				cc_cdc_reset_ctrlr_half_properties.sv \
+				../src/cc_cdc_reset_ctrlr.sv ../src/cc_cdc_4phase.sv \
+				../src/cc_sync.sv ../src/cc_pkg.sv
+	./run_cdc_reset_ctrlr_composed.sh
+	touch $@
+
 .PHONY: clean
 clean:
 	$(RM) -r fifo.check fifo/
 #	$(RM) -r delta_counter.check delta_counter/
 	$(RM) -r counter.check counter/
 	$(RM) -r fall_through_register.check fall_through_register/
+	$(RM) -r cdc_reset_ctrlr_half.check cdc_reset_ctrlr_half/
+	$(RM) -r cdc_reset_ctrlr_composed.check cdc_reset_ctrlr_composed/