Code

Ci formalverif#5

Code

Merged

cmomin merged 29 commits intomainsimple-crypto/SMAesH:mainfrom CI-formalverifsimple-crypto/SMAesH:CI-formalverifCopy head branch name to clipboardOct 3, 2024

+246-11,143

Commits

Commits on Oct 1, 2024

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

  cmomin

  committed
  fb9d82a

  Copy full SHA for fb9d82a

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

  cmomin

  committed
  25c27c6

  Copy full SHA for 25c27c6

• Add formal test in continuous integration

  cmomin

  committed
  42fed28

  Copy full SHA for 42fed28

• Add formal test in continuous integration

  cmomin

  committed
  9f7f7d3

  Copy full SHA for 9f7f7d3

• fix conflict

  cmomin

  committed
  d3446db

  Copy full SHA for d3446db

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

  cmomin

  committed
  df43e9d

  Copy full SHA for df43e9d

• add iverilog in dependencies for formal-tests CI

  cmomin

  committed
  5cef1cb

  Copy full SHA for 5cef1cb

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

  cmomin

  committed
  5a4392d

  Copy full SHA for 5a4392d

Commits on Oct 2, 2024

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

  cmomin

  committed
  1334903

  Copy full SHA for 1334903

• fix path for hw-devtools in CI

  cmomin

  committed
  2c232bf

  Copy full SHA for 2c232bf

• fix path to hw-devtools

  cmomin

  committed
  f975f26

  Copy full SHA for f975f26

• cleaning CI rules for formal-verif

  cmomin

  committed
  4018f5a

  Copy full SHA for 4018f5a

• Fix tar rules for hw-devtools

  cmomin

  committed
  9d34140

  Copy full SHA for 9d34140

• merge with main

  cmomin

  committed
  06a7870

  Copy full SHA for 06a7870

• Use verilator v5.006 for formal-tests CI

  cmomin

  committed
  e211495

  Copy full SHA for e211495

• Makefile: path to MATCHI

  cassiersg

  committed
  f2ddf85

  Copy full SHA for f2ddf85

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

  cmomin

  committed
  267f25b

  Copy full SHA for 267f25b

• Fix DIR_MATCHI_ROOT in CI

  cmomin

  committed
  6882823

  Copy full SHA for 6882823

Commits on Oct 3, 2024

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

  cmomin

  committed
  0382840

  Copy full SHA for 0382840

• Fix upload working dire befor running tests

  cmomin

  committed
  a10a9fd

  Copy full SHA for a10a9fd

• Fix flow for CI debug

  cmomin

  committed
  874ba7c

  Copy full SHA for 874ba7c

• modify CI flows to ease offline VM bug replication

  cmomin

  committed
  75f8ba5

  Copy full SHA for 75f8ba5

• Try with running in local 24.04

  cmomin

  committed
  3fcedc6

  Copy full SHA for 3fcedc6

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

  cmomin

  committed
  e0d7e6b

  Copy full SHA for e0d7e6b

• Merge branch 'CI-formalverif' of github.com:simple-crypto/SMAesH into CI-formalverif

  cmomin

  committed
  41a5c12

  Copy full SHA for 41a5c12

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

  cmomin

  committed
  7a41e99

  Copy full SHA for 7a41e99

• reset full formal verif in top-level Makefile

  cmomin

  committed
  89f70a1

  Copy full SHA for 89f70a1

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

  cmomin

  committed
  400c29a

  Copy full SHA for 400c29a

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

  cmomin

  committed
  0cc7c67

  Copy full SHA for 0cc7c67