[chip,formal] Add AST mem cfg to conn csv

This commit enables splitting of CSVs by area so that it can be more cleanly maintained. In addition, the AST mem cfg signals are added to its own csv file. Signed-off-by: Srikrishna Iyer <[email protected]>
antmicro · Oct 19, 2021 · edc8093 · edc8093
1 parent 7e18769
commit edc8093
Show file tree

Hide file tree

Showing 8 changed files with 113 additions and 28 deletions.
diff --git a/hw/formal/tools/dvsim/common_conn_cfg.hjson b/hw/formal/tools/dvsim/common_conn_cfg.hjson
@@ -8,7 +8,7 @@
 
   // Vars that need to exported to the env
   exports: [
-    {CSV_PATH: "{csv_path}"}
+    {CONN_CSVS: "'{conn_csvs}'"}
   ]
 
   overrides: [

diff --git a/hw/formal/tools/jaspergold/conn.tcl b/hw/formal/tools/jaspergold/conn.tcl
@@ -11,6 +11,13 @@ if {$env(COV) == 1} {
   check_cov -init -model {branch statement functional} \
   -enable_prove_based_proof_core
 }
+
+set conn_csvs [regexp -all -inline {\S+} $env(CONN_CSVS)]
+if {$conn_csvs eq ""} {
+  puts "ERROR: CONN_CSVS environment variable is empty."
+  quit
+}
+
 #-------------------------------------------------------------------------
 # read design
 #-------------------------------------------------------------------------
@@ -20,12 +27,14 @@ if {$env(COV) == 1} {
 analyze -sv09     \
   +define+FPV_ON  \
   -f [glob *.scr] \
-  -bbox_m ast     \
-  -bbox_m ast_dft
+  -bbox_m aon_osc \
+  -bbox_m io_osc  \
+  -bbox_m sys_osc \
+  -bbox_m usb_osc
 
 # Black-box assistant will blackbox the modules which are not needed by looking at
 # the connectivity csv.
-blackbox_assistant -config -connectivity_Map $env(CSV_PATH)
+blackbox_assistant -config -connectivity_map $conn_csvs
 
 # This is jg work-around when black-boxing with inout ports
 set_port_direction_handling coercion_weak_bbox
@@ -48,13 +57,15 @@ if {$env(DUT_TOP) == "chip_earlgrey_asic"} {
 # configure proofgrid
 #-------------------------------------------------------------------------
 set_proofgrid_mode local
-set_proofgrid_per_engine_max_local_jobs 2
+set_proofgrid_per_engine_max_local_jobs 16
 
 # Uncomment below 2 lines when using LSF:
 # set_proofgrid_mode lsf
 # set_proofgrid_per_engine_max_jobs 16
 
-check_conn -load $env(CSV_PATH)
+foreach i $conn_csvs {
+  check_conn -load $i
+}
 
 #-------------------------------------------------------------------------
 # prove all assertions & report

diff --git a/hw/top_earlgrey/formal/chip_conn_cfg.hjson b/hw/top_earlgrey/formal/chip_conn_cfg.hjson
@@ -9,7 +9,12 @@
 
   fusesoc_core: lowrisc:systems:chip_earlgrey_asic:0.1
 
-  csv_path: "{proj_root}/hw/top_earlgrey/formal/conn_csvs/top_earlgrey_conn.csv"
+  conn_csvs_dir: "{proj_root}/hw/top_earlgrey/formal/conn_csvs"
+  conn_csvs: ["{conn_csvs_dir}/clkmgr_idle.csv",
+              "{conn_csvs_dir}/clkmgr_peri.csv",
+              "{conn_csvs_dir}/clkmgr_trans.csv",
+              "{conn_csvs_dir}/pwrmgr_rstmgr.csv",
+              "{conn_csvs_dir}/ast_mem_cfg.csv"]
 
   // TODO: reduce run time and turn on coverage
   cov: false

diff --git a/hw/top_earlgrey/formal/conn_csvs/ast_mem_cfg.csv b/hw/top_earlgrey/formal/conn_csvs/ast_mem_cfg.csv
@@ -0,0 +1,43 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+#
+# Run these checks with:
+#  ./util/dvsim/dvsim.py hw/top_earlgrey/formal/chip_conn_cfg.hjson
+
+,NAME,SRC BLOCK,SRC SIGNAL,DEST BLOCK,DEST SIGNAL,,,,,,
+
+# AST DFT module emits some configuration bits for single and dual port memories in the chip. These
+# cannot be covered functionally in the open source repo, since they are not used by the generic
+# memory models. TThese signals are excluded from coverage collection AFTER they have been added to
+# this checker.
+#
+#  The source path (within AST) is inferred manually from the RTL. The destination paths are
+#  obtained by running a basic chip level simulation with the plusarg "+show_mem_paths=1".
+
+# Dual port RAMs.
+# To spi_device.
+CONNECTION,AST_DFT_SPI_DEVICE_RAM_2P_CFG,u_ast.u_ast_dft,"{dpram_rmf_o, dpram_rml_o}",top_earlgrey.u_spi_device.u_memory_2p.u_mem.gen_generic.u_impl_generic,cfg_i
+
+# To usbdev.
+CONNECTION,AST_DFT_USBDEV_RAM_2P_CFG,u_ast.u_ast_dft,"{dpram_rmf_o, dpram_rml_o}",top_earlgrey.u_usbdev.u_memory_2p.u_mem.gen_generic.u_impl_generic,cfg_i
+
+# Single port RAMs.
+# To otbn.
+CONNECTION,AST_DFT_OTBN_IMEM_RAM_1P_CFG,u_ast.u_ast_dft,"{spram_rm_o, sprgf_rm_o}",top_earlgrey.u_otbn.u_imem.u_prim_ram_1p_adv.u_mem.gen_generic.u_impl_generic,cfg_i
+CONNECTION,AST_DFT_OTBN_DMEM_RAM_1P_CFG,u_ast.u_ast_dft,"{spram_rm_o, sprgf_rm_o}",top_earlgrey.u_otbn.u_dmem.u_prim_ram_1p_adv.u_mem.gen_generic.u_impl_generic,cfg_i
+
+# To rv_core_ibex.
+CONNECTION,AST_DFT_RV_CORE_IBEX_TAG0_RAM_1P_CFG,u_ast.u_ast_dft,"{spram_rm_o, sprgf_rm_o}",top_earlgrey.u_rv_core_ibex.u_core.gen_rams.gen_rams_inner[0].tag_bank.gen_generic.u_impl_generic,cfg_i
+CONNECTION,AST_DFT_RV_CORE_IBEX_TAG1_RAM_1P_CFG,u_ast.u_ast_dft,"{spram_rm_o, sprgf_rm_o}",top_earlgrey.u_rv_core_ibex.u_core.gen_rams.gen_rams_inner[1].tag_bank.gen_generic.u_impl_generic,cfg_i
+CONNECTION,AST_DFT_RV_CORE_IBEX_DATA0_RAM_1P_CFG,u_ast.u_ast_dft,"{spram_rm_o, sprgf_rm_o}",top_earlgrey.u_rv_core_ibex.u_core.gen_rams.gen_rams_inner[0].data_bank.gen_generic.u_impl_generic,cfg_i
+CONNECTION,AST_DFT_RV_CORE_IBEX_DATA1_RAM_1P_CFG,u_ast.u_ast_dft,"{spram_rm_o, sprgf_rm_o}",top_earlgrey.u_rv_core_ibex.u_core.gen_rams.gen_rams_inner[1].data_bank.gen_generic.u_impl_generic,cfg_i
+
+# To sram_ctrl (main).
+CONNECTION,AST_DFT_SRAM_MAIN_RAM_1P_CFG,u_ast.u_ast_dft,"{spram_rm_o, sprgf_rm_o}",top_earlgrey.u_sram_ctrl_main.u_prim_ram_1p_scr.u_prim_ram_1p_adv.u_mem.gen_generic.u_impl_generic,cfg_i
+
+# To sram_ctrl (ret).
+CONNECTION,AST_DFT_SRAM_RET_RAM_1P_CFG,u_ast.u_ast_dft,"{spram_rm_o, sprgf_rm_o}",top_earlgrey.u_sram_ctrl_ret_aon.u_prim_ram_1p_scr.u_prim_ram_1p_adv.u_mem.gen_generic.u_impl_generic,cfg_i
+
+# To rom.
+CONNECTION,AST_DFT_ROM_CFG,u_ast.u_ast_dft,sprom_rm_o,top_earlgrey.u_rom_ctrl.gen_rom_scramble_enabled.u_rom.u_rom.u_prim_rom.gen_generic.u_impl_generic,cfg_i
diff --git a/hw/top_earlgrey/formal/conn_csvs/clkmgr_idle.csv b/hw/top_earlgrey/formal/conn_csvs/clkmgr_idle.csv
@@ -0,0 +1,14 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+#
+# Run these checks with:
+#  ./util/dvsim/dvsim.py hw/top_earlgrey/formal/chip_conn_cfg.hjson
+
+,NAME,SRC BLOCK,SRC SIGNAL,DEST BLOCK,DEST SIGNAL,,,,,,
+
+# clkmgr idle connectivity
+CONNECTION,CLKMGR_IDLE0,top_earlgrey.u_clkmgr_aon,idle_i[0],top_earlgrey.u_aes,idle_o
+CONNECTION,CLKMGR_IDLE1,top_earlgrey.u_clkmgr_aon,idle_i[1],top_earlgrey.u_hmac,idle_o
+CONNECTION,CLKMGR_IDLE2,top_earlgrey.u_clkmgr_aon,idle_i[2],top_earlgrey.u_kmac,idle_o
+CONNECTION,CLKMGR_IDLE3,top_earlgrey.u_clkmgr_aon,idle_i[3],top_earlgrey.u_otbn,idle_o
diff --git a/...ey/formal/conn_csvs/top_earlgrey_conn.csv → ...earlgrey/formal/conn_csvs/clkmgr_peri.csv b/...ey/formal/conn_csvs/top_earlgrey_conn.csv → ...earlgrey/formal/conn_csvs/clkmgr_peri.csv
@@ -2,17 +2,11 @@
 # Licensed under the Apache License, Version 2.0, see LICENSE for details.
 # SPDX-License-Identifier: Apache-2.0
 #
-# Run these checks with
-#  cd hw/top_earlgrey/formal
-#  ../../../util/dvsim/dvsim.py chip_conn_cfg.hjson
+# Run these checks with:
+#  ./util/dvsim/dvsim.py hw/top_earlgrey/formal/chip_conn_cfg.hjson
 
 ,NAME,SRC BLOCK,SRC SIGNAL,DEST BLOCK,DEST SIGNAL,,,,,,
 
-# clkmgr idle connectivity
-CONNECTION,CLKMGR_IDLE0,top_earlgrey.u_clkmgr_aon,idle_i[0],top_earlgrey.u_aes,idle_o
-CONNECTION,CLKMGR_IDLE1,top_earlgrey.u_clkmgr_aon,idle_i[1],top_earlgrey.u_hmac,idle_o
-CONNECTION,CLKMGR_IDLE2,top_earlgrey.u_clkmgr_aon,idle_i[2],top_earlgrey.u_kmac,idle_o
-CONNECTION,CLKMGR_IDLE3,top_earlgrey.u_clkmgr_aon,idle_i[3],top_earlgrey.u_otbn,idle_o
 # clkmgr peri clock connectivity
 CONNECTION,CLKMGR_PERI_CLK0_GPIO,top_earlgrey.u_clkmgr_aon,clocks_o.clk_io_div4_peri,top_earlgrey.u_gpio,clk_i
 CONNECTION,CLKMGR_PERI_CLK0_SPI_DEVICE,top_earlgrey.u_clkmgr_aon,clocks_o.clk_io_div4_peri,top_earlgrey.u_spi_device,clk_i
@@ -32,16 +26,3 @@ CONNECTION,CLKMGR_PERI_CLK1_SPI_DEVICE,top_earlgrey.u_clkmgr_aon,clocks_o.clk_io
 CONNECTION,CLKMGR_PERI_CLK1_SPI_HOST0,top_earlgrey.u_clkmgr_aon,clocks_o.clk_io_peri,top_earlgrey.u_spi_host0,clk_core_i
 CONNECTION,CLKMGR_PERI_CLK1_SPI_HOST1,top_earlgrey.u_clkmgr_aon,clocks_o.clk_io_div2_peri,top_earlgrey.u_spi_host1,clk_core_i
 CONNECTION,CLKMGR_PERI_CLK2_USBDEV,top_earlgrey.u_clkmgr_aon,clocks_o.clk_usb_peri,top_earlgrey.u_usbdev,clk_usb_48mhz_i
-# clkmgr trans clock connectivity
-CONNECTION,CLKMGR_AES,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_aes,top_earlgrey.u_aes,clk_i
-CONNECTION,CLKMGR_AES_EDN,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_aes,top_earlgrey.u_aes,clk_edn_i
-CONNECTION,CLKMGR_HMAC,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_hmac,top_earlgrey.u_hmac,clk_i
-CONNECTION,CLKMGR_KMAC,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_kmac,top_earlgrey.u_kmac,clk_i
-CONNECTION,CLKMGR_KMAC_EDN,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_kmac,top_earlgrey.u_kmac,clk_edn_i
-CONNECTION,CLKMGR_OTBN,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_otbn,top_earlgrey.u_otbn,clk_i
-CONNECTION,CLKMGR_OTBN_EDN,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_otbn,top_earlgrey.u_otbn,clk_edn_i
-# pwrmgr rstmgr connections
-CONNECTION,CLKMGR_RST_LC_REQ,top_earlgrey.u_pwrmgr_aon,pwr_rst_o.rst_lc_req,top_earlgrey.u_rstmgr_aon,pwr_i.rst_lc_req
-CONNECTION,CLKMGR_RST_SYS_REQ,top_earlgrey.u_pwrmgr_aon,pwr_rst_o.rst_sys_req,top_earlgrey.u_rstmgr_aon,pwr_i.rst_sys_req
-CONNECTION,CLKMGR_RST_LC_SRC_N,top_earlgrey.u_pwrmgr_aon,pwr_rst_i.rst_lc_src_n,top_earlgrey.u_rstmgr_aon,pwr_o.rst_lc_src_n
-CONNECTION,CLKMGR_RST_SYS_SRC_N,top_earlgrey.u_pwrmgr_aon,pwr_rst_i.rst_sys_src_n,top_earlgrey.u_rstmgr_aon,pwr_o.rst_sys_src_n
diff --git a/hw/top_earlgrey/formal/conn_csvs/clkmgr_trans.csv b/hw/top_earlgrey/formal/conn_csvs/clkmgr_trans.csv
@@ -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
+#
+# Run these checks with:
+#  ./util/dvsim/dvsim.py hw/top_earlgrey/formal/chip_conn_cfg.hjson
+
+,NAME,SRC BLOCK,SRC SIGNAL,DEST BLOCK,DEST SIGNAL,,,,,,
+
+# clkmgr trans clock connectivity
+CONNECTION,CLKMGR_AES,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_aes,top_earlgrey.u_aes,clk_i
+CONNECTION,CLKMGR_AES_EDN,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_aes,top_earlgrey.u_aes,clk_edn_i
+CONNECTION,CLKMGR_HMAC,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_hmac,top_earlgrey.u_hmac,clk_i
+CONNECTION,CLKMGR_KMAC,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_kmac,top_earlgrey.u_kmac,clk_i
+CONNECTION,CLKMGR_KMAC_EDN,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_kmac,top_earlgrey.u_kmac,clk_edn_i
+CONNECTION,CLKMGR_OTBN,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_otbn,top_earlgrey.u_otbn,clk_i
+CONNECTION,CLKMGR_OTBN_EDN,top_earlgrey.u_clkmgr_aon,clocks_o.clk_main_otbn,top_earlgrey.u_otbn,clk_edn_i
diff --git a/hw/top_earlgrey/formal/conn_csvs/pwrmgr_rstmgr.csv b/hw/top_earlgrey/formal/conn_csvs/pwrmgr_rstmgr.csv
@@ -0,0 +1,14 @@
+# Copyright lowRISC contributors.
+# Licensed under the Apache License, Version 2.0, see LICENSE for details.
+# SPDX-License-Identifier: Apache-2.0
+#
+# Run these checks with:
+#  ./util/dvsim/dvsim.py hw/top_earlgrey/formal/chip_conn_cfg.hjson
+
+,NAME,SRC BLOCK,SRC SIGNAL,DEST BLOCK,DEST SIGNAL,,,,,,
+
+# pwrmgr rstmgr connections
+CONNECTION,CLKMGR_RST_LC_REQ,top_earlgrey.u_pwrmgr_aon,pwr_rst_o.rst_lc_req,top_earlgrey.u_rstmgr_aon,pwr_i.rst_lc_req
+CONNECTION,CLKMGR_RST_SYS_REQ,top_earlgrey.u_pwrmgr_aon,pwr_rst_o.rst_sys_req,top_earlgrey.u_rstmgr_aon,pwr_i.rst_sys_req
+CONNECTION,CLKMGR_RST_LC_SRC_N,top_earlgrey.u_pwrmgr_aon,pwr_rst_i.rst_lc_src_n,top_earlgrey.u_rstmgr_aon,pwr_o.rst_lc_src_n
+CONNECTION,CLKMGR_RST_SYS_SRC_N,top_earlgrey.u_pwrmgr_aon,pwr_rst_i.rst_sys_src_n,top_earlgrey.u_rstmgr_aon,pwr_o.rst_sys_src_n