Use eqy and sby to perform formal verification (#2529)

This PR changes the way Formal Verification is performed.

Up to now, some of the tests were failing because we failed to prove
equivalence (but it doesn't mean that we proved that they aren't
equivalent). FV is now performed using `eqy` and `sby` tools, which
lowers false-negative (and positive) tests.

.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

@@ -14,20 +14,15 @@ jobs:
       matrix:
         include:
           - name: simple
-            test-suite: tests/simple_tests
           - name: sv2v
-            test-suite: third_party/sv2v/test
           - name: yosys
-            test-suite: third_party/yosys/tests
       fail-fast: false
     name: ${{ matrix.name }}
     env:
       GIT_HTTP_LOW_SPEED_LIMIT: 1
       GIT_HTTP_LOW_SPEED_TIME: 600
       DEBIAN_FRONTEND: noninteractive
       GHA_MACHINE_TYPE: "n2-highmem-8"
-      PARSER: yosys-plugin
-      TEST_SUITE_DIR: ${{ matrix.test-suite }}
       TEST_SUITE_NAME: ${{ matrix.name }}
 
     steps:
@@ -42,35 +37,12 @@ jobs:
 
       - name: Install dependencies
         run: |
-          apt-get update -q
-          apt-get install -y \
-              ant \
-              build-essential \
-              cmake \
-              default-jre \
-              flex \
-              git \
-              google-perftools \
-              jq \
-              libfl-dev \
-              libgoogle-perftools-dev \
-              python3 \
-              python3-dev \
-              swig \
-              tcl-dev \
-              tclsh \
-              time \
-              uuid \
-              uuid-dev \
-              ;
+          ./tests/scripts/run_formal.sh --name $TEST_SUITE_NAME install_dependencies
+
 
       - name: Checkout submodules
         run: |
-          git submodule sync
-          git submodule update --depth 1 --init --recursive --checkout \
-              third_party/yosys \
-              third_party/sv2v \
-              ;
+          ./tests/scripts/run_formal.sh --name $TEST_SUITE_NAME load_submodules
 
       - name: Download binaries
         uses: actions/download-artifact@v2
@@ -87,29 +59,21 @@ jobs:
           name: sv2v
           path: out/current/bin/
 
+      - name: Build eqy and sby
+        run: |
+          ./tests/scripts/run_formal.sh --name $TEST_SUITE_NAME build_dependencies
+
       - name: Test
         run: |
           chmod +x out/current/bin/sv2v
           source .github/scripts/common.sh
-          export PATH="$PWD/out/current/bin:$PATH"
-          ./run_fv_tests.mk -j$(nproc) \
-              TEST_SUITE_DIR:="$(realpath ${TEST_SUITE_DIR})" \
-              TEST_SUITE_NAME:="${TEST_SUITE_NAME}" \
-              test
+          ./tests/scripts/run_formal.sh  --name $TEST_SUITE_NAME run
 
-      - 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
 
       - 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
@@ -118,12 +82,6 @@ jobs:
           path: |
             build/*.tar
 
-      - name: Upload list of performed tests
-        uses: actions/upload-artifact@v2
-        with:
-          name: formal-verification-tests-list
-          path: build/*.performed_tests_list.txt
-
       - name: Upload load graphs
         uses: actions/upload-artifact@v2
         with:
@@ -135,34 +93,5 @@ jobs:
       - name: Check results and print a summary
         run: |
           set -o pipefail
-          python3 ./tests/formal/results.py "build/tests/${TEST_SUITE_NAME}" | tee $GITHUB_STEP_SUMMARY
-
-  passlist-check:
-    name: Passlist Check
-    needs: tests-formal-verification
-    if: ${{ !cancelled() }}
-    runs-on: [self-hosted, Linux, X64, gcp-custom-runners]
-    container: ubuntu:jammy-20221130
+          ./tests/scripts/run_formal.sh --name $TEST_SUITE_NAME gather_results | tee $GITHUB_STEP_SUMMARY
 
-    steps:
-      - uses: actions/checkout@v3
-        with:
-          fetch-depth: 1
-
-      - name: Download lists of performed tests
-        uses: actions/download-artifact@v2
-        with:
-          name: formal-verification-tests-list
-
-      - name: Compare lists
-        run: |
-          sort *.performed_tests_list.txt > performed_tests_list.txt
-          grep -o '^[^ #]\+' tests/formal/passlist.txt | 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