diff --git a/cdc/fpv/BUILD.bazel b/cdc/fpv/BUILD.bazel index b07af6dd3..1f434e1a3 100644 --- a/cdc/fpv/BUILD.bazel +++ b/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", + ], +) 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/fpv/br_cdc_stable_data_fpv.jg.tcl b/cdc/fpv/br_cdc_stable_data_fpv.jg.tcl new file mode 100644 index 000000000..ac722ea90 --- /dev/null +++ b/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 diff --git a/cdc/fpv/br_cdc_stable_data_fpv_monitor.sv b/cdc/fpv/br_cdc_stable_data_fpv_monitor.sv new file mode 100644 index 000000000..a71c89295 --- /dev/null +++ b/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