Ci formalverif (#5)

* Move formal verif to cocotb flow with verilator + add formal verif for AES-128 ENC to top-level Makefile

* Add top-level formal verification for AES-128/192/256 ENC/DEC + optimize formal verif. flow for verilator compilation

* Add formal test in continuous integration

* Add formal test in continuous integration

* Add dependencies in formal-tests target in top level Makefile

* add iverilog in dependencies for formal-tests CI

* add +x permission to matchi in formal-tests CI

* Download verilator from hw-devtools for formal-tests in CI

* fix path for hw-devtools in CI

* fix path to hw-devtools

* cleaning CI rules for formal-verif

* Fix tar rules for hw-devtools

* Use verilator v5.006 for formal-tests CI

* Makefile: path to MATCHI

* reduce depth of VCD simulation + update to latest release of hw-devtools

* Fix DIR_MATCHI_ROOT in CI

* Add logfile to matchi + add workdir of formal checks in artifact

* Fix upload working dire befor running tests

* Fix flow for CI debug

* modify CI flows to ease offline VM bug replication

* Try with running in local 24.04

* Move to simulation with non-annotated netlist in formal-verif

* move to renamed signals in netlist for formal-verif simulation

* reset full formal verif in top-level Makefile

* Remove the hard dependence on matchi for target other thatn formal-tests in top Makefile + adapt CI for formal-tests

* Add Sbox generation from cache + dependencies in format-tests CI

---------

Co-authored-by: Gaëtan Cassiers <[email protected]>

.github/workflows/ci.yml

@@ -60,7 +60,7 @@ jobs:
         with:
           key: "sbox-compress-v1-d${{ matrix.nshares }}-${{ hashFiles('sboxes-compress/canright_aes_sbox_dual.v') }}-${{ steps.compress-version.outputs.cv }}"
           path: work/d${{ matrix.nshares }}/sbox
-      - run: make sbox
+      - run: make sbox DIR_MATCHI_ROOT=.
       - name: Upload COMPRESS sbox
         uses: actions/upload-artifact@v4
         with:
@@ -86,7 +86,34 @@ jobs:
           name: sbox_${{ matrix.nshares }}
           path: work/d${{ matrix.nshares }}/sbox
       - run: sudo apt-get install -y yosys verilator iverilog
-      - run: make func-tests
+      - run: make func-tests DIR_MATCHI_ROOT=.
+
+  formal_verif_matchi:
+    needs: [sbox]
+    runs-on: ubuntu-24.04
+    strategy:
+      fail-fast: true
+      matrix:
+        nshares: [2]
+    steps:
+      - name: Check out repository code
+        uses: actions/checkout@v4
+        with:
+          submodules: true
+      - uses: actions/download-artifact@v4
+        with:
+          name: sbox_${{ matrix.nshares }}
+          path: work/d${{ matrix.nshares }}/sbox
+      - run: sudo apt-get install -y yosys iverilog python3.12-venv
+      - run: mkdir -p ${{ github.workspace }}/verif-tools
+      - run: wget https://github.com/cassiersg/matchi/releases/download/v0.1.0/matchi -P ${{ github.workspace }}/verif-tools
+      - run: chmod +x ${{ github.workspace }}/verif-tools/matchi
+      - run: (cd ${{ github.workspace }}/verif-tools; curl -L https://github.com/cassiersg/matchi/archive/refs/tags/v0.1.0.tar.gz | tar xz)
+      - run: (curl -L https://github.com/simple-crypto/hw-devtools/releases/download/v241002-5/hw-devtools.tar.gz | tar xz; sudo apt install ./hw-devtools/*.deb)
+      - run: mkdir -p work
+      - run: verilator --version > work/verilator_version
+      - run: yosys --version > work/yosys_version
+      - run: make formal-tests DIR_MATCHI_ROOT=. MATCHI_CELLS=${{ github.workspace }}/verif-tools/matchi-0.1.0/matchi_cells MATCHI_BIN=${{ github.workspace }}/verif-tools/matchi
 
   release:
     needs: [build_latex, functest]

Makefile

@@ -9,6 +9,7 @@ VE=$(abspath $(WORKDIR)/ve)
 VE_INSTALLED=$(VE)/installed
 PYTHON_VE=source $(VE)/bin/activate
 
+### HDL configuration
 # Directory created containing all the HDL files
 DIR_HDL?=$(WORKDIR)/hdl
 HDL_DONE = $(DIR_HDL)/.gather
@@ -25,6 +26,7 @@ DIR_SMAESH_HDL=hdl/smaesh_hpc
 
 .PHONY: sbox hdl
 
+## Python venv setting
 $(VE)/pyvenv.cfg:
 	mkdir -p $(WORKDIR)
 	python3 -m venv $(VE)
@@ -46,7 +48,7 @@ $(HDL_DONE): $(SBOX_FILE)
 
 hdl: $(HDL_DONE)
 
-# Functionnal testing
+## Functionnal testing
 FUNC_LOG=$(WORKDIR)/functests/simu.log
 FUNC_SUCCESS=$(WORKDIR)/functests/success
 $(FUNC_LOG): $(VE_INSTALLED) $(HDL_DONE)
@@ -59,6 +61,30 @@ $(FUNC_LOG): $(VE_INSTALLED) $(HDL_DONE)
 
 func-tests: $(FUNC_SUCCESS)
 
+## Formal composition verification using matchi (SCA security)
+KEY_SIZE = 128 192 256
+DIR_FORMAL_VERIF=$(WORKDIR)/formal-verif
+
+### Matchi configuration
+# Path to the clone repo of matchi verification tool
+# Prefix to the file matchi_cells.v and matchi_cells.lib
+MATCHI_CELLS?=$(DIR_MATCHI_ROOT)/matchi_cells
+# Path to the mathci bin
+MATCHI_BIN?=$(DIR_MATCHI_ROOT)/matchi/target/release/matchi
+
+matchi_configured: 
+	@set e; if [ -z $${DIR_MATCHI_ROOT+x} ]; then echo "DIR_MATCHI_ROOT must be set for formal verification" && exit 1; else echo "DIR_MATCHI_ROOT=${DIR_MATCHI_ROOT}"; fi
+
+FORMAL_VERIF_DONE=$(DIR_FORMAL_VERIF)/.formal_verif
+$(FORMAL_VERIF_DONE): $(VE_INSTALLED) $(HDL_DONE) matchi_configured
+	# Verify encryption
+	$(foreach ksize,$(KEY_SIZE),$(PYTHON_VE); make -C ./formal_verif NSHARES=$(NSHARES) KEY_SIZE=$(ksize) INVERSE=0 MATCHI_CELLS=$(MATCHI_CELLS) MATCHI_BIN=$(MATCHI_BIN) WORKDIR=$(DIR_FORMAL_VERIF) HDL_DIR=$(DIR_HDL) matchi-run || exit 1;)
+	# Verify decryption
+	$(foreach ksize,$(KEY_SIZE),$(PYTHON_VE); make -C ./formal_verif NSHARES=$(NSHARES) KEY_SIZE=$(ksize) INVERSE=1 MATCHI_CELLS=$(MATCHI_CELLS) MATCHI_BIN=$(MATCHI_BIN) WORKDIR=$(DIR_FORMAL_VERIF) HDL_DIR=$(DIR_HDL) matchi-run || exit 1;)
+	touch $(FORMAL_VERIF_DONE)
+
+formal-tests: $(FORMAL_VERIF_DONE)
+
 
 clean:
-	if [ -d $(DIR_HDL) ]; then rm -r $(DIR_HDL); fi
+	if [ -d $(WORKDIR) ]; then rm -r $(WORKDIR); fi