Improvements to waveform analysis, EVAL-HD, riscv-formal, CI

.github/workflows/ci.yml

@@ -1,5 +1,5 @@
-name: Docker build test
-on: [push, pull_request]
+name: Full CI tests and Docker deployment
+on: [pull_request]
 
 jobs:
   build-docker:
@@ -93,9 +93,9 @@ jobs:
           run: |
             cd /ecosystem/benchmarks/spectreguard
             make && mv specBench.bin specBench-32.bin
-            make clean && make 64BIT=1 && mv specBench.bin specBench-64.bin
             ../../simulation/build/sim-32-i specBench-32.bin
             ../../simulation/build/sim-32-o specBench-32.bin
+            make clean && make 64BIT=1 && mv specBench.bin specBench-64.bin
             ../../simulation/build/sim-64-i specBench-64.bin
             ../../simulation/build/sim-64-o specBench-64.bin
 
@@ -117,19 +117,27 @@ jobs:
         with:
           image: ecosystem:latest
           run: |
-            cd /ecosystem
             . /ecosystem/waveform-analysis/.venv/bin/activate
             cd /ecosystem/noninterference-testing/
-            make -C programs vcd USECLANG=0 RISCV_PREFIX=riscv64-unknown-elf SIM_EXE=/ecosystem/simulation/build/sim-32-o
-            ./run-security-eval.py
+            make -C programs vcd SIM_EXE=/ecosystem/simulation/build/sim-32-o
+            waveform-security
 
       - name: Run EVAL-HD
         uses: addnab/docker-run-action@v3
         with:
           image: ecosystem:latest
           run: |
+            . /ecosystem/waveform-analysis/.venv/bin/activate
             cd /ecosystem/synthesis
-            ./run-yosys.sh
+            ./eval-hd.py ../core/Core.v --cell-library ../eval-hd/freepdk-45nm/stdcells.lib
+
+      - name: Run one riscv-formal test
+        uses: addnab/docker-run-action@v3
+        with:
+          image: ecosystem:latest
+          run: |
+            cd /ecosystem/formal-verification/riscv-formal
+            make formal-insn_bgeu
 
   push-image:
     name: Push Docker image

.github/workflows/reduced.yml

@@ -0,0 +1,83 @@
+name: Reduced CI tests
+on: [push, pull_request]
+
+jobs:
+  build-docker:
+    name: Build Docker image
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+    steps:
+      - name: Free Disk Space
+        uses: jlumbroso/free-disk-space@main
+        with:
+          tool-cache: false
+
+      - name: Check out repository
+        uses: actions/checkout@v2
+        with:
+          submodules: 'recursive'
+
+      - name: Set up Docker Buildx
+        uses: docker/setup-buildx-action@v2
+
+      - name: Build Docker image
+        uses: docker/build-push-action@v4
+        with:
+          context: .
+          file: "Dockerfile"
+          tags: ecosystem:latest
+          push: false
+          build-args: |
+            INSTALL_PROTEUS=true
+          outputs: type=docker,dest=/tmp/ecosystem-docker.tar
+
+      - name: Upload Docker artifact
+        uses: actions/upload-artifact@v4
+        with:
+          name: ecosystem-docker
+          path: /tmp/ecosystem-docker.tar
+
+  ci-tests:
+    runs-on: ubuntu-latest
+    needs: build-docker
+    steps:
+      - name: Free Disk Space
+        uses: jlumbroso/free-disk-space@main
+        with:
+          tool-cache: false
+          docker-images: false
+
+      - name: Check out repository
+        uses: actions/checkout@v2
+
+      - name: Download Docker artifact
+        uses: actions/download-artifact@v4
+        with:
+          name: ecosystem-docker
+          path: /tmp
+
+      - name: Load Docker image
+        run: docker load --input /tmp/ecosystem-docker.tar
+
+      - name: Run functional tests
+        uses: addnab/docker-run-action@v3
+        with:
+          image: ecosystem:latest
+          run: |
+            cd /ecosystem
+            cp simulation/build/sim-32-i simulation/build/sim && make clean -C functional-tests && make RISCV_PREFIX=riscv64-unknown-elf BUILD_CORE=0 -C functional-tests
+            cp simulation/build/sim-32-o simulation/build/sim && make clean -C functional-tests && make RISCV_PREFIX=riscv64-unknown-elf BUILD_CORE=0 -C functional-tests
+            cp simulation/build/sim-64-i simulation/build/sim && make clean -C functional-tests && make RISCV_PREFIX=riscv64-unknown-elf BUILD_CORE=0 64BIT=1 -C functional-tests
+            cp simulation/build/sim-64-o simulation/build/sim && make clean -C functional-tests && make RISCV_PREFIX=riscv64-unknown-elf BUILD_CORE=0 64BIT=1 -C functional-tests
+
+      - name: Run non-interference test
+        uses: addnab/docker-run-action@v3
+        with:
+          image: ecosystem:latest
+          run: |
+            cd /ecosystem
+            . /ecosystem/waveform-analysis/.venv/bin/activate
+            cd /ecosystem/noninterference-testing/
+            make -C programs vcd SIM_EXE=/ecosystem/simulation/build/sim-32-o
+            waveform-security

