Use eqy and sby to perform formal verification

This commit also changes passlist and skiplist format.

Author: Szelwiga

.ci.yml

@@ -2,7 +2,6 @@ stages:
   - check_code_format
   - build_binaries
   - run_parsing_and_formal_tests
-  - verify_formal_tests_passlist
   - run_large_designs_tests
   - optional_bsg_tests
 
@@ -12,13 +11,20 @@ check_format:
   stage: check_code_format
   script:
     - echo "Install dependencies"
-    - apt update && apt install -y git clang-format
+    - apt update && apt install -y git clang-format python3 jq
     - echo "Check code format"
     - ./.github/scripts/format_sources.sh
+    - exit_code=0
     - if ! git diff --exit-code; then
     -   echo "Format locally using ./.github/scripts/format_sources.sh"
-    -   /bin/false
+    -   exit_code=1
     - fi
+    - ./.github/scripts/sort_passlists.sh
+    - if ! git diff --exit-code; then
+    -   echo "Format locally using ./.github/scripts/format_sources.sh"
+    -   exit_code=1
+    - fi
+    - exit $exit_code
 
 build_binaries:
   stage: build_binaries
@@ -45,8 +51,7 @@ build_binaries:
     - echo "Build sv2v binary"
     - git submodule update --init --recursive --checkout third_party/sv2v
     - wget -qO- https://get.haskellstack.org/ | sh -s - -f -d /usr/local/bin
-    - make -j$(nproc) -C $PWD/third_party/sv2v
-    - cp third_party/sv2v/bin/sv2v out/release/bin/
+    - make build_sv2v -j$(nproc)
   artifacts:
     when: always
     paths:
@@ -129,18 +134,17 @@ formal_verification_simple_tests:
   script:
     - echo "Install dependencies"
     - apt update
-    - apt install -y $DEPENDENCIES_FOR_TESTING
+    - apt install -y $DEPENDENCIES_FOR_TESTING python3-click
+    - echo "Load submodules"
+    - git submodule sync
+    - git submodule update --init --checkout third_party/{eqy,sby}
+    - echo "Prepare eqy"
+    - make build_eqy build_sby -j $(nproc)
     - echo "Start testing"
     - export PATH="$PWD/out/current/bin:$PATH"
     - ./run_fv_tests.mk -j $(nproc) TEST_SUITE_DIR:="$DIR" TEST_SUITE_NAME:="$NAME" test
     - echo "Gather tests results"
-    - list_file="build/$NAME.performed_tests_list.txt"
-    - for result_json in build/tests/*/*/result.json; do
-    -   test_name=$(jq -r '.name' "${result_json}")
-    -   printf '%s:%s\n' "$NAME" "${test_name}" >> "$list_file"
-    - done
-    - set -o pipefail
-    - python3 ./tests/formal/results.py "build/tests/${NAME}" | tee "build/${NAME}_summary.txt"
+    - ./tests/formal/gather_fv_results.sh $NAME
   artifacts:
     when: always
     paths:
@@ -161,21 +165,17 @@ formal_verification_yosys_tests:
   script:
     - echo "Install dependencies"
     - apt update
-    - apt install -y $DEPENDENCIES_FOR_TESTING
+    - apt install -y $DEPENDENCIES_FOR_TESTING python3-click
     - echo "Load submodules"
     - git submodule sync
-    - git submodule update --init --recursive third_party/yosys
+    - git submodule update --init --checkout third_party/{eqy,sby,yosys}
+    - echo "Prepare eqy"
+    - make build_eqy build_sby -j $(nproc)
     - echo "Start testing"
     - export PATH="$PWD/out/current/bin:$PATH"
     - ./run_fv_tests.mk -j $(nproc) TEST_SUITE_DIR:="$DIR" TEST_SUITE_NAME:="$NAME" test
     - echo "Gather tests results"
-    - list_file="build/$NAME.performed_tests_list.txt"
-    - for result_json in build/tests/*/*/result.json; do
-    -   test_name=$(jq -r '.name' "${result_json}")
-    -   printf '%s:%s\n' "$NAME" "${test_name}" >> "$list_file"
-    - done
-    - set -o pipefail
-    - python3 ./tests/formal/results.py "build/tests/${NAME}" | tee "build/${NAME}_summary.txt"
+    - ./tests/formal/gather_fv_results.sh $NAME
   artifacts:
     when: always
     paths:
