[kmac/pre_syn] Enable Yosys synthesis of full SHA3 core or entire KMAC
Previously, we were only able to synthesize keccak_2share or
keccak_round, i.e., the core modules to formally analyze the masking
using Alma.
Signed-off-by: Pirmin Vogel <vogelpi@lowrisc.org>
diff --git a/hw/ip/kmac/pre_syn/syn_setup.example.sh b/hw/ip/kmac/pre_syn/syn_setup.example.sh
index de23713..ba0b527 100644
--- a/hw/ip/kmac/pre_syn/syn_setup.example.sh
+++ b/hw/ip/kmac/pre_syn/syn_setup.example.sh
@@ -7,12 +7,14 @@
# Setup IP name and top module.
# When changing the top module, some parameters might not exist and
# tcl/yosys_run_synth.tcl might need to be adjusted accordingly.
+# Known working top modules are: keccak_2share, keccak_round, sha3, kmac
export LR_SYNTH_IP_NAME=kmac
export LR_SYNTH_TOP_MODULE=keccak_2share
# Setup module parameters. The Width is actually 1600 but it can have any value
# in [25, 50, 100, 200, 400, 800, 1600]. We choose 25 instead to get smaller
-# netlist thereby speeding up the formal masking verification.
+# netlist thereby speeding up the formal masking verification. Ignored for sha3
+# and kmac top modules.
export LR_SYNTH_WIDTH=25
export LR_SYNTH_EN_MASKING=1
diff --git a/hw/ip/kmac/pre_syn/syn_yosys.sh b/hw/ip/kmac/pre_syn/syn_yosys.sh
index 860018d..235ec69 100755
--- a/hw/ip/kmac/pre_syn/syn_yosys.sh
+++ b/hw/ip/kmac/pre_syn/syn_yosys.sh
@@ -72,8 +72,21 @@
"$LR_SYNTH_SRC_DIR"/../prim_xilinx/rtl/prim_xilinx_flop_en.sv
"$LR_SYNTH_SRC_DIR"/../prim_xilinx/rtl/prim_xilinx_buf.sv
"$LR_SYNTH_SRC_DIR"/../prim_xilinx/rtl/prim_xilinx_xor2.sv
+ "$LR_SYNTH_SRC_DIR"/../tlul/rtl/tlul_adapter_sram.sv
+ "$LR_SYNTH_SRC_DIR"/../tlul/rtl/tlul_sram_byte.sv
+ "$LR_SYNTH_SRC_DIR"/../tlul/rtl/tlul_socket_1n.sv
+ "$LR_SYNTH_SRC_DIR"/../tlul/rtl/tlul_err_resp.sv
+ "$LR_SYNTH_SRC_DIR"/../tlul/rtl/tlul_fifo_sync.sv
"$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_dom_and_2share.sv
"$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_keccak.sv
+ "$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_slicer.sv
+ "$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_intr_hw.sv
+ "$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_edn_req.sv
+ "$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_fifo_sync.sv
+ "$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_arbiter_fixed.sv
+ "$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_packer.sv
+ "$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_count.sv
+ "$LR_SYNTH_SRC_DIR"/../prim/rtl/prim_double_lfsr.sv
)
# Get OpenTitan dependency packages.
@@ -126,11 +139,6 @@
continue
fi
- # Skipe certain problematic module files that we don't need for the keccak_2share module.
- if [ "$module" = "kmac_app" ]; then
- continue
- fi
-
sv2v \
--define=SYNTHESIS \
"${OT_DEP_PACKAGES[@]}" \
@@ -155,7 +163,7 @@
# Remove the StateEnumT parameter from prim_sparse_fsm_flop instances. Yosys doesn't seem to
# support this.
sed -i '/\.StateEnumT(logic \[.*/d' $LR_SYNTH_OUT_DIR/generated/${module}.v
- sed -i '/\.StateEnumT_StateWidth(.*/d' $LR_SYNTH_OUT_DIR/generated/${module}.v
+ sed -i '/\.StateEnumT.*StateWidth.*(.*/d' $LR_SYNTH_OUT_DIR/generated/${module}.v
done
#-------------------------------------------------------------------------
diff --git a/hw/ip/kmac/pre_syn/tcl/yosys_run_synth.tcl b/hw/ip/kmac/pre_syn/tcl/yosys_run_synth.tcl
index ab53257..ad57cb4 100644
--- a/hw/ip/kmac/pre_syn/tcl/yosys_run_synth.tcl
+++ b/hw/ip/kmac/pre_syn/tcl/yosys_run_synth.tcl
@@ -18,7 +18,9 @@
# Set top-module parameters.
yosys "chparam -set EnMasking $lr_synth_en_masking $lr_synth_top_module"
-yosys "chparam -set Width $lr_synth_width $lr_synth_top_module"
+if { $lr_synth_top_module == "keccak_2share" || $lr_synth_top_module == "keccak_round"} {
+ yosys "chparam -set Width $lr_synth_width $lr_synth_top_module"
+}
# Remap Xilinx Vivado "dont_touch" attributes to Yosys "keep" attributes.
yosys "attrmap -tocase keep -imap dont_touch=\"yes\" keep=1 -imap dont_touch=\"no\" keep=0 -remove keep=0"
