Initial FPV bench setup for br_cdc_reg

cdc/fpv/BUILD.bazel

@@ -602,3 +602,50 @@ 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",
+    ],
+)

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/rtl/BUILD.bazel

@@ -351,3 +351,37 @@ br_verilog_elab_and_lint_test_suite(
         "//gate/rtl:br_gate_mock",
     ],
 )
+
+verilog_library(
+    name = "br_cdc_stable_data_autoupdate",
+    srcs = ["br_cdc_stable_data_autoupdate.sv"],
+    deps = [
+        ":br_cdc_stable_data",
+        "//macros:br_asserts_internal",
+        "//macros:br_registers",
+    ],
+)
+
+br_verilog_elab_and_lint_test_suite(
+    name = "br_cdc_stable_data_autoupdate_test_suite",
+    params = {
+        "Width": ["8"],
+        "InitValue": [
+            "0",
+            "1",
+        ],
+        "RegisterResetActive": [
+            "0",
+            "1",
+        ],
+        "NumSyncStages": [
+            "2",
+            "3",
+        ],
+    },
+    top = "br_cdc_stable_data_autoupdate",
+    deps = [
+        ":br_cdc_stable_data_autoupdate",
+        "//gate/rtl:br_gate_mock",
+    ],
+)

cdc/rtl/br_cdc_stable_data_autoupdate.sv

@@ -0,0 +1,72 @@
+// SPDX-License-Identifier: Apache-2.0
+//
+// Bedrock-RTL Stable Data CDC with Automatic Update
+//
+// This is a thin wrapper around br_cdc_reg for synchronizing an infrequently
+// changing multi-bit value. It is similar to br_cdc_stable_data, but the src_valid
+// signal is generated automatically based on whether the src_data signal has been changed.
+//
+
+`include "br_asserts_internal.svh"
+`include "br_registers.svh"
+
+module br_cdc_stable_data_autoupdate #(
+    parameter int Width = 1,
+    parameter logic [Width-1:0] InitValue = '0,
+    parameter bit RegisterResetActive = 1,
+    parameter int NumSyncStages = 3
+) (
+    input logic src_clk,
+    input logic src_rst,
+    input logic [Width-1:0] src_data,
+
+    // ri lint_check_waive ONE_LOCAL_CLOCK
+    input logic dst_clk,
+    input logic dst_rst,
+    output logic dst_updated,
+    output logic [Width-1:0] dst_data
+);
+  // Integration Checks
+  // Rely on checks in br_cdc_stable_data submodule
+
+  // Implementation
+  logic src_valid;
+  logic src_ready;
+  logic [Width-1:0] src_data_reg;
+
+  logic dst_updated_next;
+  logic [Width-1:0] dst_data_next;
+
+  `BR_REGLIX(src_data_reg, src_data, src_valid && src_ready, InitValue, src_clk, src_rst)
+
+  // Send into the register if the data has changed but hasn't been
+  // crossed over yet.
+  assign src_valid = src_data != src_data_reg;
+
+  br_cdc_reg #(
+      .Width(Width),
+      .RegisterResetActive(RegisterResetActive),
+      .NumSyncStages(NumSyncStages),
+      // Data can change if data changes while register is backpressured
+      .EnableAssertPushDataStability(0)
+  ) br_cdc_reg_inst (
+      .push_clk  (src_clk),    // ri lint_check_waive SAME_CLOCK_NAME
+      .push_rst  (src_rst),
+      .push_valid(src_valid),
+      .push_ready(src_ready),
+      .push_data (src_data),
+
+      .pop_clk(dst_clk),  // ri lint_check_waive SAME_CLOCK_NAME
+      .pop_rst(dst_rst),
+      .pop_ready(1'b1),
+      .pop_valid(dst_updated_next),
+      .pop_data(dst_data_next)
+  );
+
+  `BR_REGX(dst_updated, dst_updated_next, dst_clk, dst_rst)
+  `BR_REGLIX(dst_data, dst_data_next, dst_updated_next, InitValue, dst_clk, dst_rst)
+
+  // Implementation checks
+  // TODO(zhemao): Add some here
+
+endmodule : br_cdc_stable_data_autoupdate

cdc/sim/BUILD.bazel

@@ -305,3 +305,55 @@ br_verilog_sim_test_tools_suite(
         "//gate/rtl:br_gate_mock",
     ],
 )
+
+verilog_library(
+    name = "br_cdc_stable_data_autoupdate_tb",
+    srcs = ["br_cdc_stable_data_autoupdate_tb.sv"],
+    deps = [
+        "//cdc/rtl:br_cdc_stable_data_autoupdate",
+        "//misc/sim:br_test_driver",
+    ],
+)
+
+verilog_elab_test(
+    name = "br_cdc_stable_data_autoupdate_tb_elab_test",
+    tool = "verific",
+    top = "br_cdc_stable_data_autoupdate_tb",
+    deps = [
+        ":br_cdc_stable_data_autoupdate_tb",
+        "//gate/rtl:br_gate_mock",
+    ],
+)
+
+br_verilog_sim_test_tools_suite(
+    name = "br_cdc_stable_data_autoupdate_sim_test_tools_suite",
+    params = {
+        "Width": ["8"],
+        "InitValue": [
+            "0",
+            "1",
+        ],
+        "RegisterResetActive": [
+            "0",
+            "1",
+        ],
+        "NumSyncStages": [
+            "2",
+            "3",
+        ],
+        "SrcClkPeriodNs": [
+            "10",
+            "16",
+        ],
+        "DstClkPeriodNs": [
+            "10",
+            "16",
+        ],
+    },
+    tools = ["vcs"],
+    top = "br_cdc_stable_data_autoupdate_tb",
+    deps = [
+        ":br_cdc_stable_data_autoupdate_tb",
+        "//gate/rtl:br_gate_mock",
+    ],
+)