[util/syn_yosys] Add file lists to syn_yosys flow and run LEC on full design
Signed-off-by: Nils Graef <nilsg@google.com>
Signed-off-by: Nils Graf <nilsg@google.com>
diff --git a/hw/formal/lec_sv2v b/hw/formal/lec_sv2v
deleted file mode 100755
index a3b0414..0000000
--- a/hw/formal/lec_sv2v
+++ /dev/null
@@ -1,24 +0,0 @@
-#!/bin/bash
-
-# Copyright lowRISC contributors.
-# Licensed under the Apache License, Version 2.0, see LICENSE for details.
-# SPDX-License-Identifier: Apache-2.0
-
-# This script runs LEC (logical equivalence checking) between 2 RTL
-# files using Cadence Conformal LEC. Specifically, it checks if the
-# Verilog file gnereated by the sv2v tool is logically equivalent to
-# the original SystemVerilog.
-#
-# Usage: lec_sv2v <path-to-files> <module-name>
-# Example: To run lec between prim_subreg.sv and generated prim_subreg.v,
-# which are in directory ../../util/syn_out, type:
-# lec_sv2v ../../util/syn_out prim_subreg
-
-export LEC_DIR=${1}
-export LEC_TOP=${2}
-
-# run Conformal LEC
-lec -xl -nogui -nobanner \
- -dofile lec_sv2v.do \
- -logfile lec_${LEC_TOP}.log \
- <<< "exit -force"
diff --git a/hw/formal/lec_sv2v.do b/hw/formal/lec_sv2v.do
index 8495730..18b4cd3 100644
--- a/hw/formal/lec_sv2v.do
+++ b/hw/formal/lec_sv2v.do
@@ -4,64 +4,41 @@
// dofile for LEC script lec_sv2v
-//-----------------------------------------------------------------
+//-------------------------------------------------------------------------
// read in golden (SystemVerilog) and revised (Verilog)
-//-----------------------------------------------------------------
+//-------------------------------------------------------------------------
+set parallel option -threads 8
-// black box all instantiated modules (so only top-module is used)
-set undefined cell black_box
-
-// flatten module ports for comparison
+// map all multi-dimensional ports (including structs) onto 1-dim. ports
set naming rule -mdportflatten
-// Some of the prim_generic_ modules are instantiated using SystemVerilog
-// wildcard port bindings. These wildcard bindings are elaborated during
-// conversion. For the comparison to work, we need to read the signature of
-// these modules, but we still want to treat them as black boxes.
-add notranslate filepathnames $LEC_DIR/prim_*.*
+read design -golden -sv12 -f flist_gold -rootonly -root $LEC_TOP
+read design -revised -ve -f flist_rev -rootonly -root $LEC_TOP
-// ensure the module under test is not blackboxed
-add notranslate filepathnames $LEC_DIR/$LEC_TOP.*
-del notranslate filepathnames $LEC_DIR/$LEC_TOP.*
-
-// read golden design
-read design -golden -sv12 \
- $LEC_DIR/top_pkg.sv \
- $LEC_DIR/tlul_pkg.sv \
- $LEC_DIR/*_pkg.sv \
- $LEC_DIR/prim_*.sv \
- $LEC_DIR/$LEC_TOP.sv
-
-// read revised design
-read design -revised -verilog \
- $LEC_DIR/prim_*.v \
- $LEC_DIR/$LEC_TOP.v
-
-// force comparison of the desired module
-set root module $LEC_TOP -both
-
-//-----------------------------------------------------------------
+//-------------------------------------------------------------------------
// pre-LEC reports
-//-----------------------------------------------------------------
+//-------------------------------------------------------------------------
+report rule check -verbose
report design data
report black box
report module
-//-----------------------------------------------------------------
+//-------------------------------------------------------------------------
// compare
-//-----------------------------------------------------------------
-set mapping method -noname
+//-------------------------------------------------------------------------
set system mode lec
-set parallel option -threads 4
-analyze datapath -merge -verbose -effort ultra
+
+set mapping method -nets -mem -unreach -noname
+map key points
+report unmapped points
+
add compare point -all
-set compare effort ultra
-compare -threads 4
+compare -threads 8 -noneq_stop 1
analyze abort -compare
-//-----------------------------------------------------------------
+//-------------------------------------------------------------------------
// reports
-//-----------------------------------------------------------------
+//-------------------------------------------------------------------------
report compare data -class nonequivalent -class abort -class notcompared
report verification -verbose
report statistics
diff --git a/util/syn_yosys.sh b/util/syn_yosys.sh
index 3ca23a2..98cbe9e 100755
--- a/util/syn_yosys.sh
+++ b/util/syn_yosys.sh
@@ -10,47 +10,65 @@
# The following tools are required:
# - sv2v: SystemVerilog-to-Verilog converter from github.com/zachjs/sv2v
# - yosys: synthesis tool from github.com/YosysHQ/yosys
+# - Cadence Conformal
#
# Usage:
-# syn_yosys.sh 2>&1 | tee syn.std
+# ./syn_yosys.sh 2>&1 | tee syn.std
#-------------------------------------------------------------------------
# use fusesoc to generate files and file list
#-------------------------------------------------------------------------
-\rm -Rf build
-fusesoc --cores-root .. run --target=syn --setup lowrisc:systems:top_earlgrey
+\rm -Rf build syn_out
+fusesoc --cores-root .. run --target=syn \
+ --setup lowrisc:systems:top_earlgrey > /dev/null 2>&1
# copy all files into directory "syn_out"
-\rm -Rf syn_out
mkdir syn_out
cp \
- build/lowrisc_systems_top_earlgrey_0.1/src/*/*.sv \
- build/lowrisc_systems_top_earlgrey_0.1/src/*/*/*.sv \
- build/lowrisc_systems_top_earlgrey_0.1/src/*/*/*/*.sv \
+ build/*/src/*/*.sv* \
+ build/*/src/*/*/*.sv* \
+ build/*/src/*/*/*/*.sv* \
syn_out
cd syn_out
-# not synthesizable
-\rm prim_pad_wrapper.sv
-\rm prim_generic_pad_wrapper.sv
+# copy file list, remove incdir and pins_if, and flatten pathnames
+grep -Ev 'incdir|pins_if' ../build/*/*/*.scr | sed 's!.*/!!' > flist_gold
-# not used for synthesis
-\rm pins_if.sv
-\rm tlul_assert.sv
-\rm tlul_assert_multiple.sv
-
-# match filename to module name
-mv ibex_register_file{_ff,}.sv
-
-# prim_util_memload.sv is only meant to be included within a module
-mv prim_util_memload.sv{,h}
-sed -i.delete.bak -e "s/prim_util_memload\.sv/prim_util_memload.svh/" *.sv
-rm *.delete.bak # some sed implementations require backup extensions
+# generate revised flist by replacing '.sv' by '.v' and removing packages
+sed 's/.sv/.v/g' flist_gold | grep -v "_pkg.v" > flist_rev
#-------------------------------------------------------------------------
# convert all RTL files to Verilog
#-------------------------------------------------------------------------
-printf "\n\nsv2v:\n"
+
+# hack SystemVerilog files to avoid SV2V and/or LEC issues
+# TODO: eventually remove these hacks
+
+# 1) Setting ByteAccess = 0 for tlul_adapter_sram.sv doesn't work. This
+# hack changes the functionality so needs fixing
+sed -i 's/ByteAccess *(0)/ByteAccess(1)/g' *.sv
+
+# 2) Replace "inside" for dm_csrs.sv and dm_mem.sv. This hack changes
+# the functionality so needs fixing
+sed -i 's/) inside/)/g' dm_csrs.sv
+sed -i 's/\[(dm::Data0):DataEnd\]:/dm::Data0:/g' dm_csrs.sv
+sed -i 's/\[(dm::ProgBuf0):ProgBufEnd\]:/dm::ProgBuf0:/g' dm_csrs.sv
+sed -i 's/inside//g' dm_mem.sv
+sed -i 's/\[(dm::DataAddr):DataEndAddr\]:/dm::DataAddr:/' dm_mem.sv
+sed -i 's/\[DataBaseAddr:DataEndAddr\]:/DataBaseAddr:/' dm_mem.sv
+sed -i 's/\[ProgBufBaseAddr:ProgBufEndAddr\]:/ProgBufBaseAddr:/' dm_mem.sv
+sed -i 's/\[AbstractCmdBaseAddr:AbstractCmdEndAddr\]:/AbstractCmdBaseAddr:/' dm_mem.sv
+sed -i 's/\[FlagsBaseAddr:FlagsEndAddr\]:/FlagsBaseAddr:/' dm_mem.sv
+
+printf "\nSV2V VERSION:\n"
+sv2v --version
+
+printf "\nSV2V ERRORS:\n"
+
+# prim_util_memload.sv is only meant to be included within a module
+mv prim_util_memload.sv{,h}
+sed -i "s/prim_util_memload\.sv/prim_util_memload.svh/" *.sv
+
sv2v -DSYNTHESIS *.sv > combined.v
# split files up
modules=`cat combined.v | grep "^module" | sed -e "s/^module //" | sed -e "s/ (//"`
@@ -60,14 +78,54 @@
done
rm combined.v
+# rename ibex_register_file_ff, match filename to module name
+mv ibex_register_file{,_ff}.v
+
+# remove *pkg.v files (they are empty files and not needed for Verilog)
+rm -Rf *_pkg.v
+
#-------------------------------------------------------------------------
# run LEC (generarted Verilog vs. original SystemVerilog)
#-------------------------------------------------------------------------
printf "\n\nLEC RESULTS:\n"
-cd ../../hw/formal
-for file in ../../util/syn_out/*.v; do
- module=`basename -s .v $file`
- ./lec_sv2v ../../util/syn_out $module > /dev/null 2>&1
+
+# top_earlgrey and all its submodules
+declare -a modules=(
+ "rv_dm"
+ "spi_device"
+ "usbdev"
+ "flash_ctrl"
+ "tlul_adapter_sram"
+ "prim_rom_adv"
+ "prim_ram_1p_adv"
+ "uart"
+ "gpio"
+ "aes"
+ "hmac"
+ "pinmux"
+ "padctrl"
+ "alert_handler"
+ "pwrmgr"
+ "rstmgr"
+ "clkmgr"
+ "nmi_gen"
+ "rv_timer"
+ "rv_plic"
+ "rv_core_ibex"
+ "xbar_main"
+ "xbar_peri"
+ "flash_phy"
+ "top_earlgrey"
+)
+
+for module in "${modules[@]}"; do
+ export LEC_TOP="$module"
+
+ # run Conformal LEC
+ lec -xl -nogui -nobanner \
+ -dofile ../../hw/formal/lec_sv2v.do \
+ -logfile lec_${module}.log \
+ <<< "exit -force" > /dev/null 2>&1
# summarize results
result=`grep "Compare Results" lec_${module}.log 2>&1`
@@ -76,21 +134,20 @@
else
result=`echo $result | awk '{ print $4 }'`
fi
- printf "%-35s %s\n" $module $result
+ printf "%-25s %s\n" $module $result
done
-cd -
#-------------------------------------------------------------------------
# run yosys
#-------------------------------------------------------------------------
printf "\n\nYosys:\n"
yosys -QTqp "
-read_verilog *.v;
-hierarchy -check -top top_earlgrey;
-synth_xilinx;
-write_blif out.blif;
-write_edif out.edif;
-write_json out.json;
+ read_verilog *.v;
+ hierarchy -check -top top_earlgrey;
+ synth_xilinx;
+ write_blif out.blif;
+ write_edif out.edif;
+ write_json out.json;
"
# TODOs:
