[otbn/hw] Add HPC gadgets to prims

hw/ip/otbn/pre_sca/alma/cpp/testbench.h

@@ -0,0 +1,73 @@
+// Copyright lowRISC contributors (OpenTitan project).
+// Copyright IAIK.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+#ifndef OPENTITAN_HW_IP_MASK_ACC_PRE_SCA_ALMA_CPP_TESTBENCH_H_
+#define OPENTITAN_HW_IP_MASK_ACC_PRE_SCA_ALMA_CPP_TESTBENCH_H_
+
+#include "verilated.h"
+#include "verilated_vcd_c.h"
+
+template <class Module>
+struct Testbench {
+  unsigned long m_tickcount;
+  Module m_core;
+  VerilatedVcdC *m_trace = NULL;
+
+  Testbench() {
+    Verilated::traceEverOn(true);
+    m_tickcount = 0ul;
+  }
+
+  ~Testbench() { closetrace(); }
+
+  void opentrace(const char *vcdname) {
+    if (!m_trace) {
+      m_trace = new VerilatedVcdC;
+      m_core.trace(m_trace, 99);
+      m_trace->open(vcdname);
+    }
+  }
+
+  void closetrace() {
+    if (m_trace) {
+      m_trace->close();
+      delete m_trace;
+      m_trace = NULL;
+    }
+  }
+
+  void reset() {
+    m_core.rst_ni = 0;
+    this->tick();
+    this->tick();
+    m_core.rst_ni = 1;
+  }
+
+  void tick() {
+    // Falling edge
+    m_core.clk_i = 0;
+    m_core.eval();
+    if (m_trace)
+      m_trace->dump(20 * m_tickcount);
+
+    // Rising edge
+    m_core.clk_i = 1;
+    m_core.eval();
+    if (m_trace)
+      m_trace->dump(20 * m_tickcount + 10);
+
+    // Falling edge settle eval
+    m_core.clk_i = 0;
+    m_core.eval();
+
+    if (m_trace)
+      m_trace->flush();
+    m_tickcount++;
+  }
+
+  bool done() { return Verilated::gotFinish(); }
+};
+
+#endif  // OPENTITAN_HW_IP_MASK_ACC_PRE_SCA_ALMA_CPP_TESTBENCH_H_

hw/ip/otbn/pre_sca/alma/cpp/verilator_tb_otbn_hpc2_and_sca_wrapper.cpp

@@ -0,0 +1,47 @@
+// Copyright lowRISC contributors (OpenTitan project).
+// Copyright IAIK.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+#include <stdio.h>
+#include <random>
+#include "Vcircuit.h"
+#include "testbench.h"
+
+int main(int argc, char **argv) {
+  Verilated::commandArgs(argc, argv);
+  Testbench<Vcircuit> tb;
+  tb.opentrace("tmp.vcd");
+
+  // RNG Setup for high-quality entropy
+  std::random_device rd;
+  std::mt19937 gen(rd());
+  std::uniform_int_distribution<uint32_t> dis(0, 0xFFFFFFFF);
+
+  tb.reset();
+
+  // Mask for the randomness
+  const uint32_t WORD_MASK = 0x1;
+
+  // Initialize the first cycle of randomness
+  tb.m_core.rand_i = dis(gen) & WORD_MASK;
+
+  // Drive Combined Shares (A and B)
+  tb.m_core.share0_i = 0x2;
+  tb.m_core.share1_i = 0x3;
+  tb.m_core.en_i = 0x0;
+
+  tb.tick();
+
+  tb.m_core.en_i = 0x1;
+
+  // Simulation Run
+  for (int i = 0; i < 3; i++) {
+    tb.tick();
+    tb.m_core.en_i = 0x0; 
+    tb.m_core.rand_i = dis(gen) & WORD_MASK;
+  }
+
+  tb.closetrace();
+  return 0;
+}

hw/ip/otbn/pre_sca/alma/cpp/verilator_tb_otbn_hpc2o_sca_wrapper.cpp

