[fpv] Add formal target to alert related FPV testbench

This PR adds a formal target to the alert_handler related FPV testbench and their templates. Signed-off-by: Cindy Chen <chencindy@opentitan.org>
antmicro · Oct 19, 2021 · c9887c2 · c9887c2
1 parent 7a0e654
commit c9887c2
Show file tree

Hide file tree

Showing 5 changed files with 48 additions and 12 deletions.
diff --git a/hw/ip_templates/alert_handler/fpv/alert_handler_esc_timer_fpv.core.tpl b/hw/ip_templates/alert_handler/fpv/alert_handler_esc_timer_fpv.core.tpl
@@ -5,7 +5,7 @@ CAPI=2:
 name: ${instance_vlnv("lowrisc:fpv:alert_handler_esc_timer_fpv:0.1")}
 description: "alert_handler_esc_timer FPV target"
 filesets:
-  files_fpv:
+  files_formal:
     depend:
       - lowrisc:prim:all
       - ${instance_vlnv("lowrisc:ip:alert_handler")}
@@ -16,10 +16,16 @@ filesets:
     file_type: systemVerilogSource
 
 targets:
-  default:
+  default: &default_target
     # note, this setting is just used
     # to generate a file list for jg
     default_tool: icarus
     filesets:
-      - files_fpv
+      - files_formal
     toplevel: alert_handler_esc_timer_tb
+
+  formal:
+    <<: *default_target
+
+  lint:
+    <<: *default_target
diff --git a/hw/ip_templates/alert_handler/fpv/alert_handler_ping_timer_fpv.core.tpl b/hw/ip_templates/alert_handler/fpv/alert_handler_ping_timer_fpv.core.tpl
@@ -5,7 +5,7 @@ CAPI=2:
 name: ${instance_vlnv("lowrisc:fpv:alert_handler_ping_timer_fpv:0.1")}
 description: "ALERT_HANDLER FPV target"
 filesets:
-  files_fpv:
+  files_formal:
     depend:
       - lowrisc:prim:all
       - ${instance_vlnv("lowrisc:ip:alert_handler")}
@@ -16,10 +16,16 @@ filesets:
     file_type: systemVerilogSource
 
 targets:
-  default:
+  default: &default_target
     # note, this setting is just used
     # to generate a file list for jg
     default_tool: icarus
     filesets:
-      - files_fpv
+      - files_formal
     toplevel: alert_handler_ping_timer_tb
+
+  formal:
+    <<: *default_target
+
+  lint:
+    <<: *default_target
diff --git a/hw/top_earlgrey/ip_autogen/alert_handler/fpv/alert_handler_esc_timer_fpv.core b/hw/top_earlgrey/ip_autogen/alert_handler/fpv/alert_handler_esc_timer_fpv.core
@@ -5,7 +5,7 @@ CAPI=2:
 name: lowrisc:opentitan:top_earlgrey_alert_handler_esc_timer_fpv:0.1
 description: "alert_handler_esc_timer FPV target"
 filesets:
-  files_fpv:
+  files_formal:
     depend:
       - lowrisc:prim:all
       - lowrisc:opentitan:top_earlgrey_alert_handler
@@ -16,10 +16,16 @@ filesets:
     file_type: systemVerilogSource
 
 targets:
-  default:
+  default: &default_target
     # note, this setting is just used
     # to generate a file list for jg
     default_tool: icarus
     filesets:
-      - files_fpv
+      - files_formal
     toplevel: alert_handler_esc_timer_tb
+
+  formal:
+    <<: *default_target
+
+  lint:
+    <<: *default_target
diff --git a/hw/top_earlgrey/ip_autogen/alert_handler/fpv/alert_handler_ping_timer_fpv.core b/hw/top_earlgrey/ip_autogen/alert_handler/fpv/alert_handler_ping_timer_fpv.core
@@ -5,7 +5,7 @@ CAPI=2:
 name: lowrisc:opentitan:top_earlgrey_alert_handler_ping_timer_fpv:0.1
 description: "ALERT_HANDLER FPV target"
 filesets:
-  files_fpv:
+  files_formal:
     depend:
       - lowrisc:prim:all
       - lowrisc:opentitan:top_earlgrey_alert_handler
@@ -16,10 +16,16 @@ filesets:
     file_type: systemVerilogSource
 
 targets:
-  default:
+  default: &default_target
     # note, this setting is just used
     # to generate a file list for jg
     default_tool: icarus
     filesets:
-      - files_fpv
+      - files_formal
     toplevel: alert_handler_ping_timer_tb
+
+  formal:
+    <<: *default_target
+
+  lint:
+    <<: *default_target
diff --git a/hw/top_earlgrey/lint/top_earlgrey_fpv_lint_cfgs.hjson b/hw/top_earlgrey/lint/top_earlgrey_fpv_lint_cfgs.hjson
@@ -18,6 +18,18 @@
   rel_path: "hw/top_earlgrey/fpv/lint/{tool}"
 
   use_cfgs: [{
+              name: alert_handler_esc_timer_fpv
+              fusesoc_core: lowrisc:opentitan:top_earlgrey_alert_handler_esc_timer_fpv
+              import_cfgs: ["{proj_root}/hw/lint/tools/dvsim/common_lint_cfg.hjson"]
+              rel_path: "hw/ip/alert_handler/alert_handler_esc_timer_fpv/lint/{tool}"
+             }
+             {
+              name: alert_handler_ping_timer_fpv
+              fusesoc_core: lowrisc:opentitan:top_earlgrey_alert_handler_ping_timer_fpv
+              import_cfgs: ["{proj_root}/hw/lint/tools/dvsim/common_lint_cfg.hjson"]
+              rel_path: "hw/ip/alert_handler/alert_handler_ping_timer_fpv/lint/{tool}"
+             }
+            {
                name: prim_arbiter_ppc_fpv
                fusesoc_core: lowrisc:fpv:prim_arbiter_ppc_fpv
                import_cfgs: ["{proj_root}/hw/lint/tools/dvsim/common_lint_cfg.hjson"]