.gitmodules

@@ -1,6 +1,3 @@
-[submodule "formal-verification/riscv-formal/riscv-formal"]
-	path = formal-verification/riscv-formal/riscv-formal
-	url = https://github.com/YosysHQ/riscv-formal.git
 [submodule "functional-tests/riscv-tests"]
 	path = functional-tests/riscv-tests
 	url = https://github.com/riscv-software-src/riscv-tests.git

Dockerfile

@@ -3,12 +3,14 @@ FROM ubuntu:24.04
 # Set to noninteractive mode
 ARG DEBIAN_FRONTEND=noninteractive
 
-ARG INSTALL_TOOLCHAIN
-ARG INSTALL_EVAL_HD
-ARG INSTALL_PROTEUS
+ARG INSTALL_TOOLCHAIN=false
+ARG INSTALL_EVAL_HD=false
+ARG INSTALL_PROTEUS=false
+ARG INSTALL_RISCV_FORMAL=true
 RUN echo "Install RISC-V toolchain: ${INSTALL_TOOLCHAIN}"
 RUN echo "Install EVAL-HD: ${INSTALL_EVAL_HD}"
 RUN echo "Setup Proteus core: ${INSTALL_PROTEUS}"
+RUN echo "Install riscv-formal: ${INSTALL_RISCV_FORMAL}"
 
 ################################################################################
 # Basic dependencies
@@ -35,6 +37,7 @@ WORKDIR /ecosystem
 RUN if [ "${INSTALL_TOOLCHAIN}" = "true" ] ; then ./install-scripts/toolchain.sh ; else echo Skipping RISC-V toolchain... ; fi
 RUN if [ "${INSTALL_EVAL_HD}" = "true" ] ; then ./install-scripts/eval-hd.sh ; else echo Skipping EVAL-HD setup... ; fi
 RUN if [ "${INSTALL_PROTEUS}" = "true" ] ; then ./install-scripts/proteus.sh ; else echo Skipping Proteus core setup... ; fi
+RUN if [ "${INSTALL_RISCV_FORMAL}" = "true" ] ; then ./install-scripts/riscv-formal.sh ; else echo Skipping riscv-formal setup... ; fi
 
 # add RISC-V toolchain to path if it was installed (https://stackoverflow.com/a/51264575)
 ENV TOOLCHAIN_PATH=${INSTALL_TOOLCHAIN:+/opt/riscv/bin:}

README.md

