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
1 change: 1 addition & 0 deletions cdc/fpv/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -599,6 +599,7 @@ br_verilog_fpv_test_tools_suite(
# VCF experiment
br_verilog_fpv_test_tools_suite(
name = "br_cdc_fifo_flops_test_vcf",
gui = True,
params = {
"Jasper": [
"0",
Expand Down
7 changes: 5 additions & 2 deletions cdc/fpv/br_cdc_fifo_flops_fpv.vcf.tcl
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,11 @@

# clock/reset set up
create_clock clk -period 10
create_random_clock -clock push_clk -period 10
create_random_clock -clock pop_clk -period 10
#create_random_clock -clock push_clk -period 10
#create_random_clock -clock pop_clk -period 10
# create clock with ratio 3:5
create_clock push_clk -period 30
create_clock pop_clk -period 50
# Synopsys AE claims:
# create_random_clock is implemented by driving clock through a clock gater with enable being x
# therefore, user needs to add liveness assumptions to ensure clock will eventually toggle
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