@@ -0,0 +1,47 @@
+// Copyright lowRISC contributors (OpenTitan project).
+// Copyright IAIK.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+#include <stdio.h>
+#include <random>
+#include "Vcircuit.h"
+#include "testbench.h"
+
+int main(int argc, char **argv) {
+  Verilated::commandArgs(argc, argv);
+  Testbench<Vcircuit> tb;
+  tb.opentrace("tmp.vcd");
+
+  // RNG Setup for high-quality entropy
+  std::random_device rd;
+  std::mt19937 gen(rd());
+  std::uniform_int_distribution<uint32_t> dis(0, 0xFFFFFFFF);
+
+  tb.reset();
+
+  // Mask for the randomness
+  const uint32_t WORD_MASK = 0x1;
+
+  // Initialize the first cycle of randomness
+  tb.m_core.rand_i = dis(gen) & WORD_MASK;
+
+  // Drive Combined Shares (A and B)
+  tb.m_core.share0_i = 0x4;
+  tb.m_core.share1_i = 0x3;
+  tb.m_core.en_i = 0x0;
+
+  tb.tick();
+
+  tb.m_core.en_i = 0x1;
+
+  // Simulation Run
+  for (int i = 0; i < 3; i++) {
+    tb.tick();
+    tb.m_core.en_i = 0x0; 
+    tb.m_core.rand_i = dis(gen) & WORD_MASK;
+  }
+
+  tb.closetrace();
+  return 0;
+}

hw/ip/otbn/pre_sca/alma/cpp/verilator_tb_otbn_hpc3_and_sca_wrapper.cpp

@@ -0,0 +1,47 @@
+// Copyright lowRISC contributors (OpenTitan project).
+// Copyright IAIK.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+#include <stdio.h>
+#include <random>
+#include "Vcircuit.h"
+#include "testbench.h"
+
+int main(int argc, char **argv) {
+  Verilated::commandArgs(argc, argv);
+  Testbench<Vcircuit> tb;
+  tb.opentrace("tmp.vcd");
+
+  // RNG Setup for high-quality entropy
+  std::random_device rd;
+  std::mt19937 gen(rd());
+  std::uniform_int_distribution<uint32_t> dis(0, 0xFFFFFFFF);
+
+  tb.reset();
+
+  // Mask for the randomness
+  const uint32_t WORD_MASK = 0x3;
+
+  // Initialize the first cycle of randomness
+  tb.m_core.rand_i = dis(gen) & WORD_MASK;
+
+  // Drive Combined Shares (A and B)
+  tb.m_core.share0_i = 0x2;
+  tb.m_core.share1_i = 0x3;
+  tb.m_core.en_i = 0x0;
+
+  tb.tick();
+
+  tb.m_core.en_i = 0x1;
+
+  // Simulation Run
+  for (int i = 0; i < 3; i++) {
+    tb.tick();
+    tb.m_core.en_i = 0x0; 
+    tb.m_core.rand_i = dis(gen) & WORD_MASK;
+  }
+
+  tb.closetrace();
+  return 0;
+}

hw/ip/otbn/pre_sca/alma/cpp/verilator_tb_otbn_hpc3o_sca_wrapper.cpp

@@ -0,0 +1,47 @@
+// Copyright lowRISC contributors (OpenTitan project).
+// Copyright IAIK.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+#include <stdio.h>
+#include <random>
+#include "Vcircuit.h"
+#include "testbench.h"
+
+int main(int argc, char **argv) {
+  Verilated::commandArgs(argc, argv);
+  Testbench<Vcircuit> tb;
+  tb.opentrace("tmp.vcd");
+
+  // RNG Setup for high-quality entropy
+  std::random_device rd;
+  std::mt19937 gen(rd());
+  std::uniform_int_distribution<uint32_t> dis(0, 0xFFFFFFFF);
+
+  tb.reset();
+
+  // Mask for the randomness
+  const uint32_t WORD_MASK = 0x3;
+
+  // Initialize the first cycle of randomness
+  tb.m_core.rand_i = dis(gen) & WORD_MASK;
+
+  // Drive Combined Shares (A and B)
+  tb.m_core.share0_i = 0x4;
+  tb.m_core.share1_i = 0x3;
+  tb.m_core.en_i = 0x0;
+
+  tb.tick();
+
+  tb.m_core.en_i = 0x1;
+
+  // Simulation Run
+  for (int i = 0; i < 3; i++) {
+    tb.tick();
+    tb.m_core.en_i = 0x0; 
+    tb.m_core.rand_i = dis(gen) & WORD_MASK;
+  }
+
+  tb.closetrace();
+  return 0;
+}

hw/ip/otbn/pre_sca/alma/verify_sec_add.sh