@@ -196,45 +196,22 @@ formal_verification_sv2v_tests:
   script:
     - echo "Install dependencies"
     - apt update
-    - apt install -y $DEPENDENCIES_FOR_TESTING
+    - apt install -y $DEPENDENCIES_FOR_TESTING python3-click
     - echo "Load submodules"
     - git submodule sync
-    - git submodule update --init --recursive --checkout third_party/sv2v
+    - git submodule update --init --checkout third_party/{sv2v,eqy,sby}
+    - echo "Prepare eqy"
+    - make build_eqy build_sby -j $(nproc)
     - echo "Start testing"
     - export PATH="$PWD/out/current/bin:$PATH"
     - ./run_fv_tests.mk -j $(nproc) TEST_SUITE_DIR:="$DIR" TEST_SUITE_NAME:="$NAME" test
     - echo "Gather tests results"
-    - list_file="build/$NAME.performed_tests_list.txt"
-    - for result_json in build/tests/*/*/result.json; do
-    -   test_name=$(jq -r '.name' "${result_json}")
-    -   printf '%s:%s\n' "$NAME" "${test_name}" >> "$list_file"
-    - done
-    - set -o pipefail
-    - python3 ./tests/formal/results.py "build/tests/${NAME}" | tee "build/${NAME}_summary.txt"
+    - ./tests/formal/gather_fv_results.sh $NAME
   artifacts:
     when: always
     paths:
       - build/
 
-verify_formal_tests_passlist:
-  stage: verify_formal_tests_passlist
-  dependencies: [formal_verification_simple_tests, formal_verification_yosys_tests, formal_verification_sv2v_tests]
-  only:
-    - main
-    - merge_requests
-  script:
-    - echo "Check if every test from passlist.txt was executed"
-    - sort build/*.performed_tests_list.txt > performed_tests_list.txt
-    - cat tests/formal/passlist.txt | sed '/^#/d' | sort > sorted_passlist.txt
-    - readarray not_performed_tests < <(comm -13 performed_tests_list.txt sorted_passlist.txt)
-    - if (( ${#not_performed_tests[@]} > 0 )); then
-    -   printf '\x1b[1mTests from passlist.txt that were not performed:\x1b[0m\n'
-    -   printf '\x1b[91m%s\x1b[0m\n' "${not_performed_tests[@]}"
-    -   exit 1
-    - else
-    -   exit 0
-    - fi
-
 veer_synth_large_design:
   stage: run_large_designs_tests
   dependencies: [build_binaries]

.github/scripts/run_group_test.sh

@@ -41,11 +41,17 @@ test_cases=( $(cd ${REPO_DIR}/tests && echo simple_tests/!(${filter_pat})) )
 global_status=0
 mkdir -p "$(dirname "$RESULTS_FILE")"
 
+declare -a failed_tests_list
+
 # Test
 
 cd $REPO_DIR
 for test_case in "${test_cases[@]}"; do
-    printf '::group::%s\n' "$test_case"
+    if [ -n "$GITHUB_ACTIONS" ]; then
+        printf '::group::%s\n' "$test_case"
+    else
+        printf "# %s #\n" "$test_case"
+    fi
     export test_case
     test_name="${test_case//tests\//}"
     test_name="${test_name//\//_}"
@@ -119,9 +125,25 @@ for test_case in "${test_cases[@]}"; do
     fi
 
     printf '%d\t%d\t%s\n' "$test_ok" "$asan_ok" "$test_name" >> "$RESULTS_FILE"
-    printf '::endgroup::\n'
+    if [ -n "$GITHUB_ACTIONS" ]; then
+        printf '::endgroup::\n'
+    else
+        if (( $test_ok == 1 )); then
+            printf "|  PASS\n\n"
+        else
+            failed_tests_list+=("$test_name")
+        fi
+    fi
 done
 
+if [ -z "$GITHUB_ACTIONS" ] && [[ $global_status -ne 0 ]]; then
+    echo "Failed tests list:"
+    for test_name in ${failed_tests_list[@]}
+    do
+		echo $test_name
+    done
+fi
+
 # Leave with non-zero error status if any test failed
 if [[ $global_status -ne 0 ]]; then
     exit 1

.github/scripts/sort_passlists.sh

@@ -7,11 +7,10 @@ declare -r SELF_DIR="$(dirname $(readlink -f ${BASH_SOURCE[0]}))"
 declare -r REPO_DIR=$SELF_DIR/../..
 cd $REPO_DIR
 
-files_to_sort_check=(
-    tests/formal/passlist.txt
-    tests/opentitan/opentitan_parsing_test/ot_cores_passlist.txt
-)
+opentitan_passlist="tests/opentitan/opentitan_parsing_test/ot_cores_passlist.txt"
+formal_testlist="tests/formal/testlist.json"
 
-for f in "${files_to_sort_check[@]}"; do
-    LC_ALL=C.UTF-8 sort -f -u -o $f $f
-done
+LC_ALL=C.UTF-8 sort -f -u -o $opentitan_passlist $opentitan_passlist
+
+cat $formal_testlist | jq -s -c 'sort_by(.d) | .[]' |  python3 -m json.tool > ${formal_testlist}.tmp
+mv ${formal_testlist}.tmp $formal_testlist

.github/workflows/formal-verification.yml

@@ -56,6 +56,7 @@ jobs:
               libgoogle-perftools-dev \
               python3 \
               python3-dev \
+              python3-click \
               swig \
               tcl-dev \
               tclsh \
@@ -68,8 +69,7 @@ jobs:
         run: |
           git submodule sync
           git submodule update --depth 1 --init --recursive --checkout \
-              third_party/yosys \
-              third_party/sv2v \
+              third_party/{yosys,sv2v,eqy,sby} \
               ;
 
       - name: Download binaries
@@ -87,6 +87,10 @@ jobs:
           name: sv2v
           path: out/current/bin/
 
+      - name: Build eqy and sby
+        run: |
+          make build_eqy build_sby -j$(nproc)
+
       - name: Test
         run: |
           chmod +x out/current/bin/sv2v
@@ -99,17 +103,12 @@ jobs:
 
       - name: Generate list of performed tests
         run: |
-          list_file="build/${TEST_SUITE_NAME}.performed_tests_list.txt"
-          touch "$list_file"
-          for result_json in build/tests/*/*/result.json; do
-            test_name=$(jq -r '.name' "${result_json}")
-            printf '%s:%s\n' "${TEST_SUITE_NAME}" "${test_name}" >> "$list_file"
-          done
+          ./tests/formal/gather_fv_results.sh $NAME
 
       - name: Pack formal verification logs
         run: |
           cd build
