From feb552d568d713c9689d799572e5ca2c4048a167 Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Fri, 28 Nov 2025 17:16:05 +0100
Subject: [PATCH 01/10] Separate binaries for correctness and noninterference
 testing, improved documentation

---
 .github/workflows/ci.yml                      |   4 +-
 noninterference-testing/README.md             |  80 +++++-------
 noninterference-testing/programs/Makefile     |   3 +-
 .../programs/Makefile.include                 |   6 +-
 .../run-correctness-eval.py                   |  68 ----------
 waveform-analysis/.gitignore                  |   1 +
 waveform-analysis/README.md                   |  14 +++
 waveform-analysis/pyproject.toml              |   2 +
 .../waveform_analysis/check_correctness.py    |  62 ++++++++++
 .../src/waveform_analysis/check_security.py   | 116 +++++++++++-------
 .../src/waveform_analysis/py.typed            |   0
 11 files changed, 186 insertions(+), 170 deletions(-)
 delete mode 100755 noninterference-testing/run-correctness-eval.py
 create mode 100644 waveform-analysis/.gitignore
 create mode 100755 waveform-analysis/src/waveform_analysis/check_correctness.py
 rename noninterference-testing/run-security-eval.py => waveform-analysis/src/waveform_analysis/check_security.py (60%)
 create mode 100644 waveform-analysis/src/waveform_analysis/py.typed

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 0770615..322e994 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -107,8 +107,8 @@ jobs:
             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
