FPV bench setup for br_cdc_stable_data

cdc/fpv/BUILD.bazel

@@ -602,3 +602,97 @@ br_verilog_fpv_test_tools_suite(
         "//mux/rtl:br_mux_bin_structured_gates_mock",
     ],
 )
+
+verilog_library(
+    name = "br_cdc_reg_fpv_monitor",
+    srcs = ["br_cdc_reg_fpv_monitor.sv"],
+    visibility = ["//visibility:public"],
+    deps = [
+        "//cdc/rtl:br_cdc_reg",
+        "//macros:br_asserts",
+        "//macros:br_registers",
+    ],
+)
+
+verilog_elab_test(
+    name = "br_cdc_reg_fpv_monitor_elab_test",
+    custom_tcl_header = "//:elab_test_jg_custom_header.verific.tcl",
+    tool = "verific",
+    deps = [":br_cdc_reg_fpv_monitor"],
+)
+
+br_verilog_fpv_test_tools_suite(
+    name = "br_cdc_reg_test_suite",
+    params = {
+        "Width": [
+            "2",
+        ],
+        "RegisterPopOutputs": [
+            "0",
+            "1",
+        ],
+        "RegisterResetActive": [
+            "0",
+            "1",
+        ],
+        "NumSyncStages": [
+            "2",
+            "3",
+        ],
+    },
+    tools = {
+        "jg": "br_cdc_reg_fpv.jg.tcl",
+    },
+    top = "br_cdc_reg_fpv_monitor",
+    deps = [
+        ":br_cdc_reg_fpv_monitor",
+        "//gate/rtl:br_gate_mock",
+    ],
+)
+
+verilog_library(
+    name = "br_cdc_stable_data_fpv_monitor",
+    srcs = ["br_cdc_stable_data_fpv_monitor.sv"],
+    visibility = ["//visibility:public"],
+    deps = [
+        "//cdc/rtl:br_cdc_stable_data",
+        "//macros:br_asserts",
+        "//macros:br_registers",
+    ],
+)
+
+verilog_elab_test(
+    name = "br_cdc_stable_data_fpv_monitor_elab_test",
+    custom_tcl_header = "//:elab_test_jg_custom_header.verific.tcl",
+    tool = "verific",
+    deps = [":br_cdc_stable_data_fpv_monitor"],
+)
+
+br_verilog_fpv_test_tools_suite(
+    name = "br_cdc_stable_data_test_suite",
+    params = {
+        "Width": [
+            "2",
+        ],
+        "InitValue": [
+            "0",
+            "1",
+        ],
+        "RegisterResetActive": [
+            "0",
+            "1",
+        ],
+        "NumSyncStages": [
+            "2",
+            "3",
+        ],
+    },
+    tools = {
+        "jg": "br_cdc_stable_data_fpv.jg.tcl",
+    },
+    top = "br_cdc_stable_data_fpv_monitor",
+    deps = [
+        ":br_cdc_stable_data_fpv_monitor",
+        "//gate/rtl:br_gate_mock",
+    ],
+)

cdc/fpv/br_cdc_reg_fpv.jg.tcl

