diff --git a/cdc/fpv/BUILD.bazel b/cdc/fpv/BUILD.bazel index b07af6dd3..0c4358f0d 100644 --- a/cdc/fpv/BUILD.bazel +++ b/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", + ], +) diff --git a/cdc/fpv/br_cdc_reg_fpv.jg.tcl b/cdc/fpv/br_cdc_reg_fpv.jg.tcl new file mode 100644 index 000000000..18f0a2f47 --- /dev/null +++ b/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 diff --git a/cdc/fpv/br_cdc_reg_fpv_monitor.sv b/cdc/fpv/br_cdc_reg_fpv_monitor.sv new file mode 100644 index 000000000..4e606ef6c --- /dev/null +++ b/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 diff --git a/cdc/rtl/BUILD.bazel b/cdc/rtl/BUILD.bazel index b51e743bf..c012ae3e6 100644 --- a/cdc/rtl/BUILD.bazel +++ b/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", + ], +) diff --git a/cdc/rtl/br_cdc_stable_data_autoupdate.sv b/cdc/rtl/br_cdc_stable_data_autoupdate.sv new file mode 100644 index 000000000..0ed9cfdcc --- /dev/null +++ b/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 diff --git a/cdc/sim/BUILD.bazel b/cdc/sim/BUILD.bazel index 666d9a3ba..9d3bd6a73 100644 --- a/cdc/sim/BUILD.bazel +++ b/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", + ], +) diff --git a/cdc/sim/br_cdc_stable_data_autoupdate_tb.sv b/cdc/sim/br_cdc_stable_data_autoupdate_tb.sv new file mode 100644 index 000000000..b8c7cac6f --- /dev/null +++ b/cdc/sim/br_cdc_stable_data_autoupdate_tb.sv @@ -0,0 +1,79 @@ +// SPDX-License-Identifier: Apache-2.0 +// +// Bedrock-RTL Stable Data CDC Unit Test +// + +module br_cdc_stable_data_autoupdate_tb; + parameter int Width = 8; + parameter logic [Width-1:0] InitValue = '0; + parameter bit RegisterResetActive = 1; + parameter int NumSyncStages = 3; + parameter int SrcClkPeriodNs = 10; + parameter int DstClkPeriodNs = 10; + + logic src_clk; + logic src_rst; + logic [Width-1:0] src_data; + logic dst_clk; + logic dst_rst; + logic dst_updated; + logic [Width-1:0] dst_data; + + br_cdc_stable_data_autoupdate #( + .Width(Width), + .InitValue(InitValue), + .RegisterResetActive(RegisterResetActive), + .NumSyncStages(NumSyncStages) + ) dut ( + .src_clk, + .src_rst, + .src_data, + .dst_clk, + .dst_rst, + .dst_updated, + .dst_data + ); + + br_test_driver #( + .ResetCycles(14) + ) td ( + .clk(src_clk), + .rst(src_rst) + ); + + initial dst_clk = 1'b0; + always #(DstClkPeriodNs / 2) dst_clk = ~dst_clk; + + initial begin + dst_rst = 1'b1; + src_data = InitValue; + + td.reset_dut(); + + @(negedge dst_clk); + dst_rst = 1'b0; + + @(posedge dst_clk); + td.check_integer(dst_data, InitValue, "dst_data initial value mismatch"); + + for (int i = 5; i < 15; i++) begin + // Send the update + @(negedge src_clk); + src_data = i; + + // Wait until we see the update on the destination side + @(posedge dst_clk); + while (!dst_updated) @(posedge dst_clk); + td.check_integer(dst_data, i, "dst_data value mismatch"); + // The data should remain stable after update + @(posedge dst_clk); + td.check_integer(dst_data, i, "dst_data value not stable"); + + // Need to wait some cycles for the source side to be ready again + td.wait_cycles(10); + end + + td.finish(); + end + +endmodule