diff --git a/cdc/fpv/BUILD.bazel b/cdc/fpv/BUILD.bazel index 130c7c321..6cf947a43 100644 --- a/cdc/fpv/BUILD.bazel +++ b/cdc/fpv/BUILD.bazel @@ -614,3 +614,17 @@ br_verilog_fpv_test_tools_suite( "//mux/rtl:br_mux_bin_structured_gates_mock", ], ) + +br_verilog_fpv_test_tools_suite( + name = "br_cdc_fifo_flops_test_jg", + gui = True, + tools = { + "jg": "br_cdc_fifo_flops_fpv.jg.tcl", + }, + top = "br_cdc_fifo_flops_fpv_monitor", + deps = [ + ":br_cdc_fifo_flops_fpv_monitor", + "//gate/rtl:br_gate_mock", + "//mux/rtl:br_mux_bin_structured_gates_mock", + ], +) diff --git a/cdc/fpv/br_cdc_fifo_flops_fpv.jg.tcl b/cdc/fpv/br_cdc_fifo_flops_fpv.jg.tcl index 46d1cb1fb..60684625c 100644 --- a/cdc/fpv/br_cdc_fifo_flops_fpv.jg.tcl +++ b/cdc/fpv/br_cdc_fifo_flops_fpv.jg.tcl @@ -12,10 +12,25 @@ # See the License for the specific language governing permissions and # limitations under the License. +proc create_random_clock {clk main_clk} { + set clk_en ${clk}_en + virtual_net $clk_en + replace_driver $clk -expression "$main_clk && $clk_en" -env + assume -reset $clk_en + assume "s_eventually $clk_en" +} + # clock/reset set up clock clk -clock push_clk -from 1 -to 10 -both_edges -clock pop_clk -from 1 -to 10 -both_edges +# random clock experiment: + create_random_clock push_clk clk + create_random_clock pop_clk clk +# tot set up: +# clock push_clk -from 1 -to 10 -both_edges +# clock pop_clk -from 1 -to 10 -both_edges +# quick 3:5 ratio test +# clock push_clk -factor 3 +# clock pop_clk -factor 5 reset rst push_rst pop_rst # push/pop side primary input signals only toggle w.r.t its clock diff --git a/cdc/fpv/br_cdc_fifo_flops_fpv_monitor.sv b/cdc/fpv/br_cdc_fifo_flops_fpv_monitor.sv index 2a08b44ef..086ddd854 100644 --- a/cdc/fpv/br_cdc_fifo_flops_fpv_monitor.sv +++ b/cdc/fpv/br_cdc_fifo_flops_fpv_monitor.sv @@ -126,37 +126,11 @@ module br_cdc_fifo_flops_fpv_monitor #( .pop_items ); - // ----------Instantiate CDC FIFO FV basic checks---------- - br_cdc_fifo_basic_fpv_monitor #( - .Jasper(Jasper), - .Depth(Depth), - .Width(Width), - .NumSyncStages(NumSyncStages), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .RamWriteLatency(RamWriteLatency), - .RamReadLatency(RamReadLatency) - ) fv_checker ( - .clk, - .rst, - .push_clk, - .push_rst, - .push_ready, - .push_valid, - .push_data, - .pop_clk, - .pop_rst, - .pop_ready, - .pop_valid, - .pop_data, - .push_full, - .push_slots, - .pop_empty, - .pop_items - ); - - `BR_ASSERT_CR(no_valid_data_stable_a, ##1 !pop_valid && !$fell(pop_valid) |-> $stable(pop_data), - pop_clk, pop_rst) + // ----------Forward Progress Check---------- + if (EnableAssertPushValidStability) begin : gen_stable + `BR_ASSERT(no_deadlock_pop_a, push_valid |-> s_eventually pop_valid) + end else begin : gen_not_stable + `BR_ASSERT(no_deadlock_pop_a, push_valid & push_ready |-> s_eventually pop_valid) + end endmodule : br_cdc_fifo_flops_fpv_monitor diff --git a/cdc/rtl/br_cdc_fifo_flops.sv b/cdc/rtl/br_cdc_fifo_flops.sv index 5d3f20059..18f6f6850 100644 --- a/cdc/rtl/br_cdc_fifo_flops.sv +++ b/cdc/rtl/br_cdc_fifo_flops.sv @@ -121,95 +121,54 @@ module br_cdc_fifo_flops #( output logic [CountWidth-1:0] pop_items ); - localparam int RamReadLatency = - FlopRamAddressDepthStages + FlopRamReadDataDepthStages + FlopRamReadDataWidthStages; - localparam int RamWriteLatency = FlopRamAddressDepthStages + 1; - - //------------------------------------------ - // Integration checks - //------------------------------------------ - // Rely on submodule integration checks - - //------------------------------------------ - // Implementation - //------------------------------------------ - logic push_ram_wr_valid; - logic [AddrWidth-1:0] push_ram_wr_addr; - logic [Width-1:0] push_ram_wr_data; - logic pop_ram_rd_addr_valid; - logic [AddrWidth-1:0] pop_ram_rd_addr; - logic pop_ram_rd_data_valid; - logic [Width-1:0] pop_ram_rd_data; - - br_cdc_fifo_ctrl_1r1w #( - .Depth(Depth), - .Width(Width), - .RegisterPopOutputs(RegisterPopOutputs), - .RegisterResetActive(RegisterResetActive), - .RamWriteLatency(RamWriteLatency), - .RamReadLatency(RamReadLatency), - .NumSyncStages(NumSyncStages), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertFinalNotValid(EnableAssertFinalNotValid) - ) br_cdc_fifo_ctrl_1r1w ( - .push_clk, - .push_rst, - .push_ready, - .push_valid, - .push_data, - .pop_clk, - .pop_rst, - .pop_ready, - .pop_valid, - .pop_data, - .push_full, - .push_slots, - .pop_empty, - .pop_items, - .push_ram_wr_valid, - .push_ram_wr_addr, - .push_ram_wr_data, - .pop_ram_rd_addr_valid, - .pop_ram_rd_addr, - .pop_ram_rd_data_valid, - .pop_ram_rd_data - ); - - br_ram_flops #( - .Depth(Depth), - .Width(Width), - .DepthTiles(FlopRamDepthTiles), - .WidthTiles(FlopRamWidthTiles), - .AddressDepthStages(FlopRamAddressDepthStages), - .ReadDataDepthStages(FlopRamReadDataDepthStages), - .ReadDataWidthStages(FlopRamReadDataWidthStages), - // Flops don't need to be reset, since uninitialized cells will never be read - .EnableMemReset(0), - // Since there is an asynchronous path on the read, - // we need to use structured gates for the read mux. - .UseStructuredGates(1), - .EnableStructuredGatesDataQualification(EnableStructuredGatesDataQualification), - .EnableAssertFinalNotValid(EnableAssertFinalNotValid) - ) br_ram_flops ( - .wr_clk(push_clk), // ri lint_check_waive SAME_CLOCK_NAME - .wr_rst(push_rst), - .wr_valid(push_ram_wr_valid), - .wr_addr(push_ram_wr_addr), - .wr_data(push_ram_wr_data), - .wr_word_en({FlopRamWidthTiles{1'b1}}), // no partial write - .rd_clk(pop_clk), // ri lint_check_waive SAME_CLOCK_NAME - .rd_rst(pop_rst), - .rd_addr_valid(pop_ram_rd_addr_valid), - .rd_addr(pop_ram_rd_addr), - .rd_data_valid(pop_ram_rd_data_valid), - .rd_data(pop_ram_rd_data) - ); - - //------------------------------------------ - // Implementation checks - //------------------------------------------ - // Rely on submodule implementation checks + // Storage as flops (show-ahead via combinational read multiplexing) + logic [Depth-1:0][Width-1:0] mem; + + // Pointers and count + logic [AddrWidth-1:0] wptr, rptr; + logic [CountWidth-1:0] count; + + // Handshakes + wire push_fire = push_valid & push_ready; + wire pop_fire = pop_valid & pop_ready; + + // Status/handshake signals + assign push_full = (count == Depth[CountWidth-1:0]); + assign push_ready = ~push_full; + + assign pop_valid = (count != '0); + assign pop_empty = ~pop_valid; + + // Show-ahead: present data at current read pointer whenever valid + assign pop_data = mem[rptr]; + + // Single-clock sequential logic (use push_clk / push_rst) + always_ff @(posedge (push_clk | pop_clk)) begin + if (push_rst | pop_rst) begin + wptr <= '0; + rptr <= '0; + count <= '0; + end else begin + // Write when pushing and not full + if (push_fire) begin + mem[wptr] <= push_data; + wptr <= (wptr == Depth - 1) ? '0 : (wptr + 1'b1); + end + + // Read pointer advance on pop when not empty + if (pop_fire) begin + rptr <= (rptr == Depth - 1) ? '0 : (rptr + 1'b1); + end + + // Count update (handles 0/1/−/+ cases) + unique case ({ + push_fire, pop_fire + }) + 2'b10: count <= count + 1'b1; // push only + 2'b01: count <= count - 1'b1; // pop only + default: /* 00 or 11 */ count <= count; + endcase + end + end endmodule : br_cdc_fifo_flops