[aes/pre_dv] Add scratch verification and LEC scripts for S-Boxes
This commit adds both a scratch Verilator verification TB as well as a
LEC script for Yosys to verify equivalence of different S-Box
implementations.
Signed-off-by: Pirmin Vogel <vogelpi@lowrisc.org>
diff --git a/hw/ip/aes/pre_dv/aes_sbox_lec/.gitignore b/hw/ip/aes/pre_dv/aes_sbox_lec/.gitignore
new file mode 100644
index 0000000..fb188b9
--- /dev/null
+++ b/hw/ip/aes/pre_dv/aes_sbox_lec/.gitignore
@@ -0,0 +1 @@
+scratch
diff --git a/hw/ip/aes/pre_dv/aes_sbox_lec/aes_sbox_lec.py b/hw/ip/aes/pre_dv/aes_sbox_lec/aes_sbox_lec.py
new file mode 100755
index 0000000..e65eb01
--- /dev/null
+++ b/hw/ip/aes/pre_dv/aes_sbox_lec/aes_sbox_lec.py
@@ -0,0 +1,102 @@
+#!/usr/bin/env python3
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+r"""Command-line tool to perform LEC on all AES S-Box implementations using Yosys
+
+"""
+import glob
+import os
+import subprocess
+import sys
+
+
+def replace_module_name(file_name, string_search, string_replace):
+ fin = open(file_name, 'rt')
+ data = fin.read()
+ data = data.replace(string_search, string_replace)
+ fin.close()
+ fin = open(file_name, 'wt')
+ fin.write(data)
+ fin.close()
+
+
+rtl_path = '../../rtl/'
+
+# List all S-Box reference implementation + AES package
+impl_gold = 'aes_sbox_lut'
+file_pkg = 'aes_pkg.sv'
+
+# Detect all S-Box implementations to check
+impl_list = glob.glob(rtl_path + 'aes_sbox_*.sv')
+impl_list = [
+ impl_dut.replace(rtl_path, '').replace('.sv', '') for impl_dut in impl_list
+]
+impl_list.remove(impl_gold)
+
+# Create workdir
+os.makedirs('scratch', exist_ok=True)
+
+# Convert the reference implementation to Verilog
+sv2v_cmd = ['sv2v', rtl_path + impl_gold + '.sv', rtl_path + file_pkg]
+with open('scratch/aes_sbox_ref.v', 'w') as outfile:
+ subprocess.run(sv2v_cmd, stdout=outfile)
+
+# Change module name
+replace_module_name('scratch/aes_sbox_ref.v', impl_gold, 'aes_sbox_ref')
+
+print('Running LEC on ' + str(len(impl_list)) + ' S-Box implementation(s)...')
+
+# Check every implementation separately
+num_impl_success = 0
+num_impl_failed = 0
+for impl_dut in impl_list:
+
+ # Convert DUT to Verilog
+ sv2v_cmd = ['sv2v', rtl_path + impl_dut + '.sv', rtl_path + file_pkg]
+ with open('scratch/aes_sbox_dut.v', 'w') as outfile:
+ subprocess.run(sv2v_cmd, stdout=outfile)
+
+ # Change module name
+ replace_module_name('scratch/aes_sbox_dut.v', impl_dut, 'aes_sbox_dut')
+
+ ## Perform LEC in Yosys
+ yosys_cmd = ['yosys', '../aes_sbox_lec.ys']
+ lec_log = 'scratch/' + impl_dut + '_lec.log'
+ with open(lec_log, 'w') as outfile:
+ subprocess.run(yosys_cmd, cwd="scratch", stdout=outfile)
+
+ # Get actual LEC output
+ lec_string = 'Trying to prove $equiv'
+ lec_lines = []
+ with open(lec_log, 'rt') as fin:
+ data = fin.read()
+ for line in data.split('\n'):
+ if lec_string in line:
+ lec_lines.append(line)
+
+ # Check for LEC output
+ num_lec_success = 0
+ num_lec_failed = 0
+ for line in lec_lines:
+ if 'success!' in line:
+ num_lec_success = num_lec_success + 1
+ if 'failed.' in line:
+ num_lec_failed = num_lec_failed + 1
+
+ if (len(lec_lines) == 0) or (len(lec_lines) !=
+ num_lec_success) or (num_lec_failed > 0):
+ print("LEC failed: \t\t\t" + impl_dut + '.sv\n-> ' + 'Check ' +
+ lec_log + ' for details.')
+ num_impl_failed = num_impl_failed + 1
+ else:
+ print("LEC completed successfully: \t" + impl_dut + '.sv')
+ num_impl_success = num_impl_success + 1
+
+# Print output
+print('Done.')
+if (num_impl_success == len(impl_list)) and not num_impl_failed:
+ print('SUCCESS!')
+else:
+ print('FAILED for ' + str(num_impl_failed) + ' implementation(s).')
+ sys.exit(1)
diff --git a/hw/ip/aes/pre_dv/aes_sbox_lec/aes_sbox_lec.ys b/hw/ip/aes/pre_dv/aes_sbox_lec/aes_sbox_lec.ys
new file mode 100644
index 0000000..886cf5c
--- /dev/null
+++ b/hw/ip/aes/pre_dv/aes_sbox_lec/aes_sbox_lec.ys
@@ -0,0 +1,17 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+
+# Yosys script to perform LEC between two different AES S-Box implementations.
+
+# Read the Verilog sources
+read_verilog aes_sbox_ref.v aes_sbox_dut.v
+
+# Do some preprocessing
+proc
+
+# Set up equivalence check
+equiv_make aes_sbox_ref aes_sbox_dut aes_sbox_equiv
+
+# Do the logic equivalence check
+equiv_simple
diff --git a/hw/ip/aes/pre_dv/aes_sbox_tb/README.md b/hw/ip/aes/pre_dv/aes_sbox_tb/README.md
new file mode 100644
index 0000000..98b59cf
--- /dev/null
+++ b/hw/ip/aes/pre_dv/aes_sbox_tb/README.md
@@ -0,0 +1,31 @@
+AES S-Box Verilator Testbench
+=============================
+
+This directory contains a basic, scratch Verilator testbench targeting
+functional verification of different S-Box implementations during
+development.
+
+How to build and run the testbench
+----------------------------------
+
+From the OpenTitan top level execute
+
+ ```sh
+ fusesoc --cores-root=. run --setup --build lowrisc:dv_verilator:aes_sbox_tb
+ ```
+to build the testbench and afterwards
+
+ ```sh
+ ./build/lowrisc_dv_verilator_aes_sbox_tb_0/default-verilator/Vaes_sbox_tb \
+ --trace
+ ```
+to run it.
+
+Details of the testbench
+------------------------
+
+- `rtl/aes_sbox_tb.sv`: SystemVerilog testbench, instantiates and drives the
+ different S-Box implementations, compares outputs, signals test end and
+ result (pass/fail) to C++ via output ports.
+- `cpp/aes_sbox_tb.cc`: Contains main function and instantiation of SimCtrl,
+ reads output ports of DUT and signals simulation termination to Verilator.
diff --git a/hw/ip/aes/pre_dv/aes_sbox_tb/aes_sbox_tb.core b/hw/ip/aes/pre_dv/aes_sbox_tb/aes_sbox_tb.core
new file mode 100644
index 0000000..3afe822
--- /dev/null
+++ b/hw/ip/aes/pre_dv/aes_sbox_tb/aes_sbox_tb.core
@@ -0,0 +1,52 @@
+CAPI=2:
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+name: "lowrisc:dv_verilator:aes_sbox_tb"
+description: "AES SBox Verilator TB"
+filesets:
+ files_rtl:
+ depend:
+ - lowrisc:ip:aes:0.6
+ files:
+ - rtl/aes_sbox_tb.sv
+ file_type: systemVerilogSource
+
+ files_dv_verilator:
+ depend:
+ - lowrisc:dv_verilator:simutil_verilator
+
+ files:
+ - cpp/aes_sbox_tb.cc
+ file_type: cppSource
+
+targets:
+ default:
+ default_tool: verilator
+ filesets:
+ - files_rtl
+ - files_dv_verilator
+ toplevel: aes_sbox_tb
+ tools:
+ verilator:
+ mode: cc
+ verilator_options:
+# Disabling tracing reduces compile times by multiple times, but doesn't have a
+# huge influence on runtime performance. (Based on early observations.)
+ - '--trace'
+ - '--trace-fst' # this requires -DVM_TRACE_FMT_FST in CFLAGS below!
+ - '--trace-structs'
+ - '--trace-params'
+ - '--trace-max-array 1024'
+# compiler flags
+#
+# -O
+# Optimization levels have a large impact on the runtime performance of the
+# simulation model. -O2 and -O3 are pretty similar, -Os is slower than -O2/-O3
+ - '-CFLAGS "-std=c++11 -Wall -DVM_TRACE_FMT_FST -DTOPLEVEL_NAME=aes_sbox_tb -g -O0"'
+ - '-LDFLAGS "-pthread -lutil -lelf"'
+ - "-Wall"
+ - "-Wno-PINCONNECTEMPTY"
+ # XXX: Cleanup all warnings and remove this option
+ # (or make it more fine-grained at least)
+ - "-Wno-fatal"
diff --git a/hw/ip/aes/pre_dv/aes_sbox_tb/cpp/aes_sbox_tb.cc b/hw/ip/aes/pre_dv/aes_sbox_tb/cpp/aes_sbox_tb.cc
new file mode 100644
index 0000000..b6841e9
--- /dev/null
+++ b/hw/ip/aes/pre_dv/aes_sbox_tb/cpp/aes_sbox_tb.cc
@@ -0,0 +1,61 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+
+#include "Vaes_sbox_tb.h"
+#include "verilated_toplevel.h"
+#include "verilator_sim_ctrl.h"
+
+#include <signal.h>
+#include <functional>
+#include <iostream>
+
+#include "sim_ctrl_extension.h"
+
+class AESSBoxTB : public SimCtrlExtension {
+ using SimCtrlExtension::SimCtrlExtension;
+
+ public:
+ AESSBoxTB(aes_sbox_tb *top);
+
+ void OnClock(unsigned long sim_time);
+
+ private:
+ aes_sbox_tb *top_;
+};
+
+// Constructor:
+// - Set up top_ ptr
+AESSBoxTB::AESSBoxTB(aes_sbox_tb *top) : SimCtrlExtension{}, top_(top) {}
+
+// Function called once every clock cycle from SimCtrl
+void AESSBoxTB::OnClock(unsigned long sim_time) {
+ if (top_->test_done_o) {
+ VerilatorSimCtrl::GetInstance().RequestStop(top_->test_passed_o);
+ }
+}
+
+int main(int argc, char **argv) {
+ int ret_code;
+
+ // Init verilog instance
+ aes_sbox_tb top;
+
+ // Init sim
+ VerilatorSimCtrl &simctrl = VerilatorSimCtrl::GetInstance();
+ simctrl.SetTop(&top, &top.clk_i, &top.rst_ni,
+ VerilatorSimCtrlFlags::ResetPolarityNegative);
+
+ // Create and register VerilatorSimCtrl extension
+ AESSBoxTB aessboxtb(&top);
+ simctrl.RegisterExtension(&aessboxtb);
+
+ std::cout << "Simulation of AES SBox" << std::endl
+ << "======================" << std::endl
+ << std::endl;
+
+ // Get pass / fail from Verilator
+ ret_code = simctrl.Exec(argc, argv);
+
+ return ret_code;
+}
diff --git a/hw/ip/aes/pre_dv/aes_sbox_tb/rtl/aes_sbox_tb.sv b/hw/ip/aes/pre_dv/aes_sbox_tb/rtl/aes_sbox_tb.sv
new file mode 100644
index 0000000..5058714
--- /dev/null
+++ b/hw/ip/aes/pre_dv/aes_sbox_tb/rtl/aes_sbox_tb.sv
@@ -0,0 +1,76 @@
+// Copyright lowRISC contributors.
+// Licensed under the Apache License, Version 2.0, see LICENSE for details.
+// SPDX-License-Identifier: Apache-2.0
+//
+// AES SBox testbench
+
+module aes_sbox_tb #(
+) (
+ input logic clk_i,
+ input logic rst_ni,
+
+ output logic test_done_o,
+ output logic test_passed_o
+);
+
+ import aes_pkg::*;
+
+ logic [8:0] count_d, count_q;
+ logic [7:0] stimulus;
+ ciph_op_e op;
+
+ localparam int NUM_SBOX_IMPLS = 2;
+ logic [7:0] responses[NUM_SBOX_IMPLS];
+
+ // Generate the stimuli
+ assign count_d = count_q + 9'h1;
+ always_ff @(posedge clk_i or negedge rst_ni) begin : reg_count
+ if (!rst_ni) begin
+ count_q <= '0;
+ end else begin
+ count_q <= count_d;
+ end
+ end
+
+ assign op = count_q[8] ? CIPH_FWD : CIPH_INV;
+ assign stimulus = count_q[7:0];
+
+ // Instantiate SBox Implementations
+ aes_sbox #(
+ .SBoxImpl ( "lut" )
+ ) aes_sbox_lut (
+ .op_i ( op ),
+ .data_i ( stimulus ),
+ .data_o ( responses[0] )
+ );
+
+ aes_sbox #(
+ .SBoxImpl ( "canright" )
+ ) aes_sbox_canright (
+ .op_i ( op ),
+ .data_i ( stimulus ),
+ .data_o ( responses[1] )
+ );
+
+ // Check responses, signal end of simulation
+ always_ff @(posedge clk_i or negedge rst_ni) begin : tb_ctrl
+ test_done_o <= 1'b0;
+ test_passed_o <= 1'b1;
+
+ for (int i=1; i<NUM_SBOX_IMPLS; i++) begin
+ if (rst_ni && (responses[i] != responses[0])) begin
+ $display("\nERROR: Mismatch between LUT-based S-Box and Implementation %0d found.", i);
+ $display("op = %s, stimulus = 8'h%h, expected resp = 8'h%h, actual resp = 8'h%h\n",
+ (op == CIPH_FWD) ? "CIPH_FWD" : "CIPH_INV", stimulus, responses[0], responses[1]);
+ test_passed_o <= 1'b0;
+ test_done_o <= 1'b1;
+ end
+ end
+
+ if (count_q == 9'h1FF) begin
+ $display("\nSUCCESS: Outputs of all S-Box implementations match.");
+ test_done_o <= 1'b1;
+ end
+ end
+
+endmodule