Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
14 changes: 14 additions & 0 deletions cdc/fpv/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -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",
],
)
19 changes: 17 additions & 2 deletions cdc/fpv/br_cdc_fifo_flops_fpv.jg.tcl
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
38 changes: 6 additions & 32 deletions cdc/fpv/br_cdc_fifo_flops_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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
139 changes: 49 additions & 90 deletions cdc/rtl/br_cdc_fifo_flops.sv
Original file line number Diff line number Diff line change
Expand Up @@ -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
Loading