@@ -0,0 +1,39 @@
+# SPDX-License-Identifier: Apache-2.0
+
+
+# clock/reset set up
+clock clk
+clock push_clk -from 1 -to 10 -both_edges
+clock pop_clk -from 1 -to 10 -both_edges
+
+# declare always_in system clock
+reset -none
+assume -reset -name set_rst_during_reset {rst}
+assume -bound 1 -name delay_rst {rst}
+assume -name deassert_rst {##1 !rst}
+# reset are ready at different times
+assume -env {rst |-> push_rst}
+assume -env {rst |-> pop_rst}
+assume -env {!push_rst |=> !push_rst}
+assume -env {!pop_rst |=> !pop_rst}
+assume -env {s_eventually !push_rst}
+assume -env {s_eventually !pop_rst}
+
+# push/pop side primary input signals only toggle w.r.t its clock
+clock -rate {push_valid push_data push_rst} push_clk
+clock -rate {pop_ready pop_rst} pop_clk
+
+get_design_info
+
+# primary input control signal should be legal during reset
+assume -name no_push_valid_during_reset {@(posedge push_clk) \
+push_rst |-> push_valid == 'd0}
+
+# primary output control signal should be legal during reset
+#assert -name fv_rst_check_pop_valid {@(posedge pop_clk) \
+#pop_rst |-> pop_valid == 'd0}
+
+# limit run time to 10-mins
+set_prove_time_limit 600s
+
+prove -all

cdc/fpv/br_cdc_reg_fpv_monitor.sv

@@ -0,0 +1,115 @@
+// SPDX-License-Identifier: Apache-2.0
+
+// FPV monitor for br_cdc_reg
+
+`include "br_asserts.svh"
+
+module br_cdc_reg_fpv_monitor #(
+    parameter int Width = 1,  // Must be at least 1
+    parameter bit RegisterPopOutputs = 0,
+    parameter bit RegisterResetActive = 1,
+    parameter int NumSyncStages = 3,
+    parameter bit EnableCoverPushBackpressure = 1,
+    parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
+    parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability,
+    // If 1 use Jasper scoreboard, else use Synopsys FML scoreboard
+    parameter bit Jasper = 1
+) (
+
+    // FV system clk and rst
+    input logic clk,
+    input logic rst,
+
+    // Push-side interface.
+    input logic             push_clk,
+    input logic             push_rst,
+    input logic             push_valid,
+    input logic [Width-1:0] push_data,
+
+    // Pop-side interface.
+    input logic pop_clk,
+    input logic pop_rst,
+    input logic pop_ready
+);
+  // ----------Instantiate DUT----------
+  logic push_ready;
+  logic pop_valid;
+  logic [Width-1:0] pop_data;
+
+  br_cdc_reg #(
+      .Width(Width),
+      .RegisterPopOutputs(RegisterPopOutputs),
+      .RegisterResetActive(RegisterResetActive),
+      .NumSyncStages(NumSyncStages),
+      .EnableCoverPushBackpressure(EnableCoverPushBackpressure),
+      .EnableAssertPushValidStability(EnableAssertPushValidStability),
+      .EnableAssertPushDataStability(EnableAssertPushDataStability)
+  ) dut (
+      .push_clk,
+      .push_rst,
+      .push_valid,
+      .push_data,
+      .pop_clk,
+      .pop_rst,
+      .pop_ready,
+      .pop_valid,
+      .pop_data
+  );
+
+  // ----------Assumptions----------
+  if (!EnableCoverPushBackpressure) begin : gen_backpressure
+    `BR_ASSUME(no_backpressure_a, !push_ready |-> !push_valid)
+  end
+  if (EnableAssertPushValidStability) begin : gen_push_valid_stable
+    `BR_ASSUME(push_valid_stable_a, push_valid && !push_ready |=> push_valid)
+  end
+  if (EnableAssertPushDataStability) begin : gen_push_data_stable
+    `BR_ASSUME(push_data_stable_a, push_valid && !push_ready |=> $stable(push_data))
+  end
+
+  // ----------Data integrity Check----------
+  logic push_beat;
+  logic pop_beat;
+
+  assign push_beat = push_valid && push_ready;
+  assign pop_beat  = pop_valid && pop_ready;
+
+  if (Jasper) begin : gen_jasper
+    jasper_scoreboard_3 #(
+        .CHUNK_WIDTH(Width),
+        .IN_CHUNKS(1),
+        .OUT_CHUNKS(1),
+        .SINGLE_CLOCK(0),
+        .MAX_PENDING(1 + RegisterPopOutputs)
+    ) scoreboard (
+        .incoming_clk(push_clk),
+        .outgoing_clk(pop_clk),
+        .rstN(!rst),
+        .incoming_vld(push_beat),
+        .incoming_data(push_data),
+        .outgoing_vld(pop_beat),
+        .outgoing_data(pop_data)
+    );
+  end else begin : gen_snps
+    snps_fml_scoreboard #(
+        .DATA_CHUNK_WIDTH(Width),
+        .NUM_OF_IN_CHUNKS(1),
+        .NUM_OF_OUT_CHUNKS(1),
+        .MAX_OUTSTANDING_CHUNKS(1 + RegisterPopOutputs),
+        .ENABLE_INORDER(1),
+        .ENABLE_DUAL_CLOCKS(1),
+        .SCBMODE(0)
+    ) scoreboard (
+        .Resetn(!rst),
+        .ClkIn(push_clk),
+        .ValidIn(push_beat),
+        .DataIn(push_data),
+        .ClkOut(pop_clk),
+        .ValidOut(pop_beat),
+        .DataOut(pop_data)
+    );
+  end
+
+  // ----------Forward Progress Check----------
+  `BR_ASSERT(no_deadlock_pop_a, push_beat |-> s_eventually pop_valid)
+endmodule : br_cdc_reg_fpv_monitor

cdc/fpv/br_cdc_stable_data_fpv.jg.tcl

@@ -0,0 +1,35 @@
+# SPDX-License-Identifier: Apache-2.0
+
+
+# clock/reset set up
+clock clk
+clock src_clk -from 1 -to 10 -both_edges
+clock dst_clk -from 1 -to 10 -both_edges
+
+# declare always_in system clock
+reset -none
+assume -reset -name set_rst_during_reset {rst}
+assume -bound 1 -name delay_rst {rst}
+assume -name deassert_rst {##1 !rst}
+# reset are ready at different times
+assume -env {rst |-> src_rst}
+assume -env {rst |-> dst_rst}
+assume -env {!src_rst |=> !src_rst}
+assume -env {!dst_rst |=> !dst_rst}
+assume -env {s_eventually !src_rst}
+assume -env {s_eventually !dst_rst}
+
+# push/pop side primary input signals only toggle w.r.t its clock
+clock -rate {src_valid src_data src_rst} src_clk
+clock -rate {dst_rst} dst_clk
+
+get_design_info
+
+# primary input control signal should be legal during reset
+assume -name no_src_valid_during_reset {@(posedge src_clk) \
+src_rst |-> src_valid == 'd0}
+
+# limit run time to 10-mins
+set_prove_time_limit 600s
+
+prove -all

cdc/fpv/br_cdc_stable_data_fpv_monitor.sv

@@ -0,0 +1,74 @@
+`include "br_asserts.svh"
+`include "br_registers.svh"
+
+module br_cdc_stable_data_fpv_monitor #(
+    parameter int Width = 1,
+    parameter logic [Width-1:0] InitValue = '0,
+    parameter bit EnableRegisterResetActive = 1,
+    parameter int NumSyncStages = 3
+) (
+    // FV system clk and rst
+    input logic clk,
+    input logic rst,
+
+    input logic src_clk,
+    input logic src_rst,
+    input logic src_valid,
+    input logic [Width-1:0] src_data,
+
+    input logic dst_clk,
+    input logic dst_rst
+);
+
+  // ----------Instantiate DUT----------
+  logic dst_updated;
+  logic [Width-1:0] dst_data;
+
+  br_cdc_stable_data #(
+      .Width(Width),
+      .InitValue(InitValue),
+      .RegisterResetActive(EnableRegisterResetActive),
+      .NumSyncStages(NumSyncStages)
+  ) dut (
+      .src_clk,
+      .src_rst,
+      .src_valid,
+      .src_data,
+      .dst_clk,
+      .dst_rst,
+      .dst_updated,
+      .dst_data
+  );
+
+  // ----------FV Assumptions----------
+  // Data gets lost if we assert src_valid too frequently.
+  // Pick a relatively large number of cycles to hold between assertions.
+  // TODO(masai): Figure out a better way to determine this value.
+  localparam int MinStableCycles = 100;
+
+  `BR_ASSUME_CR(src_valid_infrequent_a, src_valid |=> !src_valid [* MinStableCycles], src_clk,
+                src_rst)
+  `BR_ASSUME_CR(no_src_valid_during_any_reset_a, (src_rst | dst_rst) |-> !src_valid, src_clk,
+                src_rst)
+
+  // ----------Basic Checks----------
+  `BR_ASSERT_CR(init_value_correct_a, $fell(dst_rst) |-> dst_data == InitValue, dst_clk, dst_rst)
+
+  // ----------Data integrity Check----------
+  jasper_scoreboard_3 #(
+      .CHUNK_WIDTH(Width),
+      .IN_CHUNKS(1),
+      .OUT_CHUNKS(1),
+      .SINGLE_CLOCK(0),
+      .MAX_PENDING(1)
+  ) scoreboard (
+      .incoming_clk(src_clk),
+      .outgoing_clk(dst_clk),
+      .rstN(!rst),
+      .incoming_vld(src_valid),
+      .incoming_data(src_data),
+      .outgoing_vld(dst_updated),
+      .outgoing_data(dst_data)
+  );
+
+endmodule : br_cdc_stable_data_fpv_monitor