@@ -0,0 +1,48 @@
+#!/bin/bash
+# Copyright lowRISC contributors (OpenTitan project).
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# Script to formally verify the masking of the SEC_ADD unit using Alma.
+
+set -e
+
+# Argument parsing
+TARGET_TYPE="${1:-mask_accelerator}"
+case "$TARGET_TYPE" in
+  hpc2_and) export TOP_MODULE=otbn_hpc2_and_sca_wrapper ;;
+  hpc2o)    export TOP_MODULE=otbn_hpc2o_sca_wrapper ;;
+  hpc3_and) export TOP_MODULE=otbn_hpc3_and_sca_wrapper ;;
+  hpc3o)    export TOP_MODULE=otbn_hpc3o_sca_wrapper ;;
+  *)        export TOP_MODULE=otbn_hpc3o_sca_wrapper ;;
+esac
+
+TESTBENCH=${TOP_MODULE}
+
+echo "Verifying ${TOP_MODULE} using Alma"
+
+# Parse
+./parse.py --top-module ${TOP_MODULE} \
+--source ${REPO_TOP}/hw/ip/otbn/pre_syn/syn_out/latest/generated/${TOP_MODULE}.alma.v \
+--netlist tmp/circuit.v --log-yosys
+
+# Label
+sed -i 's/\(share0_i\s\[\)\([0-9]\+:0\)\(\]\s=\s\)unimportant/\1\2\3secret \2/g' tmp/labels.txt
+sed -i 's/\(share1_i\s\[\)\([0-9]\+:0\)\(\]\s=\s\)unimportant/\1\2\3secret \2/g' tmp/labels.txt
+sed -i 's/\(rand_i\s\[[0-9]\+:0\]\s=\s\)unimportant/\1random/g' tmp/labels.txt
+sed -i 's/\(rand_i\s=\s\)unimportant/\1random/g' tmp/labels.txt
+
+# Trace
+./trace.py --testbench ${REPO_TOP}/hw/ip/otbn/pre_sca/alma/cpp/verilator_tb_${TESTBENCH}.cpp \
+  --netlist tmp/circuit.v --c-compiler gcc -o tmp/circuit
+
+# Verify
+./verify.py --json tmp/circuit.json \
+  --label tmp/labels.txt \
+  --top-module ${TOP_MODULE} \
+  --vcd tmp/tmp.vcd \
+  --rst-name rst_ni --rst-phase 0 \
+  --probe-duration once \
+  --mode transient \
+  --glitch-behavior strict \
+  --cycles 6

hw/ip/otbn/pre_sca/prolead/evaluate.sh

@@ -0,0 +1,52 @@
+#!/bin/bash
+# Copyright lowRISC contributors (OpenTitan project).
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# Script for evaluating e.g. the secure adder implementation
+# cipher core using PROLEAD.
+
+set -e
+
+case "$1" in
+  hpc2_and)
+    TOP_MODULE=otbn_hpc2_and_sca_wrapper
+    ;;
+  hpc2o)
+    TOP_MODULE=otbn_hpc2o_sca_wrapper
+    ;;
+  hpc3_and)
+    TOP_MODULE=otbn_hpc3_and_sca_wrapper
+    ;;
+  hpc3o)
+    TOP_MODULE=otbn_hpc3o_sca_wrapper
+    ;;
+  *)
+    # Default case.
+    TOP_MODULE=otbn_hpc3o_sca_wrapper
+    ;;
+esac
+if [[ "$#" -gt 1 ]]; then
+  NETLIST_DIR=$2
+else
+  NETLIST_DIR="${REPO_TOP}/hw/ip/otbn/pre_syn/syn_out/latest/generated"
+fi
+
+perl -i -pe "s/(\d+)'h0+/ join(', ', ('1\\'b0') x \$1) /ge" ${NETLIST_DIR}/${TOP_MODULE}_netlist.v
+
+# Create results directory.
+OUT_DIR_PREFIX="out/${TOP_MODULE}"
+OUT_DIR=$(date +"${OUT_DIR_PREFIX}_%Y_%m_%d_%H_%M_%S")
+mkdir -p ${OUT_DIR}
+rm -f out/latest
+ln -s "${OUT_DIR#out/}" out/latest
+
+echo ${REPO_TOP}/hw/ip/otbn/pre_sca/prolead/server_config_${TOP_MODULE}.json
+
+# Launch the tool.
+PROLEAD -l ${REPO_TOP}/hw/ip/otbn/pre_sca/prolead/nang45.json \
+        -n nang45 \
+        -d ${NETLIST_DIR}/${TOP_MODULE}_netlist.v \
+        -m ${TOP_MODULE} \
+        -rf ${OUT_DIR} \
+        -c ${REPO_TOP}/hw/ip/otbn/pre_sca/prolead/server_config_${TOP_MODULE}.json