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: