Add chipsalliance/sv-tests to CI

.github/workflows/pull-request-checks.yaml

@@ -264,6 +264,59 @@ jobs:
       - name: vlindex on Hazard3
         run: PATH=$PATH:$PWD/vlindex examples/Hazard3/Hazard3-vlindex.sh
 
+  # This job takes approximately 1 minute
+  sv-tests:
+    runs-on: ubuntu-24.04
+    needs: check-ubuntu-24_04-make-clang
+    steps:
+      - uses: actions/checkout@v7
+      - name: Fetch dependencies
+        env:
+          DEBIAN_FRONTEND: noninteractive
+        run: |
+          sudo apt-get remove --purge man-db
+          packages_to_install="python3-pip"
+          if ! sudo apt-get install --no-install-recommends -yq $packages_to_install ; then
+            sudo apt-get update
+            sudo apt-get install --no-install-recommends -yq $packages_to_install
+          fi
+      - name: Get the ebmc binary
+        uses: actions/download-artifact@v8
+        with:
+          name: ebmc-binary
+          path: ebmc
+      - name: Try the ebmc binary
+        run: chmod a+x ./ebmc/ebmc ; ./ebmc/ebmc --version
+      - name: Run sv-tests with ebmc
+        run: PATH=$PATH:$PWD/ebmc examples/chipsalliance-sv-tests/sv-tests.sh
+      - name: Upload sv-tests report
+        uses: actions/upload-artifact@v7
+        if: always()
+        with:
+          name: sv-tests-report
+          path: sv-tests/out/report/
+          retention-days: 5
+      - name: Upload sv-tests report for GitHub Pages
+        uses: actions/upload-pages-artifact@v3
+        if: github.ref == 'refs/heads/main'
+        with:
+          path: sv-tests/out/report/
+
+  deploy-sv-tests-report:
+    runs-on: ubuntu-24.04
+    needs: sv-tests
+    if: github.ref == 'refs/heads/main'
+    permissions:
+      pages: write
+      id-token: write
+    environment:
+      name: github-pages
+      url: ${{ steps.deployment.outputs.page_url }}
+    steps:
+      - name: Deploy to GitHub Pages
+        id: deployment
+        uses: actions/deploy-pages@v4
+
   # This job takes approximately 15 minutes
   check-centos8-make-gcc:
     name: CentOS 8

examples/chipsalliance-sv-tests/ebmc.py

@@ -0,0 +1,49 @@
+#!/usr/bin/env python3
+# -*- coding: utf-8 -*-
+
+from BaseRunner import BaseRunner
+import os
+
+class ebmc(BaseRunner):
+    def __init__(self):
+        super().__init__(
+            'ebmc', 'ebmc', {
+                'preprocessing', 'parsing', 'elaboration'
+            })
+
+        self.submodule = "third_party/tools/ebmc"
+        self.url = f"https://github.com/diffblue/hw-cbmc/tree/{self.get_commit()}"
+
+    def prepare_run_cb(self, tmp_dir, params):
+        ofile = 'ebmc.out'
+
+        self.cmd = [self.executable]
+
+        if params['mode'] == 'preprocessing':
+            self.cmd.append('--preprocess')
+        elif params['mode'] == 'parsing':
+            self.cmd += ['--show-parse']
+
+        if params['top_module'] != '':
+            self.cmd += ['--module', params['top_module']]
+
+        for incdir in params['incdirs']:
+            self.cmd.append('-I' + incdir)
+
+        for define in params['defines']:
+            self.cmd.append('-D' + define)
+
+        self.cmd += params['files']
+
+    def get_version_cmd(self):
+        return [self.executable, "--version"]
+
+    def get_version(self):
+        version = super().get_version()
+
+        # The full version is the 1st line
+        version = version.splitlines()[0].split()
+
+        version.insert(0, self.name)
+
+        return " ".join(version)

examples/chipsalliance-sv-tests/sv-tests.sh

@@ -0,0 +1,69 @@
+#!/bin/sh
+
+# abort on error
+set -e
+
+SCRIPT_DIR=$(cd "$(dirname "$0")" && pwd)
+
+# clone sv-tests repo if not done yet
+if [ ! -e sv-tests/.git ] ; then
+  git clone https://github.com/chipsalliance/sv-tests
+  (cd sv-tests && git checkout cbe02cf550b1345f5b75fee0c85145b1b68f379e)
+fi
+
+# install Python dependencies needed by the runner and report generator
+pip3 install psutil pygments jinja2 markupsafe
+
+# copy the ebmc runner
+cp "$SCRIPT_DIR/ebmc.py" sv-tests/tools/runners/
+
+cd sv-tests
+
+# run the sv-tests and generate the HTML report
+make report
+
+# print a summary of pass/fail results
+python3 - <<'EOF'
+import os, sys
+
+logs_dir = 'out/logs/ebmc'
+if not os.path.exists(logs_dir):
+    print("No test results found")
+    sys.exit(0)
+
+passed = []
+failed = []
+
+for dirpath, _, filenames in os.walk(logs_dir):
+    for fn in sorted(filenames):
+        path = os.path.join(dirpath, fn)
+        if not os.path.getsize(path):
+            continue  # skipped test
+
+        params = {}
+        with open(path) as f:
+            for line in f:
+                line = line.rstrip()
+                if not line:
+                    break
+                key, _, val = line.partition(': ')
+                params[key] = val
+
+        tool_success = params.get('tool_success') == '1'
+        should_fail = params.get('should_fail') == '1'
+        tool_crashed = int(params.get('rc', 0)) >= 126
+
+        test_passed = not tool_crashed and (should_fail != tool_success)
+
+        name = params.get('name', fn)
+        if test_passed:
+            passed.append(name)
+        else:
+            failed.append(name)
+
+for name in failed:
+    print(f'FAIL: {name}')
+
+total = len(passed) + len(failed)
+print(f'\nebmc: {len(passed)} passed, {len(failed)} failed out of {total} tests')
+EOF