@@ -27,28 +27,18 @@ Alternatively, you can build this image locally with the included [Dockerfile](.
 The container can be built with the following command:
 
 ```shell-session
-$ docker build -t ecosystem .
+$ docker compose up
 ```
 
-Additional build arguments can be added with the `--build-arg FLAG_NAME=true` argument, for example `INSTALL_TOOLCHAIN` to install the RISC-V GNU toolchain, `INSTALL_EVAL_HD` to install the hardware cost evaluation tool and `INSTALL_PROTEUS` to clone and install the Proteus core inside the container (instead of mounting it as a volume).
-Note that installing these extra tools will add a substantial amount of time to the build process (should quantify it later).
-
-```shell-session
-$ docker build -t ecosystem . --build-arg INSTALL_PROTEUS=true --build-arg INSTALL_EVAL_HD=true --build-arg INSTALL_TOOLCHAIN=true
-```
+Additional build arguments can be added in `docker-compose.yml`, for example `INSTALL_TOOLCHAIN` to install the RISC-V GNU toolchain, `INSTALL_EVAL_HD` to install the hardware cost evaluation tool and `INSTALL_PROTEUS` to clone and install the Proteus core inside the container (instead of mounting it as a volume).
+Note that installing these extra tools will add a substantial amount of time to the build process.
 
 ### Working with the container
 
 You can launch a container after building:
 
 ```shell-session
-$ docker run -it ecosystem
-```
-
-Optionally, you can attach the Proteus core directory as a volume, for example after cloning it to `core`:
-
-```shell-session
-$ docker run -v ./core:/ecosystem/core -it ecosystem
+$ docker compose run --remove-orphans ecosystem
 ```
 
 ### Non-container setup

benchmarks/spectreguard/specBench.c

@@ -265,7 +265,7 @@ int main(int argc, char **argv)
     time_work = 0;
     time_encrypt = 0;
 
-    for (k = 0; k < 100; k++)
+    for (k = 0; k < 10; k++)
     {
         printf("%d\n", k);
         time1 = rdcycle();

docker-compose.yml

@@ -0,0 +1,20 @@
+services:
+  ecosystem:
+    build:
+      context: .
+      args:
+        INSTALL_EVAL_HD: "true"
+        INSTALL_TOOLCHAIN: "true"
+    container_name: ecosystem
+    restart: "no"
+    stdin_open: true
+    tty: true
+    working_dir: /ecosystem
+    volumes:
+      - ./core:/ecosystem/core
+      - ./synthesis:/ecosystem/synthesis
+      - ./noninterference-testing:/ecosystem/noninterference-testing
+      - ./waveform-analysis:/ecosystem/waveform-analysis
+      - ./install-scripts:/ecosystem/install-scripts
+      - ./formal-verification:/ecosystem/formal-verification
+    command: "/bin/bash"

formal-verification/riscv-formal/Makefile

@@ -1,27 +1,19 @@
-BASE_DIR = $(shell pwd)
-RISCV_DIR = $(BASE_DIR)/..
-RISCV_FORMAL_DIR = $(BASE_DIR)/riscv-formal
-CORE_DIR = $(RISCV_FORMAL_DIR)/cores/riscv
+BASE_DIR = $(shell pwd)/../..
+TARGET_DIR = $(BASE_DIR)/riscv-formal/cores/proteus/
 CORE ?= riscv.CoreFormal
 
 all: formal
 
-$(RISCV_DIR)/Core.v: FORCE
-	cd $(RISCV_DIR); sbt "runMain $(CORE)"
+proteus.v:
+	cd $(BASE_DIR)/core && sbt "runMain $(CORE)" && cp Core.v $(BASE_DIR)/formal-verification/riscv-formal/proteus.v
 
-setup: $(RISCV_DIR)/Core.v
-	mkdir -p $(CORE_DIR)
-	cp $< $(CORE_DIR)/riscv.v
-	cp checks.cfg wrapper.sv disasm.py $(CORE_DIR)
-	cd $(CORE_DIR); python3 $(RISCV_FORMAL_DIR)/checks/genchecks.py
+setup: proteus.v
+	mkdir -p $(TARGET_DIR)
+	cp checks.cfg wrapper.sv proteus.v $(TARGET_DIR)
+	cd $(TARGET_DIR) && python3 ../../checks/genchecks.py
 
 formal: setup
-	$(MAKE) -C $(CORE_DIR)/checks
-	@echo "Failed tests:"
-	find $(CORE_DIR)/checks -name trace.vcd
+	make -C $(TARGET_DIR)/checks -j$(nproc)
 
 formal-%: setup
-	$(MAKE) -C $(CORE_DIR)/checks $(subst formal-,,$@)_ch0
-
-.PHONY: FORCE
-
+	$(MAKE) -C $(TARGET_DIR)/checks $(subst formal-,,$@)_ch0

formal-verification/riscv-formal/checks.cfg

@@ -1,4 +1,3 @@
-
 [options]
 isa rv32i
 
@@ -19,4 +18,3 @@ causal    10    30
 [script-sources]
 read_verilog -sv @basedir@/cores/@core@/wrapper.sv
 read_verilog @basedir@/cores/@core@/@core@.v
-

install-scripts/eval-hd.sh

@@ -2,9 +2,6 @@
 
 set -ex
 
-apt-get install -yqq build-essential clang lld bison flex libreadline-dev gawk tcl-dev libffi-dev git graphviz xdot pkg-config python3 libboost-system-dev libboost-python-dev libboost-filesystem-dev zlib1g-dev
 git clone --recurse-submodules --depth 1 --shallow-submodules https://github.com/KULeuven-COSIC/eval-hd.git
-cd eval-hd/yosys
-make config-gcc
-make -j$(nproc)
-make install
+. /ecosystem/waveform-analysis/.venv/bin/activate
+pip install pyosys

install-scripts/riscv-formal.sh

@@ -0,0 +1,32 @@
+#!/bin/bash
+
+set -ex
+
+git clone https://github.com/YosysHQ/riscv-formal.git
+
+git clone --recurse-submodules --depth 1 https://github.com/YosysHQ/yosys.git
+cd yosys
+apt-get install -yqq build-essential clang lld bison flex libreadline-dev gawk tcl-dev libffi-dev git graphviz xdot pkg-config python3 libboost-system-dev libboost-python-dev libboost-filesystem-dev zlib1g-dev
+make -j$(nproc)
+make install
+
+cd ..
+
+git clone https://github.com/YosysHQ/sby
+cd sby
+make install
+
+python3 -m pip install click --break-system-packages
+
+cd ..
+
+apt update && apt install -y cmake
+
+git clone https://github.com/boolector/boolector
+cd boolector
+./contrib/setup-btor2tools.sh
+./contrib/setup-lingeling.sh
+./configure.sh
+make -C build -j$(nproc)
+cp build/bin/{boolector,btor*} /usr/local/bin/
+cp deps/btor2tools/build/bin/btorsim /usr/local/bin/