diff --git a/noninterference-testing/README.md b/noninterference-testing/README.md
index b9cd434..3e9801c 100644
--- a/noninterference-testing/README.md
+++ b/noninterference-testing/README.md
@@ -6,9 +6,37 @@ Specifically, it checks that observable microarchitectural components (e.g. exec
 
 We use noninterference testing to test security defenses implemented in Proteus. Concretely, we (1) generate sets of insecure programs that fail noninterference testing (2) secure these programs with hardware defenses and (3) make sure that secure versions pass noninterference testing.
 
-> [!WARNING]
-> The rest of this documentation is outdated and will be updated soon™.
-> Try `--help` on the script you are interested in running.
+For noninterference testing, we use the `waveform-security` binary, while for correctness testing we use `waveform-correctness`:
+
+```shell
+$ make -C programs all
+$ make -C programs vcd SIM_EXE=/ecosystem/simulation/build/sim
+
+$ waveform-correctness --p1 programs/vcd/pht-test1_FULLFENCE_LEAKBR_EXP1.vcd --p2 programs/vcd/pht-test1_NOFENCE_LEAKBR_EXP0.vcd --diff # correctness checking script
+----------------------------------------
+Mismatch at change #13
+Common value: ('TOP.Core.pipeline.retirementStage.arbitration_isDone', 1)
+Common value: ('TOP.Core.pipeline.retirementStage.in_PC', 2147483700)
+Common value: ('TOP.Core.pipeline.retirementStage.in_RD_DATA', 0)
+First value: ('TOP.Core.pipeline.retirementStage.in_RD', 16)
+Second value: ('TOP.Core.pipeline.retirementStage.in_RD', 12)
+Common value: ('TOP.Core.pipeline.retirementStage.in_RS1_DATA', 0)
+Common value: ('TOP.Core.pipeline.retirementStage.in_RS2_DATA', 0)
+First value: ('TOP.Core.pipeline.retirementStage.in_LSU_TARGET_ADDRESS', 2147483716)
+Second value: ('TOP.Core.pipeline.retirementStage.in_LSU_TARGET_ADDRESS', 2147483712)
+
+$ waveform-security --leakage-sinks LEAKLOAD LEAKBR LEAKJMP  # noninterference security evaluation
+DEBUG: + Check all input for ./programs/vcd/ssb-test1_NOFENCE_LEAKBR with base=EXP1
+ INFO:  !--- Programs ./programs/vcd/ssb-test1_NOFENCE_LEAKBR is insecure :) ---!
+DEBUG: + Check all input for ./programs/vcd/ssb-test1_FULLFENCE_LEAKBR with base=EXP1
+ INFO:  !--- Programs ./programs/vcd/ssb-test1_FULLFENCE_LEAKBR is secure :) ---!
+DEBUG: + Check all input for ./programs/vcd/ssb-test1_NOFENCE_LEAKJMP with base=EXP1
+ INFO:  !--- Programs ./programs/vcd/ssb-test1_NOFENCE_LEAKJMP is insecure :) ---!
+DEBUG: + Check all input for ./programs/vcd/ssb-test1_FULLFENCE_LEAKJMP with base=EXP1
+ INFO:  !--- Programs ./programs/vcd/ssb-test1_FULLFENCE_LEAKJMP is secure :) ---!
+
+ RESULT:  Secure programs: 12/12 Insecure programs: 6/12
+```
 
 ## Overview
 
@@ -25,50 +53,6 @@ Finally, each program is compiled with two secret values that should trigger dis
 
 ### Security evaluation
 
+Compiled programs are in [./programs/build/](./programs/build/).
 The security evaluation runs pairs of programs with different secrets and monitors a set of selected signals.
-The set of selected signals (conservative or liberal) are defined in [signals.py](./vcd_scripts/signals.py).
-
-Given two sets of signals, the [Comparator](./vcd_scripts/comparator.py) class reports any mismatch between the signal sets.
 If the set of selected signals match, then the program is secure; otherwise, there is a side-channel violation.
-
-TODO: the same principle can be applied for correctness evaluation (see [run-correctness-eval.py](./run-correctness-eval.py)) but, for now, this script is buggy.
-
-## Run security evaluation
-
-### Compile programs
-
-The first step is to compile the programs. Make sure the toolchain path is correct; the default is [../llvm-project](../llvm-project).
-
-```
-make -C programs all
-```
-
-Compiled programs are in [./programs/build/](./programs/build/).
-
-Optionally, you can create objdump files to look at the assembly code:
-
-```
-make -C programs objdump
-```
-
-### Run simulations
-
-The second step is to run the simulator to get the vcd files of these programs. Make sure the path of Proteus is correct; the default is [../proteus](../proteus). Additionally, make sure Proteus is compiled with the DynamicCore (`make -C sim CORE=riscv.CoreDynamicExtMem32`).
-
-```
-make -C programs vcd USECLANG=0 RISCV_PREFIX=riscv64-unknown-elf SIM_EXE=/ecosystem/simulation/build/sim
-```
-
-Resulting vcd files are in [./programs/vcd/](./programs/vcd/).
-
-### Run security evaluation
-
-The final step is to run the security evaluation:
-```
-python ./run-security-evaluation.sh
-```
-
-The script can take arguments. For instance to chose the conservative security comparator, use `python ./run-security-evaluation.sh --compare-signals conservative`.
-See help with `python ./run-security-evaluation.sh --help`.
-
-If you need to debug a particular program, run `python ./run-security-eval.py --debug <program>` to get a verbose output of the comparator. For instance `python ./run-security-eval.py --debug pht-test1_FULLFENCE_LEAKLOAD`.
diff --git a/noninterference-testing/programs/Makefile b/noninterference-testing/programs/Makefile
index 0a36b1e..9cf6a78 100644
--- a/noninterference-testing/programs/Makefile
+++ b/noninterference-testing/programs/Makefile
@@ -24,9 +24,8 @@ all: elf bin
 
 dirs:
 	@mkdir -p $(BUILD_DIR)
-	@mkdir -p $(SIM_DIR)
 
 elf: dirs $(ELF_TARGETS)
 bin: dirs $(BIN_TARGETS)
 vcd: dirs $(VCD_TARGETS)
-objdump: dirs $(OBJDUMP_TARGETS)
\ No newline at end of file
+objdump: dirs $(OBJDUMP_TARGETS)
diff --git a/noninterference-testing/programs/Makefile.include b/noninterference-testing/programs/Makefile.include
index f1a4ce7..61058cf 100644
--- a/noninterference-testing/programs/Makefile.include
+++ b/noninterference-testing/programs/Makefile.include
@@ -1,11 +1,9 @@
 EVAL_DIR = $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
 BASE_DIR = $(abspath $(EVAL_DIR)/../..)
-SIM_DIR = $(BASE_DIR)/proteus/sim
-SIM_EXE ?= $(SIM_DIR)/build/sim
+SIM_EXE ?= $(BASE_DIR)/simulation/build/sim-32-o
 GTKW_DIR = $(EVAL_DIR)gtkw
 CORE ?= riscv.CoreExtMem32
-BUILD_CORE ?= 1
-USECLANG ?= 1
+USECLANG ?= 0
 EXPERIMENT ?= LEGACY
 BOOT ?= 0
 BUILD_DIR ?= ./
diff --git a/noninterference-testing/run-correctness-eval.py b/noninterference-testing/run-correctness-eval.py
deleted file mode 100755
index 774e1bb..0000000
--- a/noninterference-testing/run-correctness-eval.py
+++ /dev/null
@@ -1,68 +0,0 @@
-#!/usr/bin/env python3
-
-import argparse
-import sys
-
-
-from waveform_analysis.logger import log
-from waveform_analysis.signal_extractor import CPUWaveform
-from waveform_analysis.interface_parser import proteus_o_parser
-
-
-def check_divergences(p1: str, p2: str, timing: bool, diff: bool, full_diff: bool) -> bool:
-    base_waveform: CPUWaveform = CPUWaveform(p1, proteus_o_parser)
-    return base_waveform.compare_signals(CPUWaveform(p2, proteus_o_parser), proteus_o_parser.get_instruction_stream_list(), timing_sensitive=timing, display_diff=diff, early_out=(not full_diff))
-
-
-def parse_arguments():
-    parser = argparse.ArgumentParser(
-        description="Run security evaluation on benchmarks.")
-    parser.add_argument("--program_path", type=str, default="./programs",
-                        help="Path to the program directory (default: ./programs)")
-    parser.add_argument(
-        "--p1",
-        type=str,
-        help="Name of the benchmark to run (e.g., pht-test1_FULLFENCE_LEAKLOAD_EXP0)."
-    )
-    parser.add_argument(
-        "--p2",
-        type=str,
-        help="Name of the benchmark to run (e.g., pht-test1_NOFENCE_LEAKLOAD_EXP0)."
-    )
-    parser.add_argument(
-        "--diff",
-        action="store_true",
-        help="Display difference in signals"
-    )
-    parser.add_argument(
-        "--timing",
-        action="store_true",
-        help="Report differences in timing"
-    )
-    parser.add_argument(
-        "--full_diff",
-        action="store_true",
-        help="Report all differences, not just the first one"
-    )
-    args = parser.parse_args()
-    return args
-
-
-def main():
-    args = parse_arguments()
-    p1 = args.p1
-    p2 = args.p2
-    diff = args.diff
-    timing = args.timing
-    full = args.full_diff
-
-    if not p1 or not p2:
-        print("Error: Both --p1 and --p2 arguments are required.")
-        sys.exit(1)
-
-    print(f"Running correctness evaluation for {p1} and {p2}")
-    print(check_divergences(p1, p2, timing, diff, full))
-
-
-if __name__ == "__main__":
-    main()
diff --git a/waveform-analysis/.gitignore b/waveform-analysis/.gitignore
new file mode 100644
index 0000000..1d17dae
--- /dev/null
+++ b/waveform-analysis/.gitignore
@@ -0,0 +1 @@
+.venv
diff --git a/waveform-analysis/README.md b/waveform-analysis/README.md
index 84c747c..ebaaf36 100644
--- a/waveform-analysis/README.md
+++ b/waveform-analysis/README.md
@@ -1,3 +1,17 @@
+# Waveform analysis
+
+## Binary tools
+
+After installation, the library exports the following binaries that can be used (after activating the virtual environment):
+
+- `strip-vcd`: reduce VCD files to the list of signals that we are interested in (to speed up later processing or to be able to store it)
+- `waveform-correctness`: check the equivalence of architectural signals between two waveforms
+- `waveform-security`: checks whether certain benchmarks, when compiled with and without different countermeasures exhibit the expected leakage
+
+For more details, consult the `--help` option on these binaries.
+
+## Internal detail notes
+
 Waveform analysis is a fundamental basis of a lot of the analysis we perform in the ecosystem.
 
 - cpu interfaces describe which signals should be interpreted
diff --git a/waveform-analysis/pyproject.toml b/waveform-analysis/pyproject.toml
index c25e222..49c4e69 100644
--- a/waveform-analysis/pyproject.toml
+++ b/waveform-analysis/pyproject.toml
@@ -12,3 +12,5 @@ build-backend = "uv_build"
 
 [project.scripts]
 strip-vcd = "waveform_analysis.strip:main"
+waveform-correctness = "waveform_analysis.check_correctness:main"
+waveform-security = "waveform_analysis.check_security:main"
diff --git a/waveform-analysis/src/waveform_analysis/check_correctness.py b/waveform-analysis/src/waveform_analysis/check_correctness.py
new file mode 100755
index 0000000..a7c9d64
--- /dev/null
+++ b/waveform-analysis/src/waveform_analysis/check_correctness.py
@@ -0,0 +1,62 @@
+#!/usr/bin/env python3
+
+import argparse
+
+
+from .signal_extractor import CPUWaveform
+from .interface_parser import proteus_o_parser
+
+
+def parse_arguments():
+    parser = argparse.ArgumentParser(
+        description="Run correctness evaluation on two waveforms.")
+    parser.add_argument(
+        "--p1",
+        type=str,
+        required=True,
+        help="Path of the first waveform file."
+    )
+    parser.add_argument(
+        "--p2",
+        type=str,
+        required=True,
+        help="Path of the second waveform file."
+    )
+    parser.add_argument(
+        "--diff",
+        action="store_true",
+        help="Display diverging signals (default behavior is to only report True/False)"
+    )
+    parser.add_argument(
+        "--timing",
+        action="store_true",
+        help="Report differences in timing"
+    )
+    parser.add_argument(
+        "--full_diff",
+        action="store_true",
+        help="Report all differences, not just the first one"
+    )
+    args = parser.parse_args()
+    return args
+
+
+def main():
+    args = parse_arguments()
+    p1 = args.p1
+    p2 = args.p2
+    diff = args.diff
+    timing = args.timing
+    full = args.full_diff
+
+    base_waveform = CPUWaveform(p1, proteus_o_parser)
+    identical = base_waveform.compare_signals(
+        CPUWaveform(p2, proteus_o_parser),
+        proteus_o_parser.get_instruction_stream_list(),
+        timing_sensitive=timing,
+        display_diff=diff,
+        early_out=(not full))
+    if identical:
+        print("Signals match!")
+    elif not diff:
+        print("Signals do not match!")
diff --git a/noninterference-testing/run-security-eval.py b/waveform-analysis/src/waveform_analysis/check_security.py
similarity index 60%
rename from noninterference-testing/run-security-eval.py
rename to waveform-analysis/src/waveform_analysis/check_security.py
index 43ea1d6..10cd549 100755
--- a/noninterference-testing/run-security-eval.py
+++ b/waveform-analysis/src/waveform_analysis/check_security.py
@@ -20,30 +20,28 @@ def signals_based_on_policy(waveform: CPUWaveform, policy: str) -> list[str]:
         raise NotImplementedError()
 
 
-def check_all_inputs(policy: str, filename: str, exp_numbers: list[str], display_diff: bool = False) -> int:
+def secure_for_all_inputs(policy: str, filename: str, exp_postfixes: list[str], display_diff: bool = False) -> bool:
     global policy_signals
 
-    base = exp_numbers[0]
+    base = exp_postfixes[0]
     log.debug(f"+ Check all input for {filename} with base={base}")
     base_waveform = CPUWaveform(f"{filename}_{base}.vcd", proteus_o_parser)
     if policy_signals is None:
         policy_signals = signals_based_on_policy(base_waveform, policy)
-    for input_case in exp_numbers[1:]:
+    for input_case in exp_postfixes[1:]:
         if not base_waveform.compare_signals(CPUWaveform(f"{filename}_{input_case}.vcd", proteus_o_parser), policy_signals, display_diff=display_diff):
-            log.debug(f"!--- Programs {filename} is insecure ---!")
-            return 1
-    log.debug(f"!--- Program {filename} is secure ---!")
-    return 0
+            return False
+    return True
 
 
 def check_all_combinations(
-    # comparator: Comparator,
+    path: str,
     policy: str,
     benches: list[str],
     secure_defenses: list[str],
     insecure_defenses: list[str],
     leakage_sinks: list[str],
-    exp_numbers: list[str]
+    exp_postfixes: list[str]
 ) -> None:
     secure_programs_total = 0
     secure_programs_found_secure = 0
@@ -51,14 +49,14 @@ def check_all_combinations(
     insecure_programs_found_insecure = 0
 
     for bench in benches:
-        base_file = f"{benchmark_path}/vcd/{bench}"
+        base_file = f"{path}/vcd/{bench}"
         print(f"====== Running experiment for {base_file}")
 
         for leak_sink in leakage_sinks:
             for fence in insecure_defenses:
                 file = f"{base_file}_{fence}_{leak_sink}"
                 insecure_programs_total += 1
-                if check_all_inputs(policy, file, exp_numbers) == 0:
+                if secure_for_all_inputs(policy, file, exp_postfixes):
                     log.warning(
                         f"!--- Programs {file} should be insecure :( ---!")
                 else:
@@ -68,7 +66,7 @@ def check_all_combinations(
             for fence in secure_defenses:
                 file = f"{base_file}_{fence}_{leak_sink}"
                 secure_programs_total += 1
-                if check_all_inputs(policy, file, exp_numbers) == 1:
+                if not secure_for_all_inputs(policy, file, exp_postfixes):
                     log.error(f"!--- Programs {file} should be secure :( ---!")
                 else:
                     log.info(f"!--- Programs {file} is secure :) ---!")
@@ -79,31 +77,68 @@ def check_all_combinations(
         f"Secure programs: {secure_programs_found_secure}/{secure_programs_total} Insecure programs: {insecure_programs_found_insecure}/{insecure_programs_total}")
 
 
-def debug(policy: str, target: str) -> None:
-    check_all_inputs(
-        policy, f"{benchmark_path}/vcd/{target}", ["EXP0", "EXP1"], display_diff=True)
+def debug(path: str, policy: str, target: str) -> None:
+    secure_for_all_inputs(
+        policy, f"{path}/vcd/{target}", ["EXP0", "EXP1"], display_diff=True)
 
 
-def parse_arguments(benchmarks: list[str]) -> argparse.Namespace:
+def parse_arguments() -> argparse.Namespace:
+    benchmarks = ['pht-test1', 'pht-test2', 'psf-test1', 'ssb-test1']
+    secure_defenses = ["FULLFENCE"]
+    insecure_defenses = ["NOFENCE"]
+    leakage_sinks = ["LEAKLOAD", "LEAKSTORE", "LEAKBR", "LEAKJMP", "LEAKDIV"]
+    exp_postfixes = ["EXP1", "EXP0"]
+
     parser = argparse.ArgumentParser(
         description="Run security evaluation on benchmarks.")
     parser.add_argument("--program_path", type=str, default="./programs",
                         help="Path to the program directory (default: ./programs)")
     parser.add_argument(
-        "--program_name",
+        "--benchmarks",
         type=str,
-        choices=benchmarks + ["all"],
-        default="all",
-        help="Name of the benchmark to run (default: all). Options: " +
-        ", ".join(benchmarks + ["all"])
+        nargs='*',
+        choices=benchmarks,
+        default=benchmarks,
+        help="Name of the benchmark to run (leave out to include all)."
     )
-    # Choose security comparator
     parser.add_argument(
         "--compare-signals",
         choices=["conservative", "liberal"],
         default="liberal",
         help="Choose which signals to compare: conservative (all signals except selected non-observable signals) or liberal (only selected observable signals) (default: liberal)"
     )
+    parser.add_argument(
+        "--secure-defenses",
+        type=str,
+        nargs='*',
+        choices=secure_defenses,
+        default=secure_defenses,
+        help="Secure defense configurations (leave out to include all)."
+    )
+    parser.add_argument(
+        "--insecure-defenses",
+        type=str,
+        nargs='*',
+        choices=insecure_defenses,
+        default=insecure_defenses,
+        help="Insecure defense configurations (leave out to include all)."
+    )
+    parser.add_argument(
+        "--leakage-sinks",
+        type=str,
+        nargs='*',
+        choices=leakage_sinks,
+        default=leakage_sinks,
+        help="Leakage sink configurations (leave out to include all)."
+    )
+    parser.add_argument(
+        "--experiment-postfixes",
+        type=str,
+        nargs='*',
+        choices=exp_postfixes,
+        default=exp_postfixes,
+        help="Experiment postfix identifiers (leave out to include all)."
+    )
     parser.add_argument(
         "--debug",
         type=str,
@@ -115,31 +150,20 @@ def parse_arguments(benchmarks: list[str]) -> argparse.Namespace:
 
 
 def main() -> None:
-    all_bench = ['pht-test1', 'pht-test2', 'psf-test1', 'ssb-test1']
-    args = parse_arguments(all_bench)
-
-    global benchmark_path
-    benchmark_path = args.program_path
-    benchmark = args.program_name
+    args = parse_arguments()
 
     if args.debug:
-        debug(args.compare_signals, args.debug)
+        debug(
+            path=args.program_path,
+            policy=args.compare_signals,
+            target=args.debug)
         return
 
-    # Experiment configuration
-    secure_defenses = ["FULLFENCE"]
-    insecure_defenses = ["NOFENCE"]
-    leakage_sinks = ["LEAKLOAD", "LEAKSTORE", "LEAKBR", "LEAKJMP", "LEAKDIV"]
-    exp_numbers = ["EXP1", "EXP0"]
-
-    if benchmark == "all":
-        benchs = all_bench
-    else:
-        benchs = [benchmark]
-
-    check_all_combinations(args.compare_signals, benchs, secure_defenses,
-                           insecure_defenses, leakage_sinks, exp_numbers)
-
-
-if __name__ == "__main__":
-    main()
+    check_all_combinations(
+        path=args.program_path,
+        policy=args.compare_signals,
+        benches=args.benchmarks,
+        secure_defenses=args.secure_defenses,
+        insecure_defenses=args.insecure_defenses,
+        leakage_sinks=args.leakage_sinks,
+        exp_postfixes=args.experiment_postfixes)
diff --git a/waveform-analysis/src/waveform_analysis/py.typed b/waveform-analysis/src/waveform_analysis/py.typed
new file mode 100644
index 0000000..e69de29

From eb7cce6d5eb51d4c484af7c4311780fec31c8a0e Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Mon, 1 Dec 2025 00:32:15 +0100
Subject: [PATCH 02/10] Docker compose setup

---
 Dockerfile         |  6 +++---
 README.md          | 18 ++++--------------
 docker-compose.yml | 18 ++++++++++++++++++
 3 files changed, 25 insertions(+), 17 deletions(-)
 create mode 100644 docker-compose.yml

diff --git a/Dockerfile b/Dockerfile
index bd7ecea..5855259 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -3,9 +3,9 @@ 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
 RUN echo "Install RISC-V toolchain: ${INSTALL_TOOLCHAIN}"
 RUN echo "Install EVAL-HD: ${INSTALL_EVAL_HD}"
 RUN echo "Setup Proteus core: ${INSTALL_PROTEUS}"
diff --git a/README.md b/README.md
index 1ea75e0..0cc2a06 100644
--- a/README.md
+++ b/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
diff --git a/docker-compose.yml b/docker-compose.yml
new file mode 100644
index 0000000..0133767
--- /dev/null
+++ b/docker-compose.yml
@@ -0,0 +1,18 @@
+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
+    command: "/bin/bash"

From 504886c4cc60d22f9faa50dd44aa195bc2896181 Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Mon, 1 Dec 2025 00:34:44 +0100
Subject: [PATCH 03/10] Python-based EVAL-HD workflow with critical path
 calculation

---
 synthesis/eval-hd-area.ys   | 26 -----------------
 synthesis/eval-hd-timing.ys | 29 -------------------
 synthesis/eval-hd.py        | 56 +++++++++++++++++++++++++++++++++++++
 synthesis/run-yosys.sh      |  1 -
 synthesis/top.py            | 32 +++++++++++++++++++++
 5 files changed, 88 insertions(+), 56 deletions(-)
 delete mode 100644 synthesis/eval-hd-area.ys
 delete mode 100644 synthesis/eval-hd-timing.ys
 create mode 100755 synthesis/eval-hd.py
 delete mode 100755 synthesis/run-yosys.sh
 create mode 100755 synthesis/top.py

diff --git a/synthesis/eval-hd-area.ys b/synthesis/eval-hd-area.ys
deleted file mode 100644
index abd2365..0000000
--- a/synthesis/eval-hd-area.ys
+++ /dev/null
@@ -1,26 +0,0 @@
-# read design
-read_verilog ../core/Core.v
-
-# elaborate design hierarchy
-hierarchy -check -top Core
-
-# the high-level stuff
-proc; opt; fsm; opt; memory; opt
-
-# mapping to internal cell library
-techmap; opt
-
-# mapping flip-flops to cell library
-dfflibmap -liberty ../eval-hd/freepdk-45nm/stdcells.lib
-
-# mapping logic to cell library
-abc -liberty ../eval-hd/freepdk-45nm/stdcells.lib
-
-# cleanup
-clean
-
-# write synthesized design
-write_verilog ../synthesis/result.v
-
-# get ASIC gate count and area numbers
-stat -liberty ../eval-hd/freepdk-45nm/stdcells.lib
diff --git a/synthesis/eval-hd-timing.ys b/synthesis/eval-hd-timing.ys
deleted file mode 100644
index 808ff1d..0000000
--- a/synthesis/eval-hd-timing.ys
+++ /dev/null
@@ -1,29 +0,0 @@
-# read design
-read_verilog ../core/Core.v
-
-# elaborate design hierarchy
-hierarchy -check -top Core
-
-# flatten the design
-flatten
-
-# the high-level stuff
-proc; opt; fsm; opt; memory; opt
-
-# mapping to internal cell library
-techmap; opt
-
-# mapping flip-flops to cell library
-dfflibmap -liberty ../eval-hd/freepdk-45nm/stdcells.lib
-
-# mapping logic to cell library with timing constraint
-abc -liberty ../eval-hd/freepdk-45nm/stdcells.lib -fast -D 2625
-
-# cleanup
-clean
-
-# write synthesized design
-write_verilog ../synthesis/result.v
-
-# get ASIC gate count and area numbers
-stat -liberty ../eval-hd/freepdk-45nm/stdcells.lib
diff --git a/synthesis/eval-hd.py b/synthesis/eval-hd.py
new file mode 100755
index 0000000..2b14d8b
--- /dev/null
+++ b/synthesis/eval-hd.py
@@ -0,0 +1,56 @@
+#!/usr/bin/env python3
+
+from pyosys import libyosys as ys
+import argparse
+
+def run_analysis(report_timing: bool, design_file: str, top_module: str, timing_target: int, cell_library: str) -> None:
+    design = ys.Design()
+
+    # read design
+    ys.run_pass(f"read_verilog {design_file}", design)
+
+    # elaborate design hierarchy
+    ys.run_pass(f"hierarchy -check -top {top_module}", design)
+
+    if report_timing:
+        # flatten the design
+        ys.run_pass("flatten", design)
+
+    # the high-level stuff
+    ys.run_pass("proc; opt; fsm; opt; memory; opt", design)
+
+    # mapping to internal cell library
+    ys.run_pass("techmap; opt", design)
+
+    # mapping flip-flops to cell library
+    ys.run_pass(f"dfflibmap -liberty {cell_library}", design)
+
+    if report_timing:
+        # mapping logic to cell library with timing constraint
+        ys.run_pass(f"abc -liberty {cell_library} -fast -D {timing_target}", design)
+    else:
+        # mapping logic to cell library
+        ys.run_pass(f"abc -liberty {cell_library}", design)
+
+    # cleanup
+    ys.run_pass("clean", design)
+
+    # write synthesized design
+    ys.run_pass("write_verilog result.v", design)
+
+    # get ASIC gate count and area numbers
+    ys.run_pass(f"stat -liberty {cell_library}", design)
+
+def main() -> None:
+    parser = argparse.ArgumentParser(description="Synthesize a design for ASIC using Yosys.")
+    parser.add_argument("design_file", type=str, help="Path to the Verilog design file.")
+    parser.add_argument("--top_module", type=str, default="Core", help="Name of the top module (default: Core).")
+    parser.add_argument("--cell-library", default="freepdk-45nm/stdcells.lib", help="Path to the cell library (default: FreePDK).")
+    parser.add_argument("--report-timing", action="store_true", help="Enable timing analysis during synthesis.")
+    parser.add_argument("--timing-target", type=int, default=2500, help="Target timing constraint (in picoseconds, default: 2500).")
+    args = parser.parse_args()
+
+    run_analysis(args.report_timing, args.design_file, args.top_module, args.timing_target, args.cell_library)
+
+if __name__ == "__main__":
+    main()
diff --git a/synthesis/run-yosys.sh b/synthesis/run-yosys.sh
deleted file mode 100755
index b5d281d..0000000
--- a/synthesis/run-yosys.sh
+++ /dev/null
@@ -1 +0,0 @@
-../eval-hd/yosys/yosys eval-hd-area.ys
diff --git a/synthesis/top.py b/synthesis/top.py
new file mode 100755
index 0000000..65f5869
--- /dev/null
+++ b/synthesis/top.py
@@ -0,0 +1,32 @@
+#!/usr/bin/env python3
+
+import subprocess
+import re
+
+def run_with_timing(target: int) -> bool:
+    timing_failed = False
+
+    result = subprocess.run(["./eval-hd.py", "../core/Core.v", "--report-timing", "--timing-target", str(target), "--cell-library", "../eval-hd/freepdk-45nm/stdcells.lib"], capture_output=True, text=True)
+    rs = re.search(r"Chip area for module \'\\Core\': (\d+.\d+)", result.stdout)
+    if rs:
+        area = float(rs.group(1))
+        print(f"Area = {area:.2f} µm² = {(area / 1000000):.4f} mm²")
+
+    trs = re.search(r"Cannot meet the target required times \((\d+.\d+)\). Continue anyway.", result.stdout)
+    if trs:
+        timing = float(trs.group(1))
+        print("Timing failed")
+        timing_failed = True
+    else:
+        print(f"Timing met: {target} ps = {target / 1000} ns = {1 / (target / 1000000):.2f} MHz")
+
+    return timing_failed
+
+successful_target = 10000
+
+for step in [1000, 100, 10, 1]:
+    for target in range(successful_target - 9 * step, successful_target, step):
+        failed = run_with_timing(target)
+        if not failed:
+            successful_target = target
+            break

From 342596f70c50959de619c29932bb5ab1fa15b540 Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Mon, 1 Dec 2025 17:01:49 +0100
Subject: [PATCH 04/10] Initial steps to get riscv-formal up and running

---
 .gitmodules                                   |  3 --
 Dockerfile                                    |  3 ++
 docker-compose.yml                            |  2 ++
 formal-verification/riscv-formal/Makefile     | 28 +++++++------------
 formal-verification/riscv-formal/checks.cfg   |  2 --
 formal-verification/riscv-formal/riscv-formal |  1 -
 install-scripts/riscv-formal.sh               | 23 +++++++++++++++
 7 files changed, 38 insertions(+), 24 deletions(-)
 delete mode 160000 formal-verification/riscv-formal/riscv-formal
 create mode 100755 install-scripts/riscv-formal.sh

diff --git a/.gitmodules b/.gitmodules
index a603dd7..89c54bc 100644
--- a/.gitmodules
+++ b/.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
diff --git a/Dockerfile b/Dockerfile
index 5855259..ac17de4 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -6,9 +6,11 @@ ARG DEBIAN_FRONTEND=noninteractive
 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:}
diff --git a/docker-compose.yml b/docker-compose.yml
index 0133767..47d531e 100644
--- a/docker-compose.yml
+++ b/docker-compose.yml
@@ -15,4 +15,6 @@ services:
       - ./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"
diff --git a/formal-verification/riscv-formal/Makefile b/formal-verification/riscv-formal/Makefile
index ed378b7..7577731 100644
--- a/formal-verification/riscv-formal/Makefile
+++ b/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)"
+Core.v: 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: Core.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
diff --git a/formal-verification/riscv-formal/checks.cfg b/formal-verification/riscv-formal/checks.cfg
index 74c6db1..91e445d 100644
--- a/formal-verification/riscv-formal/checks.cfg
+++ b/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
-
diff --git a/formal-verification/riscv-formal/riscv-formal b/formal-verification/riscv-formal/riscv-formal
deleted file mode 160000
index 64931a6..0000000
--- a/formal-verification/riscv-formal/riscv-formal
+++ /dev/null
@@ -1 +0,0 @@
-Subproject commit 64931a6094f02fc0946282b4cb79ec18d4e7f2d4
diff --git a/install-scripts/riscv-formal.sh b/install-scripts/riscv-formal.sh
new file mode 100755
index 0000000..ab8a18a
--- /dev/null
+++ b/install-scripts/riscv-formal.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+
+set -ex
+
+git clone https://github.com/YosysHQ/riscv-formal.git
+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/

From 63f0a0e2cecc1b1d1d68395f25b3b62624c589d1 Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Tue, 2 Dec 2025 11:50:11 +0100
Subject: [PATCH 05/10] Run full CI tests only on PRs

---
 .github/workflows/ci.yml      |  4 +-
 .github/workflows/reduced.yml | 83 +++++++++++++++++++++++++++++++++++
 2 files changed, 85 insertions(+), 2 deletions(-)
 create mode 100644 .github/workflows/reduced.yml

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 951a3a6..d26134f 100644
--- a/.github/workflows/ci.yml
+++ b/.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:
diff --git a/.github/workflows/reduced.yml b/.github/workflows/reduced.yml
new file mode 100644
index 0000000..191e4b4
--- /dev/null
+++ b/.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

From 417c892a9dfb0d7865b616c34e3485e5764b4fee Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Tue, 2 Dec 2025 21:50:19 +0100
Subject: [PATCH 06/10] Add one riscv-formal test case

---
 .github/workflows/ci.yml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index d26134f..230ff9c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -131,6 +131,14 @@ jobs:
             cd /ecosystem/synthesis
             ./run-yosys.sh
 
+      - 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
     runs-on: ubuntu-latest

From 8ec9a1d220a63923b0d15d260fa9a588e1caa733 Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Thu, 4 Dec 2025 15:46:51 +0100
Subject: [PATCH 07/10] Fix EVAL-HD CI

---
 .github/workflows/ci.yml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 230ff9c..877f208 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -117,7 +117,6 @@ jobs:
         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
@@ -128,8 +127,9 @@ jobs:
         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

From 7002897d43c35c6717f0a029e899ab81e5d1b24f Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Thu, 4 Dec 2025 23:42:27 +0100
Subject: [PATCH 08/10] Reduce SpectreGuard iterations and fix errors

---
 .github/workflows/ci.yml            | 2 +-
 benchmarks/spectreguard/specBench.c | 2 +-
 install-scripts/eval-hd.sh          | 7 ++-----
 install-scripts/riscv-formal.sh     | 8 ++++++++
 4 files changed, 12 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 877f208..85dbf77 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -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
 
diff --git a/benchmarks/spectreguard/specBench.c b/benchmarks/spectreguard/specBench.c
index d60828e..12e17cb 100644
--- a/benchmarks/spectreguard/specBench.c
+++ b/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();
diff --git a/install-scripts/eval-hd.sh b/install-scripts/eval-hd.sh
index 2d2b92c..37465e5 100755
--- a/install-scripts/eval-hd.sh
+++ b/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
diff --git a/install-scripts/riscv-formal.sh b/install-scripts/riscv-formal.sh
index ab8a18a..fb8abc2 100755
--- a/install-scripts/riscv-formal.sh
+++ b/install-scripts/riscv-formal.sh
@@ -3,6 +3,14 @@
 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
+make -j$(nproc)
+make install
+
+cd ..
+
 git clone https://github.com/YosysHQ/sby
 cd sby
 make install

From 4ac31787b1c30b5642eec1351509652e5ab6ea8b Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Fri, 5 Dec 2025 00:16:58 +0100
Subject: [PATCH 09/10] Fix yosys dependencies

---
 install-scripts/riscv-formal.sh | 1 +
 1 file changed, 1 insertion(+)

diff --git a/install-scripts/riscv-formal.sh b/install-scripts/riscv-formal.sh
index fb8abc2..a5e9b75 100755
--- a/install-scripts/riscv-formal.sh
+++ b/install-scripts/riscv-formal.sh
@@ -6,6 +6,7 @@ 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
 

From e07b6bb12449f45a226e3d03afbbab210d217b10 Mon Sep 17 00:00:00 2001
From: marton bognar <marton.bognar@kuleuven.be>
Date: Fri, 5 Dec 2025 10:15:52 +0100
Subject: [PATCH 10/10] Fix riscv-formal Makefile

---
 formal-verification/riscv-formal/Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/formal-verification/riscv-formal/Makefile b/formal-verification/riscv-formal/Makefile
index 7577731..e83fe02 100644
--- a/formal-verification/riscv-formal/Makefile
+++ b/formal-verification/riscv-formal/Makefile
@@ -4,10 +4,10 @@ CORE ?= riscv.CoreFormal
 
 all: formal
 
-Core.v: proteus.v
+proteus.v:
 	cd $(BASE_DIR)/core && sbt "runMain $(CORE)" && cp Core.v $(BASE_DIR)/formal-verification/riscv-formal/proteus.v
 
-setup: Core.v
+setup: proteus.v
 	mkdir -p $(TARGET_DIR)
 	cp checks.cfg wrapper.sv proteus.v $(TARGET_DIR)
 	cd $(TARGET_DIR) && python3 ../../checks/genchecks.py