-          tar cf ${TEST_SUITE_NAME}.tar tests/*/*/*.out tests/*/*/slpp_all/*.log tests/*/*/*.txt tests/*/*/result.json
+          tar cf ${TEST_SUITE_NAME}.tar tests/*/*
 
       - name: Upload formal verification logs
         uses: actions/upload-artifact@v2

.github/workflows/main.yml

@@ -42,7 +42,7 @@ jobs:
       - name: Install dependencies
         run: |
           apt-get update -q
-          apt-get install -y clang-format
+          apt-get install -y git clang-format python3 jq
 
       - name: Sources format check
         run: |
@@ -243,20 +243,20 @@ jobs:
         run: |
           export PATH=$PWD/install/bin:/usr/local/bin:${PATH}
           wget -qO- https://get.haskellstack.org/ | sh -s - -f -d /usr/local/bin
-          make -j$(nproc) -C $PWD/third_party/sv2v
+          make build_sv2v -j$(nproc)
 
       - name: Upload binaries
         uses: actions/upload-artifact@v2
         with:
           name: sv2v
           path: |
-            third_party/sv2v/bin/sv2v
+            out/release/bin/sv2v
 
       - name: Save build results to cache
         if: ${{ steps.cache-restore.outputs.cache-hit != 'true' && ! (failure() || cancelled()) }}
         uses: actions/cache/save@v3
         with:
-          path: third_party/sv2v/bin/sv2v
+          path: out/release/bin/sv2v
           key: ${{ steps.cache-restore.outputs.cache-primary-key }}
 
       - name: Upload load graphs

.gitmodules

@@ -52,3 +52,11 @@
 	path = third_party/OpenROAD-flow-scripts
 	url = https://github.com/The-OpenROAD-Project/OpenROAD-flow-scripts.git
 	update = none
+[submodule "third_party/sby"]
+	path = third_party/sby
+	url = https://github.com/YosysHQ/sby
+	update = none
+[submodule "third_party/eqy"]
+	path = third_party/eqy
+	url = https://github.com/YosysHQ/eqy
+	update = none

Makefile

@@ -337,6 +337,9 @@ list :
 	printf '    %s\n' \
 			'list ${F.D}|${F.!D} help' \
 			'build' \
+			'build_eqy' \
+			'build_sby' \
+			'build_sv2v' \
 			'install' \
 			'clean' \
 			;
@@ -363,6 +366,21 @@ help : list
 .PHONY: build
 build : $(foreach t,${GetTargetsList}, @${t})
 
+.PHONY: build_eqy
+build_eqy : ${OUT_DIR}/bin/yosys-config
+	export PATH="$(realpath ${OUT_DIR})/bin:${PATH}"
+	${MAKE} -C third_party/eqy install PREFIX=$(realpath ${OUT_DIR})
+
+.PHONY: build_sby
+build_sby : ${OUT_DIR}/bin/yosys-config
+	export PATH="$(realpath ${OUT_DIR})/bin:${PATH}"
+	${MAKE} -C third_party/sby install PREFIX=$(realpath ${OUT_DIR})
+
+.PHONY: build_sv2v
+build_sv2v :
+	${MAKE} -C ./third_party/sv2v
+	mkdir -p ${OUT_DIR}/bin
+	cp ./third_party/sv2v/bin/sv2v ${OUT_DIR}/bin/sv2v
 
 .PHONY: install
 install : $(foreach t,${GetTargetsList}, install@${t})

README.md

@@ -152,6 +152,8 @@ If you encounter any problems with it, please compare the results with a single
 
 #### Prerequisites
 
+##### `sv2v`
+
 Formal Verification uses `sv2v` tool and tests from its repository, which is available as a submodule.
 To download the sv2v submodule run:
 
@@ -164,9 +166,25 @@ To build sv2v and copy it to `out/current/bin` (where it is expected to be by th
 
 <!-- name="sv2v-build" -->
 ``` bash
-wget -qO- https://get.haskellstack.org/ | sh -s - -f -d $PWD/out/current/bin
-make -j$(nproc) -C $PWD/third_party/sv2v
-cp ./third_party/sv2v/bin/sv2v ./out/current/bin
+    wget -qO- https://get.haskellstack.org/ | sh -s - -f -d $PWD/out/current/bin
+    make build_sv2v -j$(nproc) 
+```
+
+##### `eqy` and `sby`
+
+Formal Verification proves design equivalence using `eqy` and `sby` tools, which are included as submodules.
+To checkout the `eqy` and `sby` submodules, run:
+
+<!-- name="eqy-sby-update" -->
+``` bash
+   git submodule update --init --checkout third_party/{eqy,sby}
+```
+
+To build `eqy` and `sby` run:
+
+<!-- name="eqy-sby-build" -->
+``` bash
+    make build_eqy build_sby -j$(nproc) 
 ```
 
 #### Testing
@@ -189,9 +207,18 @@ To start formal verification tests, use `run_fv_tests.mk`, either as an executab
 * `test_suite_dir` - path to a tests directory (e.g. `./yosys/tests`). Required by all targets except `help`.
 * `test_suite_name` - when specified, it is used as a name of a directory inside `./build/` where results are stored. Otherwise results are stored directly inside the `./build/` directory.
 
-`yosys` and `sv2v` must be present in one of `PATH` directories.
+To gather formal verification results use: 
+``` bash
+    ./tests/formal/gather_fv_results.sh \
+        TEST_SUITE_NAME:=<test_suite_name>
+```
+
 For other dependencies, please see the `.github/workflows/formal-verification.yml` file.
 
+#### More details
+
+[Formal Verification README](https://github.com/chipsalliance/synlig/tree/main/tests/formal)
+
 #### Available Targets
 
 * ``help`` - Prints help.