commit 0cc1e439b562ab1dffc5ce85ab4ad2a48b4245ee
author Guillermo Maturana <maturana@google.com> Fri Jul 01 11:19:52 2022 -0700
committer Cindy Chen <cindy.chen0316@gmail.com> Fri Jul 01 17:20:06 2022 -0700
tree e047081c0ed7219c8975d69e7415fcfb3e49e4d2
parent 1f7ba3b020414e535637ca066149323d0141ff19

[formal,conn] Add ast to entropy_src connectivity check

Also fix path to usbdev ram.

Fixes #13460

Signed-off-by: Guillermo Maturana <maturana@google.com>

hw/top_earlgrey/formal/chip_conn_cfg.hjson

diff --git a/hw/top_earlgrey/formal/chip_conn_cfg.hjson b/hw/top_earlgrey/formal/chip_conn_cfg.hjson
index 1038cbd..b155268 100644
--- a/hw/top_earlgrey/formal/chip_conn_cfg.hjson
+++ b/hw/top_earlgrey/formal/chip_conn_cfg.hjson
@@ -12,6 +12,7 @@
   bbox_cmd: "[list aon_osc io_osc sys_osc usb_osc]"
   conn_csvs_dir: "{proj_root}/hw/top_earlgrey/formal/conn_csvs"
   conn_csvs: ["{conn_csvs_dir}/aon_timer_rst.csv",
+              "{conn_csvs_dir}/ast_entropy_src_cfg.csv",
               "{conn_csvs_dir}/ast_mem_cfg.csv",
               "{conn_csvs_dir}/clkmgr_ast.csv",
               "{conn_csvs_dir}/clkmgr_idle.csv",

hw/top_earlgrey/formal/conn_csvs/ast_entropy_src_cfg.csv

diff --git a/hw/top_earlgrey/formal/conn_csvs/ast_entropy_src_cfg.csv b/hw/top_earlgrey/formal/conn_csvs/ast_entropy_src_cfg.csv
new file mode 100644
index 0000000..5ddbebd
--- /dev/null
+++ b/hw/top_earlgrey/formal/conn_csvs/ast_entropy_src_cfg.csv
@@ -0,0 +1,12 @@
+# 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 -> entropy_src connectivity
+CONNECTION, AST_ENTROPY_SRC_RNG_VAL, u_ast, rng_val_o, top_earlgrey.u_entropy_src, entropy_src_rng_i.rng_valid
+CONNECTION, AST_ENTROPY_SRC_RNG_B, u_ast, rng_b_o, top_earlgrey.u_entropy_src, entropy_src_rng_i.rng_b

hw/top_earlgrey/formal/conn_csvs/ast_mem_cfg.csv

diff --git a/hw/top_earlgrey/formal/conn_csvs/ast_mem_cfg.csv b/hw/top_earlgrey/formal/conn_csvs/ast_mem_cfg.csv
index 16d40bf..4fe71ea 100644
--- a/hw/top_earlgrey/formal/conn_csvs/ast_mem_cfg.csv
+++ b/hw/top_earlgrey/formal/conn_csvs/ast_mem_cfg.csv
@@ -20,7 +20,7 @@
 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
+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.i_prim_ram_2p_async_adv.u_mem.gen_generic.u_impl_generic, cfg_i
 
 # Single port RAMs.
 # To otbn.