Decrease formal verification logs size (#2576)

This PR decreases formal verification logs size by packing only useful logs to artifacts.
chipsalliance · Sep 19, 2024 · 146361a · 146361a
2 parents 6b113ce + be260df
commit 146361a
Show file tree

Hide file tree

Showing 3 changed files with 27 additions and 7 deletions.
diff --git a/.ci.yml b/.ci.yml
@@ -153,22 +153,22 @@ release_read_systemverilog:
   artifacts:
     when: always
     paths:
-      - build/
+      - ./*_formal_verification_logs.tar.gz
 
 simple_formal_verification_tests:
   <<: *formal_test
   script:
-    - ./tests/scripts/run_formal.sh --name simple install_dependencies load_submodules build_dependencies run gather_results
+    - ./tests/scripts/run_formal.sh --name simple install_dependencies load_submodules build_dependencies run pack_logs gather_results
 
 yosys_formal_verification_tests:
   <<: *formal_test
   script:
-    - ./tests/scripts/run_formal.sh --name yosys install_dependencies load_submodules build_dependencies run gather_results
+    - ./tests/scripts/run_formal.sh --name yosys install_dependencies load_submodules build_dependencies run pack_logs gather_results
 
 sv2v_formal_verification_tests:
   <<: *formal_test
   script:
-    - ./tests/scripts/run_formal.sh --name sv2v install_dependencies load_submodules build_dependencies run gather_results
+    - ./tests/scripts/run_formal.sh --name sv2v install_dependencies load_submodules build_dependencies run pack_logs gather_results
 
 .job_template: &large_design_test
   stage: "Run large designs tests"

diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml
@@ -73,15 +73,14 @@ jobs:
 
       - name: Pack formal verification logs
         run: |
-          cd build
-          tar cf ${TEST_SUITE_NAME}.tar tests/*/*
+          ./tests/scripts/run_formal.sh --name $TEST_SUITE_NAME pack_logs
 
       - name: Upload formal verification logs
         uses: actions/upload-artifact@v4
         with:
           name: formal-verification-logs-${{ matrix.name }}
           path: |
-            build/*.tar
+            ${{ matrix.name }}_formal_verification_logs.tar
 
       - name: Upload load graphs
         uses: actions/upload-artifact@v4

diff --git a/tests/scripts/run_formal.sh b/tests/scripts/run_formal.sh
@@ -40,6 +40,7 @@ do
 		echo "    load_submodules        - clones necessary submodules"
 		echo "    run                    - launches FV"
 		echo "    gather_results         - gathers results of FV"
+		echo "    pack_logs              - creates .tar.gz archive with selected logs"
 		echo ""
 		echo "    List of supported test suite names:"
 		echo "        simple"
@@ -66,6 +67,26 @@ do
 		[ "$name" == "'yosys'" ] && gather_results yosys ./third_party/yosys/tests
 		[ "$name" == "'sv2v'" ] && gather_results sv2v
 	;;
+	"'pack_logs'")
+		(
+			shopt -s extglob nullglob
+			[ -z "$GITHUB_ACTIONS" ] && echo "##/ Pack logs \##"
+			LOGFILE=${name//\'/}_formal_verification_logs.tar
+			DIRNAME=./build/tests/${name//\'/}
+			tar -cf ${LOGFILE} \
+				${DIRNAME}/*/result.json \
+				${DIRNAME}/*/*.sv \
+				${DIRNAME}/*/*.v \
+				${DIRNAME}/*/*.eqy \
+				${DIRNAME}/*/*/*.log \
+				${DIRNAME}/*/*/*.txt \
+				${DIRNAME}/*/*/*.ids \
+				${DIRNAME}/*/*/*.list \
+				${DIRNAME}/*/*/*.ys
+			find ${DIRNAME} -name logfile.txt -exec tar --append --file=${LOGFILE} {} +
+			gzip $LOGFILE
+		)
+	;;
 	--)
 		if [ -z $name ]; then
 			echo "Test suite name is not provided!"