diff --git a/amba/rtl/br_amba_axi_demux.sv b/amba/rtl/br_amba_axi_demux.sv index 59745866b..bcd10aa86 100644 --- a/amba/rtl/br_amba_axi_demux.sv +++ b/amba/rtl/br_amba_axi_demux.sv @@ -391,9 +391,7 @@ module br_amba_axi_demux #( br_fifo_flops #( .Depth(MaxAwRunahead), - .Width(SubIdWidth), - // Valid can drop if downstream deasserts ready. - .EnableAssertPushValidStability(0) + .Width(SubIdWidth) ) br_fifo_flops_wdata_flow_buffer ( .clk, .rst, diff --git a/amba/rtl/br_amba_axi_isolate_mgr.sv b/amba/rtl/br_amba_axi_isolate_mgr.sv index f0fb3230a..de0409366 100644 --- a/amba/rtl/br_amba_axi_isolate_mgr.sv +++ b/amba/rtl/br_amba_axi_isolate_mgr.sv @@ -413,9 +413,7 @@ module br_amba_axi_isolate_mgr #( downstream_awprot_int ) + $bits( downstream_awuser_int - )), - .EnableAssertPushValidStability(0), - .EnableAssertPushDataStability(0) + )) ) br_flow_reg_fwd_ds_aw ( .clk, .rst, @@ -456,9 +454,7 @@ module br_amba_axi_isolate_mgr #( downstream_wuser_int ) + $bits( downstream_wlast_int - )), - .EnableAssertPushValidStability(0), - .EnableAssertPushDataStability(0) + )) ) br_flow_reg_fwd_ds_w ( .clk, .rst, @@ -491,9 +487,7 @@ module br_amba_axi_isolate_mgr #( downstream_arprot_int ) + $bits( downstream_aruser_int - )), - .EnableAssertPushValidStability(0), - .EnableAssertPushDataStability(0) + )) ) br_flow_reg_fwd_ds_ar ( .clk, .rst, diff --git a/amba/rtl/br_amba_axi_isolate_sub.sv b/amba/rtl/br_amba_axi_isolate_sub.sv index ce76e672a..461bf5de0 100644 --- a/amba/rtl/br_amba_axi_isolate_sub.sv +++ b/amba/rtl/br_amba_axi_isolate_sub.sv @@ -528,9 +528,7 @@ module br_amba_axi_isolate_sub #( upstream_ruser ) + $bits( upstream_rid - )), - .EnableAssertPushValidStability(0), - .EnableAssertPushDataStability(0) + )) ) br_flow_reg_fwd_us_r ( .clk, .rst, @@ -551,9 +549,7 @@ module br_amba_axi_isolate_sub #( ); br_flow_reg_fwd #( - .Width($bits(upstream_bresp) + $bits(upstream_buser) + $bits(upstream_bid)), - .EnableAssertPushValidStability(0), - .EnableAssertPushDataStability(0) + .Width($bits(upstream_bresp) + $bits(upstream_buser) + $bits(upstream_bid)) ) br_flow_reg_fwd_us_aw ( .clk, .rst, diff --git a/amba/rtl/internal/br_amba_axi2axil_core.sv b/amba/rtl/internal/br_amba_axi2axil_core.sv index 9f581d29b..2ed5c751d 100644 --- a/amba/rtl/internal/br_amba_axi2axil_core.sv +++ b/amba/rtl/internal/br_amba_axi2axil_core.sv @@ -311,9 +311,7 @@ module br_amba_axi2axil_core #( .FlopRamWidthTiles(1), .FlopRamAddressDepthStages(0), .FlopRamReadDataDepthStages(0), - .FlopRamReadDataWidthStages(0), - // Valid from br_flow_fork is unstable - .EnableAssertPushValidStability(0) + .FlopRamReadDataWidthStages(0) ) br_fifo_flops_resp_tracker ( .clk, .rst, diff --git a/amba/rtl/internal/br_amba_axi_demux_req_tracker.sv b/amba/rtl/internal/br_amba_axi_demux_req_tracker.sv index 146508a00..556ad3e49 100644 --- a/amba/rtl/internal/br_amba_axi_demux_req_tracker.sv +++ b/amba/rtl/internal/br_amba_axi_demux_req_tracker.sv @@ -224,8 +224,7 @@ module br_amba_axi_demux_req_tracker #( br_flow_demux_select_unstable #( .NumFlows(NumIds), - .Width(1), - .EnableAssertPushValidStability(0) + .Width(1) ) br_flow_demux_select_unstable_resp_tracker_push ( .clk, .rst, @@ -418,10 +417,7 @@ module br_amba_axi_demux_req_tracker #( // Output buffer (to cut upstream_xready -> upstream_xvalid path) br_flow_reg_fwd #( - .Width(AxiIdWidth + RespPayloadWidth + 1), - // If a higher-priority downstream port with a different ID becomes valid, - // the mux select can change, resulting in data not remaining stable. - .EnableAssertPushDataStability(0) + .Width(AxiIdWidth + RespPayloadWidth + 1) ) br_flow_reg_fwd_upstream_resp ( .clk, .rst, diff --git a/amba/rtl/internal/br_amba_iso_resp_tracker.sv b/amba/rtl/internal/br_amba_iso_resp_tracker.sv index 651bffc30..5dd40c228 100644 --- a/amba/rtl/internal/br_amba_iso_resp_tracker.sv +++ b/amba/rtl/internal/br_amba_iso_resp_tracker.sv @@ -296,9 +296,7 @@ module br_amba_iso_resp_tracker #( br_fifo_flops #( .Depth(MaxTransactionSkew), - .Width(AxiBurstLenWidth + MinIdWidth), - // valid can deassert if downstream_axready deasserts - .EnableAssertPushValidStability(0) + .Width(AxiBurstLenWidth + MinIdWidth) ) br_fifo_flops_aw_staging ( .clk, .rst, @@ -322,10 +320,7 @@ module br_amba_iso_resp_tracker #( ); br_flow_fork #( - .NumFlows(2), - // If W beats are in excess when wdata alignment (during isolation) is requested, the - // upstream valid can deassert without ready asserting. - .EnableAssertPushValidStability(0) + .NumFlows(2) ) br_flow_fork_wlast_staging ( .clk, .rst, @@ -341,9 +336,7 @@ module br_amba_iso_resp_tracker #( br_fifo_flops #( .Depth(MaxTransactionSkew), - .Width(1), - // valid can deassert if downstream_wready deasserts - .EnableAssertPushValidStability(0) + .Width(1) ) br_fifo_flops_wlast_staging ( .clk, .rst, @@ -404,9 +397,7 @@ module br_amba_iso_resp_tracker #( .Depth(MaxOutstanding), .Width(AxiBurstLenWidth), .EnableBypass(1), - .RegisterPopOutputs(1), - // When EnableWlastTracking=0, valid can deassert if downstream_axready deasserts - .EnableAssertPushValidStability(EnableWlastTracking) + .RegisterPopOutputs(1) ) br_fifo_flops_req_tracker ( .clk, .rst, @@ -444,9 +435,7 @@ module br_amba_iso_resp_tracker #( .DataRamAddressDepthStages(DynamicFifoDataRamAddressDepthStages), .StagingBufferDepth(DynamicFifoStagingBufferDepth), .RegisterPopOutputs(DynamicFifoRegisterPopOutputs), - .RegisterDeallocation(DynamicFifoRegisterDeallocation), - // When EnableWlastTracking=0, valid can deassert if downstream_axready deasserts - .EnableAssertPushValidStability(EnableWlastTracking) + .RegisterDeallocation(DynamicFifoRegisterDeallocation) ) br_fifo_shared_dynamic_flops_req_tracker ( .clk, .rst, @@ -472,9 +461,7 @@ module br_amba_iso_resp_tracker #( br_flow_demux_select_unstable #( .NumFlows(AxiIdCount), - .Width(AxiBurstLenWidth), - // When EnableWlastTracking=0, valid can deassert if downstream_axready deasserts - .EnableAssertPushValidStability(EnableWlastTracking) + .Width(AxiBurstLenWidth) ) br_flow_demux_select_unstable_req_tracker ( .clk, .rst, @@ -526,9 +513,7 @@ module br_amba_iso_resp_tracker #( .Depth(PerIdFifoDepth), .Width(AxiBurstLenWidth), .EnableBypass(0), - .RegisterPopOutputs(0), - // When EnableWlastTracking=0, valid can deassert if downstream_axready deasserts - .EnableAssertPushValidStability(EnableWlastTracking) + .RegisterPopOutputs(0) ) br_fifo_flops_req_tracker ( .clk, .rst, diff --git a/arb/fpv/br_arb_rr_fpv_monitor.sv b/arb/fpv/br_arb_rr_fpv_monitor.sv index f8f12a8f5..d79224559 100644 --- a/arb/fpv/br_arb_rr_fpv_monitor.sv +++ b/arb/fpv/br_arb_rr_fpv_monitor.sv @@ -40,7 +40,7 @@ module br_arb_rr_fpv_monitor #( // ----------Round Robin checks---------- rr_basic_fpv_monitor #( .NumRequesters(NumRequesters), - .EnableAssertPushValidStability(1) + .EnableAssumeRequestStability(1) ) rr_check ( .clk, .rst, diff --git a/arb/fpv/rr_basic_fpv_monitor.sv b/arb/fpv/rr_basic_fpv_monitor.sv index e1478bb86..fbbc46411 100644 --- a/arb/fpv/rr_basic_fpv_monitor.sv +++ b/arb/fpv/rr_basic_fpv_monitor.sv @@ -10,7 +10,7 @@ module rr_basic_fpv_monitor #( // Must be at least 2 parameter int NumRequesters = 2, - parameter bit EnableAssertPushValidStability = 1 + parameter bit EnableAssumeRequestStability = 1 ) ( input logic clk, input logic rst, @@ -41,7 +41,7 @@ module rr_basic_fpv_monitor #( // j ... i ... high_priority ... ((2 ** j <= high_priority_request) && (2 ** i < high_priority_request) && (j < i))) - if (EnableAssertPushValidStability) begin : gen_req_stable + if (EnableAssumeRequestStability) begin : gen_req_stable `BR_ASSERT(round_robin_a, request[i] |-> not (!grant[i] && enable_priority_update throughout grant[j] [-> 2])) end diff --git a/cdc/fpv/BUILD.bazel b/cdc/fpv/BUILD.bazel index b07af6dd3..e8ea7977b 100644 --- a/cdc/fpv/BUILD.bazel +++ b/cdc/fpv/BUILD.bazel @@ -49,8 +49,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -59,11 +59,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -228,8 +228,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -238,11 +238,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -416,8 +416,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -426,11 +426,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/cdc/fpv/br_cdc_fifo_basic_fpv_monitor.sv b/cdc/fpv/br_cdc_fifo_basic_fpv_monitor.sv index 16584ed08..652f4539a 100644 --- a/cdc/fpv/br_cdc_fifo_basic_fpv_monitor.sv +++ b/cdc/fpv/br_cdc_fifo_basic_fpv_monitor.sv @@ -15,12 +15,6 @@ module br_cdc_fifo_basic_fpv_monitor #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // If 0, cover that push_data can be unstable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, parameter int RamWriteLatency = 1, parameter int RamReadLatency = 1, parameter int PushExtraDelay = 0, @@ -67,16 +61,7 @@ module br_cdc_fifo_basic_fpv_monitor #( // ----------FV assumptions---------- `BR_ASSUME_CR(pop_ready_liveness_a, s_eventually (pop_ready), pop_clk, pop_rst) - if (EnableCoverPushBackpressure) begin : gen_back_pressure - if (EnableAssertPushValidStability) begin : gen_push_valid_stable - `BR_ASSUME_CR(push_valid_stable_a, push_valid && !push_ready |=> push_valid, push_clk, - push_rst) - end - if (EnableAssertPushDataStability) begin : gen_push_data_stable - `BR_ASSUME_CR(push_data_stable_a, push_valid && !push_ready |=> $stable(push_data), push_clk, - push_rst) - end - end else begin : gen_no_back_pressure + if (!EnableCoverPushBackpressure) begin : gen_no_back_pressure `BR_ASSUME_CR(no_back_pressure_a, push_valid |-> push_ready, push_clk, push_rst) end @@ -209,11 +194,7 @@ module br_cdc_fifo_basic_fpv_monitor #( end // ----------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_vr |-> s_eventually pop_valid) - end + `BR_ASSERT(no_deadlock_pop_a, push_vr |-> s_eventually pop_valid) // ----------Critical Covers---------- `BR_COVER_CR(fifo_full_c, push_full, push_clk, push_rst) diff --git a/cdc/fpv/br_cdc_fifo_ctrl_1r1w_fpv_monitor.sv b/cdc/fpv/br_cdc_fifo_ctrl_1r1w_fpv_monitor.sv index 93d092cd1..f8ebace1e 100644 --- a/cdc/fpv/br_cdc_fifo_ctrl_1r1w_fpv_monitor.sv +++ b/cdc/fpv/br_cdc_fifo_ctrl_1r1w_fpv_monitor.sv @@ -21,12 +21,6 @@ module br_cdc_fifo_ctrl_1r1w_fpv_monitor #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // If 0, cover that push_data can be unstable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. parameter bit EnableAssertFinalNotValid = 1, @@ -98,8 +92,6 @@ module br_cdc_fifo_ctrl_1r1w_fpv_monitor #( .RamReadLatency(RamReadLatency), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) dut ( .push_clk, @@ -131,8 +123,6 @@ module br_cdc_fifo_ctrl_1r1w_fpv_monitor #( .Width(Width), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .RamWriteLatency(RamWriteLatency), .RamReadLatency(RamReadLatency) ) fv_checker ( diff --git a/cdc/fpv/br_cdc_fifo_ctrl_1r1w_push_credit_fpv_monitor.sv b/cdc/fpv/br_cdc_fifo_ctrl_1r1w_push_credit_fpv_monitor.sv index 51c2bf30f..ec8dca305 100644 --- a/cdc/fpv/br_cdc_fifo_ctrl_1r1w_push_credit_fpv_monitor.sv +++ b/cdc/fpv/br_cdc_fifo_ctrl_1r1w_push_credit_fpv_monitor.sv @@ -157,8 +157,6 @@ module br_cdc_fifo_ctrl_1r1w_push_credit_fpv_monitor #( .Width(Width), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(0), - .EnableAssertPushValidStability(0), - .EnableAssertPushDataStability(0), .RamWriteLatency(RamWriteLatency), .RamReadLatency(RamReadLatency) ) fv_checker ( diff --git a/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_fpv_monitor.sv b/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_fpv_monitor.sv index debe78689..320e53c75 100644 --- a/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_fpv_monitor.sv +++ b/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_fpv_monitor.sv @@ -24,8 +24,6 @@ module br_cdc_fifo_ctrl_push_pop_1r1w_fpv_monitor #( parameter int NumSyncStages = 3, parameter bit RegisterPopOutputs = 0, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, parameter bit EnableAssertFinalNotValid = 1, localparam int AddrWidth = $clog2(Depth), localparam int CountWidth = $clog2(Depth + 1) @@ -100,8 +98,6 @@ module br_cdc_fifo_ctrl_push_pop_1r1w_fpv_monitor #( .RamWriteLatency(RamWriteLatency), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) push_dut ( .push_clk, @@ -155,8 +151,6 @@ module br_cdc_fifo_ctrl_push_pop_1r1w_fpv_monitor #( .Width(Width), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .RamWriteLatency(RamWriteLatency), .RamReadLatency(RamReadLatency) ) fv_checker ( diff --git a/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_push_credit_fpv_monitor.sv b/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_push_credit_fpv_monitor.sv index b3d6e42dd..7f82b55ed 100644 --- a/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_push_credit_fpv_monitor.sv +++ b/cdc/fpv/br_cdc_fifo_ctrl_push_pop_1r1w_push_credit_fpv_monitor.sv @@ -189,8 +189,6 @@ module br_cdc_fifo_ctrl_push_pop_1r1w_push_credit_fpv_monitor #( .Width(Width), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(0), - .EnableAssertPushValidStability(0), - .EnableAssertPushDataStability(0), .RamWriteLatency(RamWriteLatency), .RamReadLatency(RamReadLatency) ) fv_checker ( diff --git a/cdc/fpv/br_cdc_fifo_flops_fpv_monitor.sv b/cdc/fpv/br_cdc_fifo_flops_fpv_monitor.sv index 955f8b3c7..27755bf91 100644 --- a/cdc/fpv/br_cdc_fifo_flops_fpv_monitor.sv +++ b/cdc/fpv/br_cdc_fifo_flops_fpv_monitor.sv @@ -37,12 +37,6 @@ module br_cdc_fifo_flops_fpv_monitor #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // If 0, cover that push_data can be unstable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. parameter bit EnableAssertFinalNotValid = 1, @@ -95,8 +89,6 @@ module br_cdc_fifo_flops_fpv_monitor #( .FlopRamReadDataWidthStages(FlopRamReadDataWidthStages), .EnableStructuredGatesDataQualification(EnableStructuredGatesDataQualification), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) dut ( .push_clk, @@ -122,8 +114,6 @@ module br_cdc_fifo_flops_fpv_monitor #( .Width(Width), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .RamWriteLatency(RamWriteLatency), .RamReadLatency(RamReadLatency) ) fv_checker ( diff --git a/cdc/fpv/br_cdc_fifo_flops_push_credit_fpv_monitor.sv b/cdc/fpv/br_cdc_fifo_flops_push_credit_fpv_monitor.sv index 12e84eb48..745fba9e8 100644 --- a/cdc/fpv/br_cdc_fifo_flops_push_credit_fpv_monitor.sv +++ b/cdc/fpv/br_cdc_fifo_flops_push_credit_fpv_monitor.sv @@ -146,8 +146,6 @@ module br_cdc_fifo_flops_push_credit_fpv_monitor #( .Width(Width), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(0), - .EnableAssertPushValidStability(0), - .EnableAssertPushDataStability(0), .RamWriteLatency(RamWriteLatency), .RamReadLatency(RamReadLatency) ) fv_checker ( diff --git a/cdc/rtl/br_cdc_fifo_ctrl_1r1w.sv b/cdc/rtl/br_cdc_fifo_ctrl_1r1w.sv index 175435970..f11ef8d96 100644 --- a/cdc/rtl/br_cdc_fifo_ctrl_1r1w.sv +++ b/cdc/rtl/br_cdc_fifo_ctrl_1r1w.sv @@ -67,10 +67,6 @@ module br_cdc_fifo_ctrl_1r1w #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. parameter bit EnableAssertFinalNotValid = 1, @@ -137,8 +133,6 @@ module br_cdc_fifo_ctrl_1r1w #( .RamWriteLatency(RamWriteLatency), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_cdc_fifo_ctrl_push_1r1w ( .push_clk, diff --git a/cdc/rtl/br_cdc_fifo_ctrl_push_1r1w.sv b/cdc/rtl/br_cdc_fifo_ctrl_push_1r1w.sv index 5e8f461d6..85054858b 100644 --- a/cdc/rtl/br_cdc_fifo_ctrl_push_1r1w.sv +++ b/cdc/rtl/br_cdc_fifo_ctrl_push_1r1w.sv @@ -35,10 +35,6 @@ module br_cdc_fifo_ctrl_push_1r1w #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. parameter bit EnableAssertFinalNotValid = 1, @@ -93,8 +89,6 @@ module br_cdc_fifo_ctrl_push_1r1w #( .RamWriteLatency(RamWriteLatency), .RegisterResetActive(RegisterResetActive), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_cdc_fifo_push_ctrl ( .clk (push_clk), // ri lint_check_waive SAME_CLOCK_NAME diff --git a/cdc/rtl/br_cdc_fifo_flops.sv b/cdc/rtl/br_cdc_fifo_flops.sv index 55f068477..ea8e1f4fa 100644 --- a/cdc/rtl/br_cdc_fifo_flops.sv +++ b/cdc/rtl/br_cdc_fifo_flops.sv @@ -68,10 +68,6 @@ module br_cdc_fifo_flops #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. parameter bit EnableAssertFinalNotValid = 1, @@ -137,8 +133,6 @@ module br_cdc_fifo_flops #( .RamReadLatency(RamReadLatency), .NumSyncStages(NumSyncStages), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_cdc_fifo_ctrl_1r1w ( .push_clk, diff --git a/cdc/rtl/internal/br_cdc_fifo_push_ctrl.sv b/cdc/rtl/internal/br_cdc_fifo_push_ctrl.sv index c9a902633..f9815484d 100644 --- a/cdc/rtl/internal/br_cdc_fifo_push_ctrl.sv +++ b/cdc/rtl/internal/br_cdc_fifo_push_ctrl.sv @@ -13,10 +13,6 @@ module br_cdc_fifo_push_ctrl #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = 1, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. parameter bit EnableAssertFinalNotValid = 1, @@ -92,8 +88,6 @@ module br_cdc_fifo_push_ctrl #( .Width(Width), .EnableBypass(1'b0), // Bypass is not enabled for CDC .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_push_ctrl_core ( .clk, diff --git a/cdc/sim/br_cdc_fifo_flops_push_credit_tb.sv b/cdc/sim/br_cdc_fifo_flops_push_credit_tb.sv index 7f788f11e..ca3b3961c 100644 --- a/cdc/sim/br_cdc_fifo_flops_push_credit_tb.sv +++ b/cdc/sim/br_cdc_fifo_flops_push_credit_tb.sv @@ -93,10 +93,7 @@ module br_cdc_fifo_flops_push_credit_tb (); br_credit_sender #( .Width(Width), - .MaxCredit(Depth), - // The test harness causes instability on the push_valid, - // so need to disable the stability check - .EnableAssertPushValidStability(0) + .MaxCredit(Depth) ) br_credit_sender ( .clk, .rst, diff --git a/cdc/sim/br_cdc_fifo_flops_tb.sv b/cdc/sim/br_cdc_fifo_flops_tb.sv index 35411b3dc..24257750f 100644 --- a/cdc/sim/br_cdc_fifo_flops_tb.sv +++ b/cdc/sim/br_cdc_fifo_flops_tb.sv @@ -46,10 +46,7 @@ module br_cdc_fifo_flops_tb; .NumSyncStages(NumSyncStages), .RegisterPopOutputs(RegisterPopOutputs), .FlopRamAddressDepthStages(FlopRamAddressDepthStages), - .FlopRamReadDataDepthStages(FlopRamReadDataDepthStages), - // The test harness causes instability on the push_valid, - // so need to disable the stability check - .EnableAssertPushValidStability(0) + .FlopRamReadDataDepthStages(FlopRamReadDataDepthStages) ) dut ( .push_clk(clk), // ri lint_check_waive SAME_CLOCK_NAME .push_rst(rst), diff --git a/credit/fpv/BUILD.bazel b/credit/fpv/BUILD.bazel index 18c0efe54..b5c9194e7 100644 --- a/credit/fpv/BUILD.bazel +++ b/credit/fpv/BUILD.bazel @@ -192,8 +192,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -206,11 +206,11 @@ br_verilog_fpv_test_tools_suite( "0", "1", ], - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/credit/fpv/br_credit_sender_fpv_monitor.sv b/credit/fpv/br_credit_sender_fpv_monitor.sv index 6ae5bc2a9..91946225f 100644 --- a/credit/fpv/br_credit_sender_fpv_monitor.sv +++ b/credit/fpv/br_credit_sender_fpv_monitor.sv @@ -23,12 +23,6 @@ module br_credit_sender_fpv_monitor #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // If 0, cover that push_data can be unstable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted at the end of the test. parameter bit EnableAssertFinalNotValid = 1, @@ -82,28 +76,12 @@ module br_credit_sender_fpv_monitor #( if (!EnableCoverPushBackpressure) begin : gen_no_push_backpressure `BR_ASSUME(no_push_backpressure_a, !push_ready[n] |-> !push_valid[n]) end - if (EnableAssertPushValidStability) begin : gen_push_valid_stable - `BR_ASSUME(push_valid_stable_a, push_valid[n] && !push_ready[n] |=> push_valid[n]) - end - if (EnableAssertPushDataStability) begin : gen_push_data_stable - `BR_ASSUME(push_data_stable_a, push_valid[n] && !push_ready[n] |=> $stable(push_data[n])) - end end `BR_ASSUME(no_spurious_pop_credit_a, (fv_max_credit - fv_pop_credit_cnt + $countones(pop_valid) ) >= pop_credit) `BR_ASSUME(legal_pop_credit_a, pop_credit <= PopCreditMaxChange) `BR_ASSUME(pop_credit_liveness_a, s_eventually |pop_credit) - if (EnableAssertPushValidStability) begin : gen_push_valid_stable - `BR_ASSUME(push_valid_stable_a, - push_valid[fv_flow] && !push_ready[fv_flow] |=> push_valid[fv_flow]) - end - - if (EnableAssertPushDataStability) begin : gen_push_data_stable - `BR_ASSUME(push_data_stable_a, - push_valid[fv_flow] && !push_ready[fv_flow] |=> $stable(push_data[fv_flow])) - end - if (!EnableCoverPushBackpressure) begin : gen_no_push_backpressure `BR_ASSUME(no_push_backpressure_a, !push_ready[fv_flow] |-> !push_valid[fv_flow]) end @@ -136,7 +114,5 @@ bind br_credit_sender br_credit_sender_fpv_monitor #( .PopCreditMaxChange(PopCreditMaxChange), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/credit/rtl/br_credit_sender.sv b/credit/rtl/br_credit_sender.sv index 99c697b23..fe6c14b42 100644 --- a/credit/rtl/br_credit_sender.sv +++ b/credit/rtl/br_credit_sender.sv @@ -79,10 +79,6 @@ module br_credit_sender #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, cover that credit_withhold can be non-zero. @@ -146,8 +142,8 @@ module br_credit_sender #( .NumFlows(NumFlows), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( diff --git a/credit/rtl/br_credit_sender_vc.sv b/credit/rtl/br_credit_sender_vc.sv index a3d17bc4f..61849a32d 100644 --- a/credit/rtl/br_credit_sender_vc.sv +++ b/credit/rtl/br_credit_sender_vc.sv @@ -31,10 +31,6 @@ module br_credit_sender_vc #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted at the end of the test. parameter bit EnableAssertFinalNotValid = 1, // If 1, then at the end of simulation, assert that the credit counter value equals @@ -139,7 +135,6 @@ module br_credit_sender_vc #( br_flow_fork #( .NumFlows(2), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_fork_push ( .clk, @@ -159,8 +154,6 @@ module br_credit_sender_vc #( .NumFlows(NumVcs), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_core_push ( .clk, diff --git a/fifo/fpv/br_fifo/BUILD.bazel b/fifo/fpv/br_fifo/BUILD.bazel index 4c69323f4..103898f32 100644 --- a/fifo/fpv/br_fifo/BUILD.bazel +++ b/fifo/fpv/br_fifo/BUILD.bazel @@ -42,8 +42,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -52,11 +52,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -189,8 +189,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -199,11 +199,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/fifo/fpv/br_fifo/br_fifo_basic_fpv_monitor.sv b/fifo/fpv/br_fifo/br_fifo_basic_fpv_monitor.sv index 84062bd47..89996c96c 100644 --- a/fifo/fpv/br_fifo/br_fifo_basic_fpv_monitor.sv +++ b/fifo/fpv/br_fifo/br_fifo_basic_fpv_monitor.sv @@ -13,8 +13,8 @@ module br_fifo_basic_fpv_monitor #( parameter int Width = 1, // Width of each entry in the FIFO. Must be at least 1. parameter bit EnableBypass = 1, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, localparam int CountWidth = $clog2(Depth + 1) ) ( input logic clk, @@ -47,10 +47,10 @@ module br_fifo_basic_fpv_monitor #( // ----------FV assumptions---------- `BR_ASSUME(pop_ready_liveness_a, s_eventually (pop_ready)) if (EnableCoverPushBackpressure) begin : gen_backpressure - if (EnableAssertPushValidStability) begin : gen_push_valid_stable + if (EnableAssumePushValidStability) 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 + if (EnableAssumePushDataStability) begin : gen_push_data_stable `BR_ASSUME(push_data_stable_a, push_valid && !push_ready |=> $stable(push_data)) end end else begin : gen_no_back_pressure @@ -72,10 +72,10 @@ module br_fifo_basic_fpv_monitor #( end // valid ready protocol check - if (EnableAssertPushValidStability) begin : gen_pop_valid_stable + if (EnableAssumePushValidStability) begin : gen_pop_valid_stable `BR_ASSERT(pop_valid_stable_a, pop_valid && !pop_ready |=> pop_valid) end - if (EnableAssertPushDataStability) begin : gen_pop_data_stable + if (EnableAssumePushDataStability) begin : gen_pop_data_stable `BR_ASSERT(pop_data_stable_a, pop_valid && !pop_ready |=> $stable(pop_data)) end diff --git a/fifo/fpv/br_fifo/br_fifo_ctrl_1r1w_fpv_monitor.sv b/fifo/fpv/br_fifo/br_fifo_ctrl_1r1w_fpv_monitor.sv index 5aa17a22a..781850cdb 100644 --- a/fifo/fpv/br_fifo/br_fifo_ctrl_1r1w_fpv_monitor.sv +++ b/fifo/fpv/br_fifo/br_fifo_ctrl_1r1w_fpv_monitor.sv @@ -23,8 +23,6 @@ module br_fifo_ctrl_1r1w_fpv_monitor #( // backing RAM is an SRAM of slightly larger depth than the FIFO depth). parameter int RamDepth = Depth, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, localparam int AddrWidth = br_math::clamped_clog2(RamDepth), localparam int CountWidth = $clog2(Depth + 1) ) ( @@ -94,9 +92,7 @@ module br_fifo_ctrl_1r1w_fpv_monitor #( .Depth(Depth), .Width(Width), .EnableBypass(EnableBypass), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) br_fifo_basic_fpv_monitor ( .clk, .rst, @@ -126,7 +122,5 @@ bind br_fifo_ctrl_1r1w br_fifo_ctrl_1r1w_fpv_monitor #( .RegisterPopOutputs(RegisterPopOutputs), .RamReadLatency(RamReadLatency), .RamDepth(RamDepth), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) monitor (.*); diff --git a/fifo/fpv/br_fifo/br_fifo_flops_fpv_monitor.sv b/fifo/fpv/br_fifo/br_fifo_flops_fpv_monitor.sv index fc8769339..857e377cd 100644 --- a/fifo/fpv/br_fifo/br_fifo_flops_fpv_monitor.sv +++ b/fifo/fpv/br_fifo/br_fifo_flops_fpv_monitor.sv @@ -18,8 +18,6 @@ module br_fifo_flops_fpv_monitor #( parameter int FlopRamReadDataDepthStages = 0, parameter int FlopRamReadDataWidthStages = 0, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, localparam int AddrWidth = $clog2(Depth), localparam int CountWidth = $clog2(Depth + 1) ) ( @@ -58,9 +56,7 @@ module br_fifo_flops_fpv_monitor #( .Depth(Depth), .Width(Width), .EnableBypass(EnableBypass), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) br_fifo_basic_fpv_monitor ( .clk, .rst, @@ -93,7 +89,5 @@ bind br_fifo_flops br_fifo_flops_fpv_monitor #( .FlopRamAddressDepthStages(FlopRamAddressDepthStages), .FlopRamReadDataDepthStages(FlopRamReadDataDepthStages), .FlopRamReadDataWidthStages(FlopRamReadDataWidthStages), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) monitor (.*); diff --git a/fifo/fpv/br_fifo_ext_arb/BUILD.bazel b/fifo/fpv/br_fifo_ext_arb/BUILD.bazel index 71ffb488f..19f1c54ea 100644 --- a/fifo/fpv/br_fifo_ext_arb/BUILD.bazel +++ b/fifo/fpv/br_fifo_ext_arb/BUILD.bazel @@ -98,8 +98,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -112,11 +112,11 @@ br_verilog_fpv_test_tools_suite( "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], diff --git a/fifo/fpv/br_fifo_ext_arb/br_fifo_shared_dynamic_ctrl_ext_arbiter_fpv_monitor.sv b/fifo/fpv/br_fifo_ext_arb/br_fifo_shared_dynamic_ctrl_ext_arbiter_fpv_monitor.sv index ce2332d6f..b6890528e 100644 --- a/fifo/fpv/br_fifo_ext_arb/br_fifo_shared_dynamic_ctrl_ext_arbiter_fpv_monitor.sv +++ b/fifo/fpv/br_fifo_ext_arb/br_fifo_shared_dynamic_ctrl_ext_arbiter_fpv_monitor.sv @@ -41,13 +41,6 @@ module br_fifo_shared_dynamic_ctrl_ext_arbiter_fpv_monitor #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // If 0, cover that push_data can be unstable. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. // ri lint_check_waive PARAM_NOT_USED @@ -167,9 +160,7 @@ module br_fifo_shared_dynamic_ctrl_ext_arbiter_fpv_monitor #( .Width(Width), .StagingBufferDepth(StagingBufferDepth), .HasStagingBuffer(HasStagingBuffer), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) fv_checker ( .clk, .rst, @@ -197,7 +188,5 @@ bind br_fifo_shared_dynamic_ctrl_ext_arbiter br_fifo_shared_dynamic_ctrl_ext_arb .DataRamReadLatency(DataRamReadLatency), .PointerRamReadLatency(PointerRamReadLatency), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/fifo/fpv/br_fifo_shared_dynamic/BUILD.bazel b/fifo/fpv/br_fifo_shared_dynamic/BUILD.bazel index f7c344e23..b9931a8bf 100644 --- a/fifo/fpv/br_fifo_shared_dynamic/BUILD.bazel +++ b/fifo/fpv/br_fifo_shared_dynamic/BUILD.bazel @@ -22,6 +22,7 @@ verilog_library( deps = [ ":br_fifo_shared_dynamic_basic_fpv_monitor", "//fifo/rtl:br_fifo_shared_dynamic_flops", + "//macros:br_asserts", "//macros:br_fv", ], ) @@ -122,8 +123,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -132,11 +133,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -377,8 +378,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -387,11 +388,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_basic_fpv_monitor.sv b/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_basic_fpv_monitor.sv index 9e3087a8f..a92502288 100644 --- a/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_basic_fpv_monitor.sv +++ b/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_basic_fpv_monitor.sv @@ -27,8 +27,6 @@ module br_fifo_shared_dynamic_basic_fpv_monitor #( parameter int StagingBufferDepth = 1, parameter bit HasStagingBuffer = 1, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, localparam int FifoIdWidth = br_math::clamped_clog2(NumFifos), localparam int AddrWidth = br_math::clamped_clog2(Depth) ) ( @@ -69,16 +67,7 @@ module br_fifo_shared_dynamic_basic_fpv_monitor #( // ----------FV assumptions---------- for (genvar i = 0; i < NumWritePorts; i++) begin : gen_asm `BR_ASSUME(push_fifo_id_legal_a, push_fifo_id[i] < NumFifos) - if (EnableCoverPushBackpressure) begin : gen_back_pressure - if (EnableAssertPushValidStability) begin : gen_push_valid_stable - `BR_ASSUME(push_valid_stable_a, push_valid[i] && !push_ready[i] |=> push_valid[i]) - end - if (EnableAssertPushDataStability) begin : gen_push_data_stable - `BR_ASSUME( - push_data_stable_a, - push_valid[i] && !push_ready[i] |=> $stable(push_data[i]) && $stable(push_fifo_id[i])) - end - end else begin : gen_no_backpressure + if (!EnableCoverPushBackpressure) begin : gen_no_back_pressure `BR_ASSUME(no_backpressure_a, push_valid[i] |-> push_ready[i]) end end diff --git a/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_ctrl_fpv_monitor.sv b/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_ctrl_fpv_monitor.sv index c114be94d..64502974c 100644 --- a/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_ctrl_fpv_monitor.sv +++ b/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_ctrl_fpv_monitor.sv @@ -36,13 +36,6 @@ module br_fifo_shared_dynamic_ctrl_fpv_monitor #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // If 0, cover that push_data can be unstable. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. // ri lint_check_waive PARAM_NOT_USED @@ -144,9 +137,7 @@ module br_fifo_shared_dynamic_ctrl_fpv_monitor #( .Width(Width), .StagingBufferDepth(StagingBufferDepth), .HasStagingBuffer(HasStagingBuffer), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) fv_checker ( .clk, .rst, @@ -173,7 +164,5 @@ bind br_fifo_shared_dynamic_ctrl br_fifo_shared_dynamic_ctrl_fpv_monitor #( .DataRamReadLatency(DataRamReadLatency), .PointerRamReadLatency(PointerRamReadLatency), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_flops_fpv_monitor.sv b/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_flops_fpv_monitor.sv index 2e39d72e8..3e142befd 100644 --- a/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_flops_fpv_monitor.sv +++ b/fifo/fpv/br_fifo_shared_dynamic/br_fifo_shared_dynamic_flops_fpv_monitor.sv @@ -53,13 +53,6 @@ module br_fifo_shared_dynamic_flops_fpv_monitor #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // If 0, cover that push_data can be unstable. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. // ri lint_check_waive PARAM_NOT_USED @@ -101,9 +94,7 @@ module br_fifo_shared_dynamic_flops_fpv_monitor #( .Width(Width), .StagingBufferDepth(StagingBufferDepth), .HasStagingBuffer(HasStagingBuffer), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) fv_checker ( .clk, .rst, @@ -138,7 +129,5 @@ bind br_fifo_shared_dynamic_flops br_fifo_shared_dynamic_flops_fpv_monitor #( .PointerRamReadDataDepthStages(PointerRamReadDataDepthStages), .PointerRamReadDataWidthStages(PointerRamReadDataWidthStages), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/fifo/fpv/br_fifo_shared_pstatic/BUILD.bazel b/fifo/fpv/br_fifo_shared_pstatic/BUILD.bazel index 8e87b609b..d6934a6f8 100644 --- a/fifo/fpv/br_fifo_shared_pstatic/BUILD.bazel +++ b/fifo/fpv/br_fifo_shared_pstatic/BUILD.bazel @@ -40,8 +40,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -50,11 +50,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -232,8 +232,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -242,11 +242,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_basic_fpv_monitor.sv b/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_basic_fpv_monitor.sv index 87236154f..3bffc8a55 100644 --- a/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_basic_fpv_monitor.sv +++ b/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_basic_fpv_monitor.sv @@ -15,8 +15,8 @@ module br_fifo_shared_pstatic_basic_fpv_monitor #( parameter bit RegisterPopOutputs = 0, parameter int RamReadLatency = 0, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, localparam int FifoIdWidth = br_math::clamped_clog2(NumFifos), localparam int AddrWidth = br_math::clamped_clog2(Depth) ) ( @@ -71,10 +71,10 @@ module br_fifo_shared_pstatic_basic_fpv_monitor #( `BR_ASSUME(push_fifo_id_legal_a, push_fifo_id < NumFifos) if (EnableCoverPushBackpressure) begin : gen_backpressure - if (EnableAssertPushValidStability) begin : gen_push_valid_stable + if (EnableAssumePushValidStability) 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 + if (EnableAssumePushDataStability) begin : gen_push_data_stable `BR_ASSUME(push_data_stable_a, push_valid && !push_ready |=> $stable(push_data) && $stable(push_fifo_id)) end @@ -101,11 +101,11 @@ module br_fifo_shared_pstatic_basic_fpv_monitor #( // ----------FV assertions---------- if ((RegisterPopOutputs != 0) || (RamReadLatency != 0)) begin : gen_pop - if (EnableAssertPushValidStability) begin : gen_pop_valid_stable + if (EnableAssumePushValidStability) begin : gen_pop_valid_stable `BR_ASSERT(pop_valid_stable_a, pop_valid[fv_fifo_id] && !pop_ready[fv_fifo_id] |=> pop_valid[fv_fifo_id]) end - if (EnableAssertPushDataStability) begin : gen_pop_data_stable + if (EnableAssumePushDataStability) begin : gen_pop_data_stable `BR_ASSERT(pop_data_stable_a, pop_valid[fv_fifo_id] && !pop_ready[fv_fifo_id] |=> $stable(pop_data[fv_fifo_id])) end diff --git a/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_ctrl_fpv_monitor.sv b/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_ctrl_fpv_monitor.sv index d295e75a6..459d45985 100644 --- a/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_ctrl_fpv_monitor.sv +++ b/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_ctrl_fpv_monitor.sv @@ -26,13 +26,6 @@ module br_fifo_shared_pstatic_ctrl_fpv_monitor #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // If 0, cover that push_data can be unstable. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. // ri lint_check_waive PARAM_NOT_USED @@ -119,9 +112,7 @@ module br_fifo_shared_pstatic_ctrl_fpv_monitor #( .StagingBufferDepth(StagingBufferDepth), .RegisterPopOutputs(RegisterPopOutputs), .RamReadLatency(RamReadLatency), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) fv_checker ( .clk, .rst, @@ -149,7 +140,5 @@ bind br_fifo_shared_pstatic_ctrl br_fifo_shared_pstatic_ctrl_fpv_monitor #( .RegisterPopOutputs(RegisterPopOutputs), .RamReadLatency(RamReadLatency), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_flops_fpv_monitor.sv b/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_flops_fpv_monitor.sv index 8b411a650..61cff2ff8 100644 --- a/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_flops_fpv_monitor.sv +++ b/fifo/fpv/br_fifo_shared_pstatic/br_fifo_shared_pstatic_flops_fpv_monitor.sv @@ -35,13 +35,6 @@ module br_fifo_shared_pstatic_flops_fpv_monitor #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // If 0, cover that push_data can be unstable. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted and that the FIFO is // empty at the end of the test. // ri lint_check_waive PARAM_NOT_USED @@ -101,9 +94,7 @@ module br_fifo_shared_pstatic_flops_fpv_monitor #( .StagingBufferDepth(StagingBufferDepth), .RegisterPopOutputs(RegisterPopOutputs), .RamReadLatency(RamReadLatency), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) fv_checker ( .clk, .rst, @@ -135,7 +126,5 @@ bind br_fifo_shared_pstatic_flops br_fifo_shared_pstatic_flops_fpv_monitor #( .RamReadDataDepthStages(RamReadDataDepthStages), .RamReadDataWidthStages(RamReadDataWidthStages), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/fifo/rtl/br_fifo_ctrl_1r1w.sv b/fifo/rtl/br_fifo_ctrl_1r1w.sv index 519a3de4c..a92cea81c 100644 --- a/fifo/rtl/br_fifo_ctrl_1r1w.sv +++ b/fifo/rtl/br_fifo_ctrl_1r1w.sv @@ -79,10 +79,6 @@ module br_fifo_ctrl_1r1w #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -159,8 +155,6 @@ module br_fifo_ctrl_1r1w #( .EnableBypass(EnableBypass), .RamDepth(RamDepth), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_push_ctrl ( diff --git a/fifo/rtl/br_fifo_flops.sv b/fifo/rtl/br_fifo_flops.sv index 12e324747..dbe370012 100644 --- a/fifo/rtl/br_fifo_flops.sv +++ b/fifo/rtl/br_fifo_flops.sv @@ -65,10 +65,6 @@ module br_fifo_flops #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -142,8 +138,6 @@ module br_fifo_flops #( .RamReadLatency(RamReadLatency), .RamDepth(RamDepth), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_ctrl_1r1w ( diff --git a/fifo/rtl/br_fifo_shared_dynamic_ctrl.sv b/fifo/rtl/br_fifo_shared_dynamic_ctrl.sv index 8f57ff324..24fee7751 100644 --- a/fifo/rtl/br_fifo_shared_dynamic_ctrl.sv +++ b/fifo/rtl/br_fifo_shared_dynamic_ctrl.sv @@ -80,11 +80,6 @@ module br_fifo_shared_dynamic_ctrl #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -160,8 +155,6 @@ module br_fifo_shared_dynamic_ctrl #( .Depth(Depth), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_shared_dynamic_push_ctrl ( diff --git a/fifo/rtl/br_fifo_shared_dynamic_ctrl_ext_arbiter.sv b/fifo/rtl/br_fifo_shared_dynamic_ctrl_ext_arbiter.sv index bafd7a60e..87acbdbe1 100644 --- a/fifo/rtl/br_fifo_shared_dynamic_ctrl_ext_arbiter.sv +++ b/fifo/rtl/br_fifo_shared_dynamic_ctrl_ext_arbiter.sv @@ -85,11 +85,6 @@ module br_fifo_shared_dynamic_ctrl_ext_arbiter #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -172,8 +167,6 @@ module br_fifo_shared_dynamic_ctrl_ext_arbiter #( .Depth(Depth), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_shared_dynamic_push_ctrl ( diff --git a/fifo/rtl/br_fifo_shared_dynamic_flops.sv b/fifo/rtl/br_fifo_shared_dynamic_flops.sv index 57087df9d..5604924be 100644 --- a/fifo/rtl/br_fifo_shared_dynamic_flops.sv +++ b/fifo/rtl/br_fifo_shared_dynamic_flops.sv @@ -101,11 +101,6 @@ module br_fifo_shared_dynamic_flops #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -225,8 +220,6 @@ module br_fifo_shared_dynamic_flops #( .DataRamReadLatency(DataRamReadLatency), .PointerRamReadLatency(PointerRamReadLatency), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_shared_dynamic_ctrl ( diff --git a/fifo/rtl/br_fifo_shared_pop_ctrl_ext_arbiter.sv b/fifo/rtl/br_fifo_shared_pop_ctrl_ext_arbiter.sv index 61d138d21..401f2b49b 100644 --- a/fifo/rtl/br_fifo_shared_pop_ctrl_ext_arbiter.sv +++ b/fifo/rtl/br_fifo_shared_pop_ctrl_ext_arbiter.sv @@ -202,7 +202,6 @@ module br_fifo_shared_pop_ctrl_ext_arbiter #( .Depth(Depth), .Width(Width), .RamReadLatency(RamReadLatency), - .EnableAssertPushValidStability(1), .ArbiterAlwaysGrants(ArbiterAlwaysGrants) ) br_fifo_shared_read_xbar ( .clk, diff --git a/fifo/rtl/br_fifo_shared_pstatic_ctrl.sv b/fifo/rtl/br_fifo_shared_pstatic_ctrl.sv index 8288a3371..fc6cb1f4e 100644 --- a/fifo/rtl/br_fifo_shared_pstatic_ctrl.sv +++ b/fifo/rtl/br_fifo_shared_pstatic_ctrl.sv @@ -58,11 +58,6 @@ module br_fifo_shared_pstatic_ctrl #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -148,8 +143,6 @@ module br_fifo_shared_pstatic_ctrl #( .Depth(Depth), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_shared_pstatic_push_ctrl ( diff --git a/fifo/rtl/br_fifo_shared_pstatic_flops.sv b/fifo/rtl/br_fifo_shared_pstatic_flops.sv index efb136925..309701b6b 100644 --- a/fifo/rtl/br_fifo_shared_pstatic_flops.sv +++ b/fifo/rtl/br_fifo_shared_pstatic_flops.sv @@ -68,11 +68,6 @@ module br_fifo_shared_pstatic_flops #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -167,8 +162,6 @@ module br_fifo_shared_pstatic_flops #( .RegisterPopOutputs(RegisterPopOutputs), .RamReadLatency(RamReadLatency), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_shared_pstatic_ctrl ( diff --git a/fifo/rtl/internal/br_fifo_push_ctrl.sv b/fifo/rtl/internal/br_fifo_push_ctrl.sv index 4c64b69b6..3413977a5 100644 --- a/fifo/rtl/internal/br_fifo_push_ctrl.sv +++ b/fifo/rtl/internal/br_fifo_push_ctrl.sv @@ -15,10 +15,6 @@ module br_fifo_push_ctrl #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = 1, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = 1, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -86,8 +82,6 @@ module br_fifo_push_ctrl #( .Width(Width), .EnableBypass(EnableBypass), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_push_ctrl_core ( diff --git a/fifo/rtl/internal/br_fifo_push_ctrl_core.sv b/fifo/rtl/internal/br_fifo_push_ctrl_core.sv index ebc1000a8..9ccbd24da 100644 --- a/fifo/rtl/internal/br_fifo_push_ctrl_core.sv +++ b/fifo/rtl/internal/br_fifo_push_ctrl_core.sv @@ -16,10 +16,6 @@ module br_fifo_push_ctrl_core #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -71,8 +67,8 @@ module br_fifo_push_ctrl_core #( .NumFlows(1), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( diff --git a/fifo/rtl/internal/br_fifo_shared_dynamic_push_ctrl.sv b/fifo/rtl/internal/br_fifo_shared_dynamic_push_ctrl.sv index 5663ec90c..4718df397 100644 --- a/fifo/rtl/internal/br_fifo_shared_dynamic_push_ctrl.sv +++ b/fifo/rtl/internal/br_fifo_shared_dynamic_push_ctrl.sv @@ -22,11 +22,6 @@ module br_fifo_shared_dynamic_push_ctrl #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. // ri lint_check_waive PARAM_NOT_USED parameter bit EnableAssertPushDataKnown = 1, @@ -79,8 +74,8 @@ module br_fifo_shared_dynamic_push_ctrl #( .NumFlows(NumWritePorts), .Width(Width + FifoIdWidth), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg_inst ( diff --git a/fifo/rtl/internal/br_fifo_shared_pstatic_push_ctrl.sv b/fifo/rtl/internal/br_fifo_shared_pstatic_push_ctrl.sv index 29a8dac9e..9a0cc44aa 100644 --- a/fifo/rtl/internal/br_fifo_shared_pstatic_push_ctrl.sv +++ b/fifo/rtl/internal/br_fifo_shared_pstatic_push_ctrl.sv @@ -21,11 +21,6 @@ module br_fifo_shared_pstatic_push_ctrl #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - // ri lint_check_waive PARAM_NOT_USED - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted and that the FIFO is @@ -73,8 +68,8 @@ module br_fifo_shared_pstatic_push_ctrl #( .NumFlows(1), .Width(Width + FifoIdWidth), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg_inst ( @@ -106,11 +101,6 @@ module br_fifo_shared_pstatic_push_ctrl #( // TODO(zhemao): Add bypass support. .EnableBypass(0), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - // Core can only have valid stability if the fifo_id is stable, - // so pass the data stability parameter instead of the - // valid stability parameter. - .EnableAssertPushValidStability(EnableAssertPushDataStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_fifo_push_ctrl_core_inst ( @@ -137,10 +127,6 @@ module br_fifo_shared_pstatic_push_ctrl #( .NumFlows(NumFifos), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - // push_fifo_id should always be stable if valid is stable. - .EnableAssertSelectStability(EnableAssertPushDataStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_demux_select_unstable_inst ( diff --git a/fifo/rtl/internal/br_fifo_shared_read_xbar.sv b/fifo/rtl/internal/br_fifo_shared_read_xbar.sv index 807b765be..7a09d0a6a 100644 --- a/fifo/rtl/internal/br_fifo_shared_read_xbar.sv +++ b/fifo/rtl/internal/br_fifo_shared_read_xbar.sv @@ -11,7 +11,6 @@ module br_fifo_shared_read_xbar #( parameter int RamReadLatency = 0, parameter int Depth = 2, parameter int Width = 1, - parameter bit EnableAssertPushValidStability = 0, parameter bit ArbiterAlwaysGrants = 1, localparam int AddrWidth = $clog2(Depth) ) ( @@ -66,9 +65,7 @@ module br_fifo_shared_read_xbar #( br_flow_demux_select_unstable #( .NumFlows(NumReadPorts), - .Width(AddrWidth), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertSelectStability(EnableAssertPushValidStability) + .Width(AddrWidth) ) br_flow_demux_select_unstable_inst ( .clk, .rst, @@ -103,8 +100,6 @@ module br_fifo_shared_read_xbar #( // If there is only one entry mapped to a port, it's impossible for more than one // FIFO to request to that port localparam bit EnableCoverMuxPushBackpressure = ReadPortEntries > 1; - localparam bit EnableAssertMuxPushValidStability = - EnableAssertPushValidStability && EnableCoverMuxPushBackpressure; logic [NumFifos-1:0] mux_push_ready; logic [NumFifos-1:0] mux_push_valid; @@ -122,8 +117,6 @@ module br_fifo_shared_read_xbar #( .NumFlows(NumFifos), .Width(TotalMuxWidth), .EnableCoverPushBackpressure(EnableCoverMuxPushBackpressure), - .EnableAssertPushValidStability(EnableAssertMuxPushValidStability), - .EnableAssertPushDataStability(EnableAssertMuxPushValidStability), .EnableCoverPopBackpressure(0), .ArbiterAlwaysGrants(ArbiterAlwaysGrants) ) br_flow_mux_core_inst ( diff --git a/fifo/sim/br_fifo_flops_push_credit_tb.sv b/fifo/sim/br_fifo_flops_push_credit_tb.sv index 517eec6b8..1fa661657 100644 --- a/fifo/sim/br_fifo_flops_push_credit_tb.sv +++ b/fifo/sim/br_fifo_flops_push_credit_tb.sv @@ -87,10 +87,7 @@ module br_fifo_flops_push_credit_tb (); br_credit_sender #( .Width(Width), - .MaxCredit(Depth), - // The test harness causes instability on the push_valid, - // so need to disable the stability check - .EnableAssertPushValidStability(0) + .MaxCredit(Depth) ) br_credit_sender ( .clk, .rst, diff --git a/fifo/sim/br_fifo_flops_tb.sv b/fifo/sim/br_fifo_flops_tb.sv index 11eb14676..dcfa9e2e3 100644 --- a/fifo/sim/br_fifo_flops_tb.sv +++ b/fifo/sim/br_fifo_flops_tb.sv @@ -46,10 +46,7 @@ module br_fifo_flops_tb; .Width(Width), .RegisterPopOutputs(RegisterPopOutputs), .EnableBypass(EnableBypass), - .FlopRamAddressDepthStages(FlopRamAddressDepthStages), - // The test harness causes instability on the push_valid, - // so need to disable the stability check - .EnableAssertPushValidStability(0) + .FlopRamAddressDepthStages(FlopRamAddressDepthStages) ) dut ( .clk(clk), .rst(rst), diff --git a/flow/fpv/arb/BUILD.bazel b/flow/fpv/arb/BUILD.bazel index e01cb3037..806e20684 100644 --- a/flow/fpv/arb/BUILD.bazel +++ b/flow/fpv/arb/BUILD.bazel @@ -34,14 +34,14 @@ br_verilog_fpv_test_tools_suite( name = "br_flow_arb_fixed_test_suite", illegal_param_combinations = { ( - "EnableAssertPushValidStability", + "EnableAssumePushValidStability", "EnableCoverPushBackpressure", ): [ ("1", "0"), ], }, params = { - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -85,14 +85,14 @@ br_verilog_fpv_test_tools_suite( name = "br_flow_arb_lru_test_suite", illegal_param_combinations = { ( - "EnableAssertPushValidStability", + "EnableAssumePushValidStability", "EnableCoverPushBackpressure", ): [ ("1", "0"), ], }, params = { - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -134,19 +134,7 @@ verilog_elab_test( br_verilog_fpv_test_tools_suite( name = "br_flow_arb_rr_test_suite", - illegal_param_combinations = { - ( - "EnableAssertPushValidStability", - "EnableCoverPushBackpressure", - ): [ - ("1", "0"), - ], - }, params = { - "EnableAssertPushValidStability": [ - "0", - "1", - ], "EnableCoverPushBackpressure": [ "0", "1", diff --git a/flow/fpv/arb/br_flow_arb_basic_fpv_monitor.sv b/flow/fpv/arb/br_flow_arb_basic_fpv_monitor.sv index b52ff0bbf..52bbfab3d 100644 --- a/flow/fpv/arb/br_flow_arb_basic_fpv_monitor.sv +++ b/flow/fpv/arb/br_flow_arb_basic_fpv_monitor.sv @@ -8,8 +8,7 @@ module br_flow_arb_basic_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 - parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure + parameter bit EnableCoverPushBackpressure = 1 ) ( input logic clk, input logic rst, @@ -24,15 +23,15 @@ module br_flow_arb_basic_fpv_monitor #( for (genvar n = 0; n < NumFlows; n++) begin : gen_asm if (!EnableCoverPushBackpressure) begin : gen_no_backpressure - `BR_ASSUME(no_backpressure_a, !push_ready[n] |-> !push_valid[n]) - end - if (EnableAssertPushValidStability) begin : gen_push_valid + // The design does not require stability, but the stateful arbiter model does. `BR_ASSUME(push_valid_stable_a, push_valid[n] && !push_ready[n] |=> push_valid[n]) + end else begin : gen_backpressure + `BR_ASSUME(no_backpressure_a, !push_ready[n] |-> !push_valid[n]) end end // ----------Sanity Check---------- - if (EnableAssertPushValidStability) begin : gen_pop_valid + if (EnableCoverPushBackpressure) begin : gen_pop_valid `BR_ASSERT(pop_valid_stable_a, pop_valid_unstable && !pop_ready |=> pop_valid_unstable) end diff --git a/flow/fpv/arb/br_flow_arb_fixed_fpv_monitor.sv b/flow/fpv/arb/br_flow_arb_fixed_fpv_monitor.sv index 3fc8e3862..66381cc11 100644 --- a/flow/fpv/arb/br_flow_arb_fixed_fpv_monitor.sv +++ b/flow/fpv/arb/br_flow_arb_fixed_fpv_monitor.sv @@ -9,7 +9,7 @@ module br_flow_arb_fixed_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -26,7 +26,7 @@ module br_flow_arb_fixed_fpv_monitor #( br_flow_arb_basic_fpv_monitor #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability) ) fv_checker ( .clk, .rst, @@ -50,6 +50,5 @@ endmodule : br_flow_arb_fixed_fpv_monitor bind br_flow_arb_fixed br_flow_arb_fixed_fpv_monitor #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/arb/br_flow_arb_lru_fpv_monitor.sv b/flow/fpv/arb/br_flow_arb_lru_fpv_monitor.sv index 4398ef509..131485b48 100644 --- a/flow/fpv/arb/br_flow_arb_lru_fpv_monitor.sv +++ b/flow/fpv/arb/br_flow_arb_lru_fpv_monitor.sv @@ -9,7 +9,7 @@ module br_flow_arb_lru_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -26,7 +26,7 @@ module br_flow_arb_lru_fpv_monitor #( br_flow_arb_basic_fpv_monitor #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability) ) fv_checker ( .clk, .rst, @@ -53,6 +53,5 @@ endmodule : br_flow_arb_lru_fpv_monitor bind br_flow_arb_lru br_flow_arb_lru_fpv_monitor #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/arb/br_flow_arb_rr_fpv_monitor.sv b/flow/fpv/arb/br_flow_arb_rr_fpv_monitor.sv index abd0f3724..923c83a3f 100644 --- a/flow/fpv/arb/br_flow_arb_rr_fpv_monitor.sv +++ b/flow/fpv/arb/br_flow_arb_rr_fpv_monitor.sv @@ -9,7 +9,6 @@ module br_flow_arb_rr_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -25,8 +24,7 @@ module br_flow_arb_rr_fpv_monitor #( // ----------Instantiate basic checks---------- br_flow_arb_basic_fpv_monitor #( .NumFlows(NumFlows), - .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability) + .EnableCoverPushBackpressure(EnableCoverPushBackpressure) ) fv_checker ( .clk, .rst, @@ -39,7 +37,7 @@ module br_flow_arb_rr_fpv_monitor #( // ----------Round Robin checks---------- rr_basic_fpv_monitor #( .NumRequesters(NumFlows), - .EnableAssertPushValidStability(EnableAssertPushValidStability) + .EnableAssumeRequestStability(EnableCoverPushBackpressure) ) rr_check ( .clk, .rst, @@ -53,6 +51,5 @@ endmodule : br_flow_arb_rr_fpv_monitor bind br_flow_arb_rr br_flow_arb_rr_fpv_monitor #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/demux/BUILD.bazel b/flow/fpv/demux/BUILD.bazel index 41e3b34c4..026f30911 100644 --- a/flow/fpv/demux/BUILD.bazel +++ b/flow/fpv/demux/BUILD.bazel @@ -35,8 +35,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", "EnableAssertSelectStability", ): [ ("0", "0", "0", "1"), @@ -52,11 +52,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -109,8 +109,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", "EnableAssertSelectStability", ): [ ("0", "0", "0", "1"), @@ -126,11 +126,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/flow/fpv/demux/br_flow_demux_basic_fpv_monitor.sv b/flow/fpv/demux/br_flow_demux_basic_fpv_monitor.sv index 32603a5d0..795d1ad91 100644 --- a/flow/fpv/demux/br_flow_demux_basic_fpv_monitor.sv +++ b/flow/fpv/demux/br_flow_demux_basic_fpv_monitor.sv @@ -10,9 +10,9 @@ module br_flow_demux_basic_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter int Width = 1, // Must be at least 1 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - parameter bit EnableAssertSelectStability = 0, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, + parameter bit EnableAssumeSelectStability = 0, parameter bit EnableAssertPopValidStability = 1, parameter bit EnableAssertPopDataStability = 1 ) ( @@ -36,10 +36,10 @@ module br_flow_demux_basic_fpv_monitor #( `BR_ASSUME(pop_ready_liveness_a, s_eventually (pop_ready[n])) end - if (EnableAssertPushValidStability) begin : gen_push_valid + if (EnableAssumePushValidStability) begin : gen_push_valid `BR_ASSUME(push_valid_stable_a, push_valid && !push_ready |=> push_valid) end - if (EnableAssertPushDataStability) begin : gen_push_data + if (EnableAssumePushDataStability) begin : gen_push_data `BR_ASSUME(push_data_stable_a, push_valid && !push_ready |=> $stable(push_data)) end @@ -47,7 +47,7 @@ module br_flow_demux_basic_fpv_monitor #( `BR_ASSUME(no_push_backpressure_a, !push_ready |-> !push_valid) end - if (EnableAssertSelectStability) begin : gen_select_stability + if (EnableAssumeSelectStability) begin : gen_select_stability `BR_ASSUME(select_stable_a, push_valid && !push_ready |=> $stable(select)) end diff --git a/flow/fpv/demux/br_flow_demux_select_fpv_monitor.sv b/flow/fpv/demux/br_flow_demux_select_fpv_monitor.sv index 1d5b297fb..dace97f75 100644 --- a/flow/fpv/demux/br_flow_demux_select_fpv_monitor.sv +++ b/flow/fpv/demux/br_flow_demux_select_fpv_monitor.sv @@ -11,9 +11,9 @@ module br_flow_demux_select_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter int Width = 1, // Must be at least 1 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - parameter bit EnableAssertSelectStability = 0, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, + parameter bit EnableAssumeSelectStability = 0, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -32,9 +32,9 @@ module br_flow_demux_select_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertSelectStability(EnableAssertSelectStability), + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), + .EnableAssumeSelectStability(EnableAssumeSelectStability), // Output flow reg ensures that pop is always stable .EnableAssertPopValidStability(1), .EnableAssertPopDataStability(1) @@ -67,8 +67,5 @@ bind br_flow_demux_select br_flow_demux_select_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertSelectStability(EnableAssertSelectStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/demux/br_flow_demux_select_unstable_fpv_monitor.sv b/flow/fpv/demux/br_flow_demux_select_unstable_fpv_monitor.sv index 1c24d5008..d0e98f03f 100644 --- a/flow/fpv/demux/br_flow_demux_select_unstable_fpv_monitor.sv +++ b/flow/fpv/demux/br_flow_demux_select_unstable_fpv_monitor.sv @@ -10,9 +10,9 @@ module br_flow_demux_select_unstable_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter int Width = 1, // Must be at least 1 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - parameter bit EnableAssertSelectStability = 0, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, + parameter bit EnableAssumeSelectStability = 0, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -31,11 +31,11 @@ module br_flow_demux_select_unstable_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertSelectStability(EnableAssertSelectStability), - .EnableAssertPopValidStability(EnableAssertPushValidStability && EnableAssertSelectStability), - .EnableAssertPopDataStability(EnableAssertPushDataStability && EnableAssertSelectStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), + .EnableAssumeSelectStability(EnableAssumeSelectStability), + .EnableAssertPopValidStability(EnableAssumePushValidStability && EnableAssumeSelectStability), + .EnableAssertPopDataStability(EnableAssumePushDataStability && EnableAssumeSelectStability) ) fv_checker ( .clk, .rst, @@ -62,8 +62,5 @@ bind br_flow_demux_select_unstable br_flow_demux_select_unstable_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertSelectStability(EnableAssertSelectStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/fork/BUILD.bazel b/flow/fpv/fork/BUILD.bazel index 92d899e43..28fb313f8 100644 --- a/flow/fpv/fork/BUILD.bazel +++ b/flow/fpv/fork/BUILD.bazel @@ -63,7 +63,7 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", + "EnableAssumePushValidStability", "EnableAssertSelectMultihotStability", ): [ ("0", "0", "1"), @@ -81,7 +81,7 @@ br_verilog_fpv_test_tools_suite( "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/flow/fpv/fork/br_flow_fork_fpv_monitor.sv b/flow/fpv/fork/br_flow_fork_fpv_monitor.sv index 46d41a79a..659e3de02 100644 --- a/flow/fpv/fork/br_flow_fork_fpv_monitor.sv +++ b/flow/fpv/fork/br_flow_fork_fpv_monitor.sv @@ -8,7 +8,6 @@ module br_flow_fork_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -30,10 +29,6 @@ module br_flow_fork_fpv_monitor #( `BR_ASSUME(pop_ready_liveness_a, s_eventually (pop_ready[n])) end - if (EnableAssertPushValidStability) begin : gen_push_valid - `BR_ASSUME(push_valid_stable_a, push_valid && !push_ready |=> push_valid) - end - if (!EnableCoverPushBackpressure) begin : gen_no_backpressure `BR_ASSUME(no_backpressure_a, !push_ready |-> !push_valid) end @@ -50,6 +45,5 @@ endmodule : br_flow_fork_fpv_monitor bind br_flow_fork br_flow_fork_fpv_monitor #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/fork/br_flow_fork_select_multihot_fpv_monitor.sv b/flow/fpv/fork/br_flow_fork_select_multihot_fpv_monitor.sv index c47ad3388..9781cbcd9 100644 --- a/flow/fpv/fork/br_flow_fork_select_multihot_fpv_monitor.sv +++ b/flow/fpv/fork/br_flow_fork_select_multihot_fpv_monitor.sv @@ -9,8 +9,6 @@ module br_flow_fork_select_multihot_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter bit EnableCoverSelectMultihot = 1, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertSelectMultihotStability = EnableAssertPushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -33,13 +31,6 @@ module br_flow_fork_select_multihot_fpv_monitor #( `BR_ASSUME(pop_ready_liveness_a, s_eventually (pop_ready[n])) end - if (EnableAssertPushValidStability) begin : gen_push_valid - `BR_ASSUME(push_valid_stable_a, push_valid && !push_ready |=> push_valid) - end - if (EnableAssertSelectMultihotStability) begin : gen_data - `BR_ASSUME(multihot_stable_a, push_valid && !push_ready |=> $stable(push_select_multihot)) - end - if (!EnableCoverSelectMultihot) begin : gen_1hot `BR_ASSUME(select_onehot_a, push_valid |-> $onehot(push_select_multihot)) end @@ -64,7 +55,5 @@ bind br_flow_fork_select_multihot br_flow_fork_select_multihot_fpv_monitor #( .NumFlows(NumFlows), .EnableCoverSelectMultihot(EnableCoverSelectMultihot), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertSelectMultihotStability(EnableAssertSelectMultihotStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/mux/BUILD.bazel b/flow/fpv/mux/BUILD.bazel index 6a5f03be4..33745029f 100644 --- a/flow/fpv/mux/BUILD.bazel +++ b/flow/fpv/mux/BUILD.bazel @@ -35,8 +35,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -45,11 +45,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -100,8 +100,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -110,11 +110,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -165,8 +165,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -175,11 +175,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -228,8 +228,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", "EnableAssertSelectStability", ): [ ("0", "0", "0", "1"), @@ -245,11 +245,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -302,8 +302,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", "EnableAssertSelectStability", ): [ ("0", "0", "0", "1"), @@ -319,11 +319,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -376,8 +376,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -386,11 +386,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -445,8 +445,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -455,11 +455,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -514,8 +514,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -524,11 +524,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/flow/fpv/mux/br_flow_mux_basic_fpv_monitor.sv b/flow/fpv/mux/br_flow_mux_basic_fpv_monitor.sv index d9ab8d1a3..47354a691 100644 --- a/flow/fpv/mux/br_flow_mux_basic_fpv_monitor.sv +++ b/flow/fpv/mux/br_flow_mux_basic_fpv_monitor.sv @@ -10,10 +10,10 @@ module br_flow_mux_basic_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter int Width = 1, // Must be at least 1 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableCoverPopBackpressure = EnableCoverPushBackpressure, - parameter bit EnableAssertPopValidStability = EnableAssertPushValidStability, + parameter bit EnableAssertPopValidStability = EnableAssumePushValidStability, parameter bit EnableAssertPopDataStability = 0, parameter bit EnableAssertMustGrant = 1, parameter bit DelayedGrant = 0 @@ -35,10 +35,10 @@ module br_flow_mux_basic_fpv_monitor #( if (!EnableCoverPushBackpressure) begin : gen_no_backpressure `BR_ASSUME(no_backpressure_a, !push_ready[n] |-> !push_valid[n]) end - if (EnableAssertPushValidStability) begin : gen_push_valid + if (EnableAssumePushValidStability) begin : gen_push_valid `BR_ASSUME(push_valid_stable_a, push_valid[n] && !push_ready[n] |=> push_valid[n]) end - if (EnableAssertPushDataStability) begin : gen_push_data + if (EnableAssumePushDataStability) begin : gen_push_data `BR_ASSUME(push_data_stable_a, push_valid[n] && !push_ready[n] |=> $stable(push_data[n])) end end diff --git a/flow/fpv/mux/br_flow_mux_fixed_fpv_monitor.sv b/flow/fpv/mux/br_flow_mux_fixed_fpv_monitor.sv index d6d83cfe2..fd85194dd 100644 --- a/flow/fpv/mux/br_flow_mux_fixed_fpv_monitor.sv +++ b/flow/fpv/mux/br_flow_mux_fixed_fpv_monitor.sv @@ -10,8 +10,8 @@ module br_flow_mux_fixed_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter int Width = 1, // Must be at least 1 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -29,8 +29,8 @@ module br_flow_mux_fixed_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), .EnableCoverPopBackpressure(EnableCoverPushBackpressure), // Pop data can never be stable .EnableAssertPopDataStability(0) @@ -65,7 +65,5 @@ bind br_flow_mux_fixed br_flow_mux_fixed_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/mux/br_flow_mux_fixed_stable_fpv_monitor.sv b/flow/fpv/mux/br_flow_mux_fixed_stable_fpv_monitor.sv index 20281e779..59867de5b 100644 --- a/flow/fpv/mux/br_flow_mux_fixed_stable_fpv_monitor.sv +++ b/flow/fpv/mux/br_flow_mux_fixed_stable_fpv_monitor.sv @@ -11,8 +11,8 @@ module br_flow_mux_fixed_stable_fpv_monitor #( parameter int Width = 1, // Must be at least 1 parameter bit RegisterPopReady = 0, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -30,8 +30,8 @@ module br_flow_mux_fixed_stable_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), .EnableCoverPopBackpressure(1), .EnableAssertPopValidStability(1), .EnableAssertPopDataStability(1), @@ -72,7 +72,5 @@ bind br_flow_mux_fixed_stable br_flow_mux_fixed_stable_fpv_monitor #( .Width(Width), .RegisterPopReady(RegisterPopReady), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/mux/br_flow_mux_lru_fpv_monitor.sv b/flow/fpv/mux/br_flow_mux_lru_fpv_monitor.sv index 1d84ce969..adfd56933 100644 --- a/flow/fpv/mux/br_flow_mux_lru_fpv_monitor.sv +++ b/flow/fpv/mux/br_flow_mux_lru_fpv_monitor.sv @@ -10,8 +10,8 @@ module br_flow_mux_lru_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter int Width = 1, // Must be at least 1 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -31,8 +31,8 @@ module br_flow_mux_lru_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), .EnableCoverPopBackpressure(EnableCoverPushBackpressure), .EnableAssertPopDataStability(0) ) fv_checker ( @@ -68,7 +68,5 @@ bind br_flow_mux_lru br_flow_mux_lru_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/mux/br_flow_mux_lru_stable_fpv_monitor.sv b/flow/fpv/mux/br_flow_mux_lru_stable_fpv_monitor.sv index e5a1ba6de..b899464f2 100644 --- a/flow/fpv/mux/br_flow_mux_lru_stable_fpv_monitor.sv +++ b/flow/fpv/mux/br_flow_mux_lru_stable_fpv_monitor.sv @@ -12,8 +12,8 @@ module br_flow_mux_lru_stable_fpv_monitor #( parameter int Width = 1, // Must be at least 1 parameter bit RegisterPopReady = 0, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -34,8 +34,8 @@ module br_flow_mux_lru_stable_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), .EnableCoverPopBackpressure(1), .EnableAssertPopValidStability(1), .EnableAssertPopDataStability(1), @@ -89,7 +89,5 @@ bind br_flow_mux_lru_stable br_flow_mux_lru_stable_fpv_monitor #( .Width(Width), .RegisterPopReady(RegisterPopReady), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/mux/br_flow_mux_rr_fpv_monitor.sv b/flow/fpv/mux/br_flow_mux_rr_fpv_monitor.sv index e2eedab0c..7f8f7adae 100644 --- a/flow/fpv/mux/br_flow_mux_rr_fpv_monitor.sv +++ b/flow/fpv/mux/br_flow_mux_rr_fpv_monitor.sv @@ -10,8 +10,8 @@ module br_flow_mux_rr_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter int Width = 1, // Must be at least 1 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -31,8 +31,8 @@ module br_flow_mux_rr_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), .EnableCoverPopBackpressure(EnableCoverPushBackpressure), .EnableAssertPopDataStability(0) ) fv_checker ( @@ -49,7 +49,7 @@ module br_flow_mux_rr_fpv_monitor #( // ----------Round Robin checks---------- rr_basic_fpv_monitor #( .NumRequesters(NumFlows), - .EnableAssertPushValidStability(EnableAssertPushValidStability) + .EnableAssumeRequestStability(EnableAssumePushValidStability) ) rr_check ( .clk, .rst, @@ -68,7 +68,5 @@ bind br_flow_mux_rr br_flow_mux_rr_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/mux/br_flow_mux_rr_stable_fpv_monitor.sv b/flow/fpv/mux/br_flow_mux_rr_stable_fpv_monitor.sv index 9323f685f..369cad4c2 100644 --- a/flow/fpv/mux/br_flow_mux_rr_stable_fpv_monitor.sv +++ b/flow/fpv/mux/br_flow_mux_rr_stable_fpv_monitor.sv @@ -11,8 +11,8 @@ module br_flow_mux_rr_stable_fpv_monitor #( parameter int Width = 1, // Must be at least 1 parameter bit RegisterPopReady = 0, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -33,8 +33,8 @@ module br_flow_mux_rr_stable_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), .EnableCoverPopBackpressure(1), .EnableAssertPopValidStability(1), .EnableAssertPopDataStability(1), @@ -53,7 +53,7 @@ module br_flow_mux_rr_stable_fpv_monitor #( // ----------Round Robin checks---------- rr_basic_fpv_monitor #( .NumRequesters(NumFlows), - .EnableAssertPushValidStability(EnableAssertPushValidStability) + .EnableAssumeRequestStability(EnableAssumePushValidStability) ) rr_check ( .clk, .rst, @@ -88,7 +88,5 @@ bind br_flow_mux_rr_stable br_flow_mux_rr_stable_fpv_monitor #( .Width(Width), .RegisterPopReady(RegisterPopReady), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/mux/br_flow_mux_select_fpv_monitor.sv b/flow/fpv/mux/br_flow_mux_select_fpv_monitor.sv index f53ae7c31..e4a6b375c 100644 --- a/flow/fpv/mux/br_flow_mux_select_fpv_monitor.sv +++ b/flow/fpv/mux/br_flow_mux_select_fpv_monitor.sv @@ -11,9 +11,9 @@ module br_flow_mux_select_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter int Width = 1, // Must be at least 1 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - parameter bit EnableAssertSelectStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, + parameter bit EnableAssumeSelectStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -32,8 +32,8 @@ module br_flow_mux_select_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), // Final flow mux stage ensures output is always stable .EnableAssertPopValidStability(1), .EnableAssertPopDataStability(1), @@ -52,7 +52,7 @@ module br_flow_mux_select_fpv_monitor #( // ----------FV assumptions---------- `BR_ASSUME(select_range_a, select < NumFlows) - if (EnableAssertSelectStability) begin : gen_stable_select + if (EnableAssumeSelectStability) begin : gen_stable_select `BR_ASSUME(select_stable_a, push_valid[select] && !push_ready[select] |=> $stable(select)) end @@ -70,8 +70,5 @@ bind br_flow_mux_select br_flow_mux_select_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertSelectStability(EnableAssertSelectStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/mux/br_flow_mux_select_unstable_fpv_monitor.sv b/flow/fpv/mux/br_flow_mux_select_unstable_fpv_monitor.sv index bd0517394..907f8570e 100644 --- a/flow/fpv/mux/br_flow_mux_select_unstable_fpv_monitor.sv +++ b/flow/fpv/mux/br_flow_mux_select_unstable_fpv_monitor.sv @@ -10,9 +10,9 @@ module br_flow_mux_select_unstable_fpv_monitor #( parameter int NumFlows = 2, // Must be at least 2 parameter int Width = 1, // Must be at least 1 parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - parameter bit EnableAssertSelectStability = 0, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, + parameter bit EnableAssumeSelectStability = 0, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -28,16 +28,16 @@ module br_flow_mux_select_unstable_fpv_monitor #( // ----------Instantiate basic checks---------- localparam bit EnableAssertPopValidStability = - EnableAssertPushValidStability && EnableAssertSelectStability; + EnableAssumePushValidStability && EnableAssumeSelectStability; localparam bit EnableAssertPopDataStability = - EnableAssertPopValidStability && EnableAssertPushDataStability; + EnableAssertPopValidStability && EnableAssumePushDataStability; br_flow_mux_basic_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), .EnableAssertPopValidStability(EnableAssertPopValidStability), .EnableAssertPopDataStability(EnableAssertPopDataStability), // Select can pick a flow that is not valid @@ -56,7 +56,7 @@ module br_flow_mux_select_unstable_fpv_monitor #( // ----------FV assumptions---------- `BR_ASSUME(select_range_a, select < NumFlows) - if (EnableAssertSelectStability) begin : gen_stable_select + if (EnableAssumeSelectStability) begin : gen_stable_select `BR_ASSUME(select_stable_a, push_valid[select] && !push_ready[select] |=> $stable(select)) end @@ -70,8 +70,5 @@ bind br_flow_mux_select_unstable br_flow_mux_select_unstable_fpv_monitor #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertSelectStability(EnableAssertSelectStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/reg/BUILD.bazel b/flow/fpv/reg/BUILD.bazel index 42c353e83..9b2de6a00 100644 --- a/flow/fpv/reg/BUILD.bazel +++ b/flow/fpv/reg/BUILD.bazel @@ -35,8 +35,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -45,11 +45,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -91,8 +91,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -101,11 +101,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -147,8 +147,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -157,11 +157,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -203,8 +203,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", ): [ ("0", "0", "1"), ("0", "1", "0"), @@ -213,11 +213,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/flow/fpv/reg/br_flow_reg_basic_fpv_monitor.sv b/flow/fpv/reg/br_flow_reg_basic_fpv_monitor.sv index 398710aa4..7f8cd3cfa 100644 --- a/flow/fpv/reg/br_flow_reg_basic_fpv_monitor.sv +++ b/flow/fpv/reg/br_flow_reg_basic_fpv_monitor.sv @@ -8,8 +8,8 @@ module br_flow_reg_basic_fpv_monitor #( parameter int Width = 1, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability ) ( input logic clk, input logic rst, @@ -28,18 +28,18 @@ module br_flow_reg_basic_fpv_monitor #( `BR_ASSUME(no_backpressure_a, !push_ready |-> !push_valid) end - if (EnableAssertPushValidStability) begin : gen_push_valid + if (EnableAssumePushValidStability) begin : gen_push_valid `BR_ASSUME(push_valid_stable_a, push_valid && !push_ready |=> push_valid) end - if (EnableAssertPushDataStability) begin : gen_push_data + if (EnableAssumePushDataStability) begin : gen_push_data `BR_ASSUME(push_data_stable_a, push_valid && !push_ready |=> $stable(push_data)) end // ----------Sanity Check---------- - if (EnableAssertPushValidStability) begin : gen_pop_valid + if (EnableAssumePushValidStability) begin : gen_pop_valid `BR_ASSERT(pop_valid_stable_a, pop_valid && !pop_ready |=> pop_valid) end - if (EnableAssertPushDataStability) begin : gen_pop_data + if (EnableAssumePushDataStability) begin : gen_pop_data `BR_ASSERT(pop_data_stable_a, pop_valid && !pop_ready |=> $stable(pop_data)) end diff --git a/flow/fpv/reg/br_flow_reg_both_fpv_monitor.sv b/flow/fpv/reg/br_flow_reg_both_fpv_monitor.sv index 93ab94226..8a00280ad 100644 --- a/flow/fpv/reg/br_flow_reg_both_fpv_monitor.sv +++ b/flow/fpv/reg/br_flow_reg_both_fpv_monitor.sv @@ -8,8 +8,8 @@ module br_flow_reg_both_fpv_monitor #( parameter int Width = 1, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -26,8 +26,8 @@ module br_flow_reg_both_fpv_monitor #( br_flow_reg_basic_fpv_monitor #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability) ) fv_checker ( .clk, .rst, @@ -48,7 +48,5 @@ endmodule : br_flow_reg_both_fpv_monitor bind br_flow_reg_both br_flow_reg_both_fpv_monitor #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/reg/br_flow_reg_fwd_fpv_monitor.sv b/flow/fpv/reg/br_flow_reg_fwd_fpv_monitor.sv index 7016cf9e9..f3800ba0a 100644 --- a/flow/fpv/reg/br_flow_reg_fwd_fpv_monitor.sv +++ b/flow/fpv/reg/br_flow_reg_fwd_fpv_monitor.sv @@ -8,8 +8,8 @@ module br_flow_reg_fwd_fpv_monitor #( parameter int Width = 1, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -26,8 +26,8 @@ module br_flow_reg_fwd_fpv_monitor #( br_flow_reg_basic_fpv_monitor #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability) ) fv_checker ( .clk, .rst, @@ -48,7 +48,5 @@ endmodule : br_flow_reg_fwd_fpv_monitor bind br_flow_reg_fwd br_flow_reg_fwd_fpv_monitor #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/reg/br_flow_reg_none_fpv_monitor.sv b/flow/fpv/reg/br_flow_reg_none_fpv_monitor.sv index 2d950f61a..96c7e5dcb 100644 --- a/flow/fpv/reg/br_flow_reg_none_fpv_monitor.sv +++ b/flow/fpv/reg/br_flow_reg_none_fpv_monitor.sv @@ -8,8 +8,8 @@ module br_flow_reg_none_fpv_monitor #( parameter int Width = 1, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -26,8 +26,8 @@ module br_flow_reg_none_fpv_monitor #( br_flow_reg_basic_fpv_monitor #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability) ) fv_checker ( .clk, .rst, @@ -48,7 +48,5 @@ endmodule : br_flow_reg_none_fpv_monitor bind br_flow_reg_none br_flow_reg_none_fpv_monitor #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/reg/br_flow_reg_rev_fpv_monitor.sv b/flow/fpv/reg/br_flow_reg_rev_fpv_monitor.sv index d6cc419ad..bdf2320a4 100644 --- a/flow/fpv/reg/br_flow_reg_rev_fpv_monitor.sv +++ b/flow/fpv/reg/br_flow_reg_rev_fpv_monitor.sv @@ -8,8 +8,8 @@ module br_flow_reg_rev_fpv_monitor #( parameter int Width = 1, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, parameter bit EnableAssertFinalNotValid = 1 ) ( input logic clk, @@ -26,8 +26,8 @@ module br_flow_reg_rev_fpv_monitor #( br_flow_reg_basic_fpv_monitor #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability) ) fv_checker ( .clk, .rst, @@ -48,7 +48,5 @@ endmodule : br_flow_reg_rev_fpv_monitor bind br_flow_reg_rev br_flow_reg_rev_fpv_monitor #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/xbar/BUILD.bazel b/flow/fpv/xbar/BUILD.bazel index 8947b7b39..ab35e0ed5 100644 --- a/flow/fpv/xbar/BUILD.bazel +++ b/flow/fpv/xbar/BUILD.bazel @@ -37,8 +37,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", "EnableAssertPushDestinationStability", ): [ ("0", "0", "0", "1"), @@ -54,11 +54,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -139,8 +139,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", "EnableAssertPushDestinationStability", ): [ ("0", "0", "0", "1"), @@ -156,11 +156,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], @@ -241,8 +241,8 @@ br_verilog_fpv_test_tools_suite( illegal_param_combinations = { ( "EnableCoverPushBackpressure", - "EnableAssertPushValidStability", - "EnableAssertPushDataStability", + "EnableAssumePushValidStability", + "EnableAssumePushDataStability", "EnableAssertPushDestinationStability", ): [ ("0", "0", "0", "1"), @@ -258,11 +258,11 @@ br_verilog_fpv_test_tools_suite( ], }, params = { - "EnableAssertPushDataStability": [ + "EnableAssumePushDataStability": [ "0", "1", ], - "EnableAssertPushValidStability": [ + "EnableAssumePushValidStability": [ "0", "1", ], diff --git a/flow/fpv/xbar/br_flow_xbar_basic_fpv_monitor.sv b/flow/fpv/xbar/br_flow_xbar_basic_fpv_monitor.sv index 1a223ad56..553ba4a0c 100644 --- a/flow/fpv/xbar/br_flow_xbar_basic_fpv_monitor.sv +++ b/flow/fpv/xbar/br_flow_xbar_basic_fpv_monitor.sv @@ -13,9 +13,9 @@ module br_flow_xbar_basic_fpv_monitor #( parameter bit RegisterDemuxOutputs = 0, parameter bit RegisterPopOutputs = 0, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - parameter bit EnableAssertPushDestinationStability = EnableAssertPushValidStability, + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, + parameter bit EnableAssumePushDestinationStability = EnableAssumePushValidStability, localparam int PushDestIdWidth = $clog2(NumPushFlows), localparam int DestIdWidth = $clog2(NumPopFlows) ) ( @@ -57,13 +57,13 @@ module br_flow_xbar_basic_fpv_monitor #( // but higher bits can be random value `BR_ASSUME(color_push_data_a, push_valid[i] |-> push_data[i][PushDestIdWidth-1:0] == i) if (EnableCoverPushBackpressure) begin : gen_push_backpressure - if (EnableAssertPushValidStability) begin : gen_push_valid + if (EnableAssumePushValidStability) begin : gen_push_valid `BR_ASSUME(push_valid_stable_a, push_valid[i] && !push_ready[i] |=> push_valid[i]) end - if (EnableAssertPushDataStability) begin : gen_push_data + if (EnableAssumePushDataStability) begin : gen_push_data `BR_ASSUME(push_data_stable_a, push_valid[i] && !push_ready[i] |=> $stable(push_data[i])) end - if (EnableAssertPushDestinationStability) begin : gen_push_dest_id + if (EnableAssumePushDestinationStability) begin : gen_push_dest_id `BR_ASSUME(push_dest_id_stable_a, push_valid[i] && !push_ready[i] |=> $stable(push_dest_id[i])) end @@ -78,7 +78,7 @@ module br_flow_xbar_basic_fpv_monitor #( // ----------Sanity Check---------- // if RegisterPopOutputs = 0, pop_valid could be unstable if push_valid or push_dest_id is unstable - if ((EnableAssertPushValidStability && EnableAssertPushDestinationStability) || + if ((EnableAssumePushValidStability && EnableAssumePushDestinationStability) || RegisterPopOutputs) begin : gen_pop_valid `BR_ASSERT(pop_valid_stable_a, pop_valid[fv_pop_id] && !pop_ready[fv_pop_id] |=> pop_valid[fv_pop_id]) diff --git a/flow/fpv/xbar/br_flow_xbar_fixed_fpv_monitor.sv b/flow/fpv/xbar/br_flow_xbar_fixed_fpv_monitor.sv index e28c56634..1ff8b3bfa 100644 --- a/flow/fpv/xbar/br_flow_xbar_fixed_fpv_monitor.sv +++ b/flow/fpv/xbar/br_flow_xbar_fixed_fpv_monitor.sv @@ -25,15 +25,12 @@ module br_flow_xbar_fixed_fpv_monitor #( // If 1, cover that the push_ready signal can be backpressured. // If 0, assert that push backpressure is not possible. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable. - // Otherwise, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable. - // Otherwise, cover that push_data can be unstable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that push_dest_id is stable. - // Otherwise, cover that push_dest_id can be unstable. - parameter bit EnableAssertPushDestinationStability = EnableAssertPushValidStability, + // If 1, assume that push_valid is stable. + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + // If 1, assume that push_data is stable. + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, + // If 1, assume that push_dest_id is stable. + parameter bit EnableAssumePushDestinationStability = EnableAssumePushValidStability, // If 1, assert that push_valid is 1 and all intermediate // register stages are empty at end of simulation. parameter bit EnableAssertFinalNotValid = 1, @@ -79,9 +76,9 @@ module br_flow_xbar_fixed_fpv_monitor #( .RegisterDemuxOutputs(RegisterDemuxOutputs), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertPushDestinationStability(EnableAssertPushDestinationStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), + .EnableAssumePushDestinationStability(EnableAssumePushDestinationStability) ) fv_checker ( .clk, .rst, @@ -118,8 +115,5 @@ bind br_flow_xbar_fixed br_flow_xbar_fixed_fpv_monitor #( .RegisterDemuxOutputs(RegisterDemuxOutputs), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertPushDestinationStability(EnableAssertPushDestinationStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/xbar/br_flow_xbar_lru_fpv_monitor.sv b/flow/fpv/xbar/br_flow_xbar_lru_fpv_monitor.sv index 8de5258dd..d9142ad69 100644 --- a/flow/fpv/xbar/br_flow_xbar_lru_fpv_monitor.sv +++ b/flow/fpv/xbar/br_flow_xbar_lru_fpv_monitor.sv @@ -25,15 +25,12 @@ module br_flow_xbar_lru_fpv_monitor #( // If 1, cover that the push_ready signal can be backpressured. // If 0, assert that push backpressure is not possible. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable. - // Otherwise, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable. - // Otherwise, cover that push_data can be unstable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that push_dest_id is stable. - // Otherwise, cover that push_dest_id can be unstable. - parameter bit EnableAssertPushDestinationStability = EnableAssertPushValidStability, + // If 1, assume that push_valid is stable. + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + // If 1, assume that push_data is stable. + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, + // If 1, assume that push_dest_id is stable. + parameter bit EnableAssumePushDestinationStability = EnableAssumePushValidStability, // If 1, assert that push_valid is 1 and all intermediate // register stages are empty at end of simulation. parameter bit EnableAssertFinalNotValid = 1, @@ -74,9 +71,9 @@ module br_flow_xbar_lru_fpv_monitor #( .RegisterDemuxOutputs(RegisterDemuxOutputs), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertPushDestinationStability(EnableAssertPushDestinationStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), + .EnableAssumePushDestinationStability(EnableAssumePushDestinationStability) ) fv_checker ( .clk, .rst, @@ -112,8 +109,5 @@ bind br_flow_xbar_lru br_flow_xbar_lru_fpv_monitor #( .RegisterDemuxOutputs(RegisterDemuxOutputs), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertPushDestinationStability(EnableAssertPushDestinationStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/fpv/xbar/br_flow_xbar_rr_fpv_monitor.sv b/flow/fpv/xbar/br_flow_xbar_rr_fpv_monitor.sv index 4cf2f6261..6c668db35 100644 --- a/flow/fpv/xbar/br_flow_xbar_rr_fpv_monitor.sv +++ b/flow/fpv/xbar/br_flow_xbar_rr_fpv_monitor.sv @@ -25,15 +25,12 @@ module br_flow_xbar_rr_fpv_monitor #( // If 1, cover that the push_ready signal can be backpressured. // If 0, assert that push backpressure is not possible. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable. - // Otherwise, cover that push_valid can be unstable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable. - // Otherwise, cover that push_data can be unstable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that push_dest_id is stable. - // Otherwise, cover that push_dest_id can be unstable. - parameter bit EnableAssertPushDestinationStability = EnableAssertPushValidStability, + // If 1, assume that push_valid is stable. + parameter bit EnableAssumePushValidStability = EnableCoverPushBackpressure, + // If 1, assume that push_data is stable. + parameter bit EnableAssumePushDataStability = EnableAssumePushValidStability, + // If 1, assume that push_dest_id is stable. + parameter bit EnableAssumePushDestinationStability = EnableAssumePushValidStability, // If 1, assert that push_valid is 1 and all intermediate // register stages are empty at end of simulation. parameter bit EnableAssertFinalNotValid = 1, @@ -74,9 +71,9 @@ module br_flow_xbar_rr_fpv_monitor #( .RegisterDemuxOutputs(RegisterDemuxOutputs), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertPushDestinationStability(EnableAssertPushDestinationStability) + .EnableAssumePushValidStability(EnableAssumePushValidStability), + .EnableAssumePushDataStability(EnableAssumePushDataStability), + .EnableAssumePushDestinationStability(EnableAssumePushDestinationStability) ) fv_checker ( .clk, .rst, @@ -95,7 +92,7 @@ module br_flow_xbar_rr_fpv_monitor #( rr_basic_fpv_monitor #( .NumRequesters(NumPushFlows), // Valid won't be stable at the arbiters if push_dest_id is unstable - .EnableAssertPushValidStability(EnableAssertPushDestinationStability) + .EnableAssumeRequestStability(EnableAssumePushDestinationStability) ) rr_check ( .clk, .rst, @@ -113,8 +110,5 @@ bind br_flow_xbar_rr br_flow_xbar_rr_fpv_monitor #( .RegisterDemuxOutputs(RegisterDemuxOutputs), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertPushDestinationStability(EnableAssertPushDestinationStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) monitor (.*); diff --git a/flow/rtl/br_flow_arb_fixed.sv b/flow/rtl/br_flow_arb_fixed.sv index a9f957343..aead2d11d 100644 --- a/flow/rtl/br_flow_arb_fixed.sv +++ b/flow/rtl/br_flow_arb_fixed.sv @@ -20,8 +20,6 @@ module br_flow_arb_fixed #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, // If 1, then assert there are no valid bits asserted at the end of the test. parameter bit EnableAssertFinalNotValid = 1 ) ( @@ -62,7 +60,6 @@ module br_flow_arb_fixed #( br_flow_arb_core #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_arb_core ( .clk, diff --git a/flow/rtl/br_flow_arb_lru.sv b/flow/rtl/br_flow_arb_lru.sv index 695217a40..a449bb6d5 100644 --- a/flow/rtl/br_flow_arb_lru.sv +++ b/flow/rtl/br_flow_arb_lru.sv @@ -22,8 +22,6 @@ module br_flow_arb_lru #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, // If 1, then assert there are no valid bits asserted at the end of the test. parameter bit EnableAssertFinalNotValid = 1 ) ( @@ -64,7 +62,6 @@ module br_flow_arb_lru #( br_flow_arb_core #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_arb_core ( .clk, diff --git a/flow/rtl/br_flow_arb_rr.sv b/flow/rtl/br_flow_arb_rr.sv index f093f9a95..79f974009 100644 --- a/flow/rtl/br_flow_arb_rr.sv +++ b/flow/rtl/br_flow_arb_rr.sv @@ -22,8 +22,6 @@ module br_flow_arb_rr #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, // If 1, then assert there are no valid bits asserted at the end of the test. parameter bit EnableAssertFinalNotValid = 1 ) ( @@ -64,7 +62,6 @@ module br_flow_arb_rr #( br_flow_arb_core #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_arb_core ( .clk, diff --git a/flow/rtl/br_flow_demux_select.sv b/flow/rtl/br_flow_demux_select.sv index a6e92a51c..ed9cbe6c6 100644 --- a/flow/rtl/br_flow_demux_select.sv +++ b/flow/rtl/br_flow_demux_select.sv @@ -22,13 +22,6 @@ module br_flow_demux_select #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that select is stable when backpressured. - // If 0, cover that select can be unstable. - parameter bit EnableAssertSelectStability = 0, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -65,9 +58,6 @@ module br_flow_demux_select #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertSelectStability(EnableAssertSelectStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_demux_select_unstable ( @@ -88,12 +78,6 @@ module br_flow_demux_select #( br_flow_reg_fwd #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - // We know that valid and data can be unstable internally. - // This register hides that instability from the pop interface. - .EnableAssertPushValidStability( - EnableAssertPushValidStability && EnableAssertSelectStability), - .EnableAssertPushDataStability( - EnableAssertPushDataStability && EnableAssertSelectStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_reg_fwd ( @@ -111,6 +95,7 @@ module br_flow_demux_select #( //------------------------------------------ // Implementation checks //------------------------------------------ + // Rely on submodule implementation checks endmodule : br_flow_demux_select diff --git a/flow/rtl/br_flow_demux_select_unstable.sv b/flow/rtl/br_flow_demux_select_unstable.sv index 08e2748b8..a3e2b7387 100644 --- a/flow/rtl/br_flow_demux_select_unstable.sv +++ b/flow/rtl/br_flow_demux_select_unstable.sv @@ -29,13 +29,6 @@ module br_flow_demux_select_unstable #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that select is stable when push is backpressured. - // If 0, cover that select can be unstable. - parameter bit EnableAssertSelectStability = 0, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -72,15 +65,11 @@ module br_flow_demux_select_unstable #( //------------------------------------------ `BR_ASSERT_STATIC(num_flows_must_be_at_least_one_a, NumFlows >= 1) `BR_ASSERT_STATIC(bit_width_must_be_at_least_one_a, Width >= 1) - `BR_ASSERT_STATIC(select_stability_implies_valid_stability_a, - !(EnableAssertSelectStability && !EnableAssertPushValidStability)) br_flow_checks_valid_data_intg #( .NumFlows(1), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( @@ -91,16 +80,6 @@ module br_flow_demux_select_unstable #( .data (push_data) ); - if (EnableCoverPushBackpressure && EnableAssertPushValidStability) begin : gen_select_checks - if (EnableAssertSelectStability) begin : gen_select_stability_check - `BR_ASSERT_INTG(select_stable_a, - (!push_ready && push_valid) |=> push_valid && $stable(select)) - end else begin : gen_select_instability_cover - `BR_COVER_INTG(select_unstable_c, - !push_ready && push_valid ##1 push_valid && !$stable(select)) - end - end - `BR_ASSERT_INTG(select_known_and_in_range_a, push_valid |-> (!$isunknown(select) && select < NumFlows)) @@ -134,22 +113,12 @@ module br_flow_demux_select_unstable #( //------------------------------------------ // Implementation checks //------------------------------------------ - if (EnableCoverPushBackpressure && EnableAssertPushValidStability && !EnableAssertSelectStability) - begin : gen_stable_push_valid - for (genvar i = 0; i < NumFlows; i++) begin : gen_pop_unstable_checks - `BR_ASSERT_IMPL( - pop_valid_instability_caused_by_select_a, - (!pop_ready[i] && pop_valid_unstable[i]) ##1 !pop_valid_unstable[i] |-> !$stable(select)) - end - end - br_flow_checks_valid_data_impl #( .NumFlows(NumFlows), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - // Pop valid and data can only be stable if select is stable. - .EnableAssertValidStability(EnableAssertPushValidStability && EnableAssertSelectStability), - .EnableAssertDataStability(EnableAssertPushDataStability && EnableAssertSelectStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_impl ( .clk, @@ -159,4 +128,13 @@ module br_flow_demux_select_unstable #( .data (pop_data_unstable) ); + if (EnableCoverPushBackpressure) begin : gen_impl_checks + for (genvar i = 0; i < NumFlows; i++) begin : gen_select_stability_asserts + `BR_COVER_IMPL(pop_valid_unstable_c, + !pop_ready[i] && pop_valid_unstable[i] ##1 !$stable(pop_valid_unstable[i])) + `BR_COVER_IMPL(pop_data_unstable_c, + !pop_ready[i] && pop_valid_unstable[i] ##1 !$stable(pop_data_unstable[i])) + end + end + endmodule : br_flow_demux_select_unstable diff --git a/flow/rtl/br_flow_fork.sv b/flow/rtl/br_flow_fork.sv index 24f4369e9..02a134a8d 100644 --- a/flow/rtl/br_flow_fork.sv +++ b/flow/rtl/br_flow_fork.sv @@ -16,8 +16,6 @@ module br_flow_fork #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, // If 1, then assert there are no valid bits asserted at the end of the test. parameter bit EnableAssertFinalNotValid = 1 ) ( @@ -49,9 +47,8 @@ module br_flow_fork #( .NumFlows(1), .Width(1), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - // Data is always stable when valid is since it is constant. - .EnableAssertDataStability(EnableAssertPushValidStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( .clk, @@ -84,7 +81,6 @@ module br_flow_fork #( .NumFlows(NumFlows), .Width(1), .EnableCoverBackpressure(EnableCoverPushBackpressure), - // We know that the pop valids can be unstable. .EnableAssertValidStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_impl ( @@ -96,7 +92,10 @@ module br_flow_fork #( ); if (EnableCoverPushBackpressure) begin : gen_push_backpressure_cover - `BR_COVER_IMPL(pop_valid_unstable_c, !$stable(pop_valid_unstable)) + for (genvar i = 0; i < NumFlows; i++) begin : gen_per_flow + `BR_COVER_IMPL(pop_valid_unstable_c, + !pop_ready[i] && pop_valid_unstable[i] ##1 !$stable(pop_valid_unstable[i])) + end end endmodule : br_flow_fork diff --git a/flow/rtl/br_flow_fork_select_multihot.sv b/flow/rtl/br_flow_fork_select_multihot.sv index 61c1225aa..1af3c8783 100644 --- a/flow/rtl/br_flow_fork_select_multihot.sv +++ b/flow/rtl/br_flow_fork_select_multihot.sv @@ -20,10 +20,6 @@ module br_flow_fork_select_multihot #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_select_multihot is stable when backpressured. - parameter bit EnableAssertSelectMultihotStability = EnableAssertPushValidStability, // If 1, then assert there are no valid bits asserted at the end of the test. parameter bit EnableAssertFinalNotValid = 1 ) ( @@ -59,8 +55,8 @@ module br_flow_fork_select_multihot #( .NumFlows(1), .Width(NumFlows), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertSelectMultihotStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( .clk, @@ -101,18 +97,11 @@ module br_flow_fork_select_multihot #( //------------------------------------------ // Implementation checks //------------------------------------------ - // Pop valid can be unstable because it will be revoked if a pop_ready falls. - // The only configuration for which it could be stable is if the select is stable - // and guaranteed to be onehot. - localparam bit EnableAssertPopValidStability = - EnableAssertPushValidStability && - EnableAssertSelectMultihotStability && - !EnableCoverSelectMultihot; br_flow_checks_valid_data_impl #( .NumFlows(NumFlows), .Width(1), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPopValidStability), + .EnableAssertValidStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_impl ( .clk, diff --git a/flow/rtl/br_flow_join.sv b/flow/rtl/br_flow_join.sv index a8413d23e..18f957ec0 100644 --- a/flow/rtl/br_flow_join.sv +++ b/flow/rtl/br_flow_join.sv @@ -15,8 +15,6 @@ module br_flow_join #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, // If 1, then assert there are no valid bits asserted at the end of the test. parameter bit EnableAssertFinalNotValid = 1 ) ( @@ -40,14 +38,12 @@ module br_flow_join #( //------------------------------------------ `BR_ASSERT_STATIC(num_flows_gte1_a, NumFlows >= 1) - br_flow_checks_valid_data_intg #( .NumFlows(NumFlows), .Width(1), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - // Data is always stable when valid is since it is constant. - .EnableAssertDataStability(EnableAssertPushValidStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( .clk, @@ -80,8 +76,8 @@ module br_flow_join #( .NumFlows(1), .Width(1), .EnableCoverBackpressure(1), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushValidStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_impl ( .clk, diff --git a/flow/rtl/br_flow_mux_fixed.sv b/flow/rtl/br_flow_mux_fixed.sv index 85f818499..4816c72bf 100644 --- a/flow/rtl/br_flow_mux_fixed.sv +++ b/flow/rtl/br_flow_mux_fixed.sv @@ -23,10 +23,6 @@ module br_flow_mux_fixed #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -75,8 +71,6 @@ module br_flow_mux_fixed #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_core ( diff --git a/flow/rtl/br_flow_mux_fixed_stable.sv b/flow/rtl/br_flow_mux_fixed_stable.sv index 0e4c7c792..1a75cf351 100644 --- a/flow/rtl/br_flow_mux_fixed_stable.sv +++ b/flow/rtl/br_flow_mux_fixed_stable.sv @@ -24,10 +24,6 @@ module br_flow_mux_fixed_stable #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -71,8 +67,6 @@ module br_flow_mux_fixed_stable #( .Width(Width), .RegisterPopReady(RegisterPopReady), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_core_stable ( diff --git a/flow/rtl/br_flow_mux_lru.sv b/flow/rtl/br_flow_mux_lru.sv index 2049adc7e..572fe1892 100644 --- a/flow/rtl/br_flow_mux_lru.sv +++ b/flow/rtl/br_flow_mux_lru.sv @@ -21,10 +21,6 @@ module br_flow_mux_lru #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -75,8 +71,6 @@ module br_flow_mux_lru #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_core ( diff --git a/flow/rtl/br_flow_mux_lru_stable.sv b/flow/rtl/br_flow_mux_lru_stable.sv index 6079eab54..6a9a18e36 100644 --- a/flow/rtl/br_flow_mux_lru_stable.sv +++ b/flow/rtl/br_flow_mux_lru_stable.sv @@ -23,10 +23,6 @@ module br_flow_mux_lru_stable #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -74,8 +70,6 @@ module br_flow_mux_lru_stable #( .Width(Width), .RegisterPopReady(RegisterPopReady), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_core_stable ( diff --git a/flow/rtl/br_flow_mux_rr.sv b/flow/rtl/br_flow_mux_rr.sv index ae4b11d41..ad9242df5 100644 --- a/flow/rtl/br_flow_mux_rr.sv +++ b/flow/rtl/br_flow_mux_rr.sv @@ -21,10 +21,6 @@ module br_flow_mux_rr #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -75,8 +71,6 @@ module br_flow_mux_rr #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_core ( diff --git a/flow/rtl/br_flow_mux_rr_stable.sv b/flow/rtl/br_flow_mux_rr_stable.sv index 4d43abb8c..37beb33a1 100644 --- a/flow/rtl/br_flow_mux_rr_stable.sv +++ b/flow/rtl/br_flow_mux_rr_stable.sv @@ -23,10 +23,6 @@ module br_flow_mux_rr_stable #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -74,8 +70,6 @@ module br_flow_mux_rr_stable #( .Width(Width), .RegisterPopReady(RegisterPopReady), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_core_stable ( diff --git a/flow/rtl/br_flow_mux_select.sv b/flow/rtl/br_flow_mux_select.sv index 9e84b3ab3..977f377a0 100644 --- a/flow/rtl/br_flow_mux_select.sv +++ b/flow/rtl/br_flow_mux_select.sv @@ -22,13 +22,6 @@ module br_flow_mux_select #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that select will not change when the selected push flow is backpressured. - // Otherwise, cover that select can be unstable. - parameter bit EnableAssertSelectStability = 0, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -68,9 +61,6 @@ module br_flow_mux_select #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertSelectStability(EnableAssertSelectStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_select_unstable ( @@ -85,17 +75,9 @@ module br_flow_mux_select #( .pop_data_unstable (internal_data_unstable) ); - // internal_valid could be unstable if push_valid or select is unstable. - localparam bit EnableAssertInternalValidStability = - EnableAssertPushValidStability && EnableAssertSelectStability; - localparam bit EnableAssertInternalDataStability = - EnableAssertInternalValidStability && EnableAssertPushDataStability; - br_flow_reg_fwd #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertInternalValidStability), - .EnableAssertPushDataStability(EnableAssertInternalDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_reg_fwd ( diff --git a/flow/rtl/br_flow_mux_select_unstable.sv b/flow/rtl/br_flow_mux_select_unstable.sv index 260950ae9..12bcd2a7a 100644 --- a/flow/rtl/br_flow_mux_select_unstable.sv +++ b/flow/rtl/br_flow_mux_select_unstable.sv @@ -32,13 +32,6 @@ module br_flow_mux_select_unstable #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that select will not change when the selected push flow is backpressured. - // Otherwise, cover that select can be unstable. - parameter bit EnableAssertSelectStability = 0, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -61,9 +54,8 @@ module br_flow_mux_select_unstable #( input logic pop_ready, // Unstable if select is changed while selected push flow is valid but not - // ready. This will be stable if EnableAssertSelectStability is 1. - // If pop stability is desired when push valid/select stability cannot be guaranteed, - // use br_flow_mux_select instead. + // ready. If pop stability is desired when push valid/select stability cannot + // be guaranteed, use br_flow_mux_select instead. output logic pop_valid_unstable, output logic [Width-1:0] pop_data_unstable ); @@ -73,8 +65,6 @@ module br_flow_mux_select_unstable #( //------------------------------------------ `BR_ASSERT_STATIC(num_flows_must_be_at_least_one_a, NumFlows >= 1) `BR_ASSERT_STATIC(width_gte_1_a, Width >= 1) - `BR_ASSERT_STATIC(select_only_stable_if_valid_stable_a, - EnableAssertPushValidStability || !EnableAssertSelectStability) `BR_ASSERT_INTG(select_in_range_a, select < NumFlows) @@ -82,8 +72,8 @@ module br_flow_mux_select_unstable #( .NumFlows(NumFlows), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( @@ -94,16 +84,6 @@ module br_flow_mux_select_unstable #( .data (push_data) ); - if (EnableCoverPushBackpressure && EnableAssertPushValidStability) begin : gen_select_checks - if (EnableAssertSelectStability) begin : gen_stable_select - `BR_ASSERT_INTG(select_stable_a, - push_valid[select] && !push_ready[select] |=> $stable(select)) - end else begin : gen_unstable_select - `BR_COVER_INTG(select_unstable_c, - push_valid[select] && !push_ready[select] ##1 !$stable(select)) - end - end - //------------------------------------------ // Implementation //------------------------------------------ @@ -126,37 +106,12 @@ module br_flow_mux_select_unstable #( //------------------------------------------ // Implementation checks //------------------------------------------ - if (EnableAssertPushValidStability && !EnableAssertSelectStability) - begin : gen_stable_push_valid_unstable_select - `BR_ASSERT_IMPL( - pop_valid_instability_caused_by_select_a, - ##1 !pop_ready && $stable(pop_ready) && $fell(pop_valid_unstable) |-> !$stable(select)) - if (EnableAssertPushDataStability) begin : gen_stable_push_data - `BR_ASSERT_IMPL(pop_data_instability_caused_by_select_a, - ##1 !pop_ready && pop_valid_unstable && $stable( - pop_ready - ) && $stable( - pop_valid_unstable - ) && !$stable( - pop_data_unstable - ) |-> !$stable( - select - )) - end - end - - // pop_valid could be unstable if push_valid or select is unstable. - localparam bit EnableAssertPopValidStability = - EnableAssertPushValidStability && EnableAssertSelectStability; - localparam bit EnableAssertPopDataStability = - EnableAssertPopValidStability && EnableAssertPushDataStability; - br_flow_checks_valid_data_impl #( .NumFlows(1), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPopValidStability), - .EnableAssertDataStability(EnableAssertPopDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_impl ( .clk, @@ -166,4 +121,9 @@ module br_flow_mux_select_unstable #( .data (pop_data_unstable) ); + `BR_COVER_IMPL(pop_valid_unstable_c, !pop_ready && pop_valid_unstable ##1 !$stable + (pop_valid_unstable)) + `BR_COVER_IMPL(pop_data_unstable_c, !pop_ready && pop_valid_unstable ##1 !$stable + (pop_data_unstable)) + endmodule : br_flow_mux_select_unstable diff --git a/flow/rtl/br_flow_reg_both.sv b/flow/rtl/br_flow_reg_both.sv index 4a9175a1e..1ae61b6e7 100644 --- a/flow/rtl/br_flow_reg_both.sv +++ b/flow/rtl/br_flow_reg_both.sv @@ -25,10 +25,6 @@ module br_flow_reg_both #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -68,8 +64,6 @@ module br_flow_reg_both #( br_flow_reg_rev #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_reg_rev ( @@ -89,8 +83,6 @@ module br_flow_reg_both #( // backpressuring the input. The rev stage will shield the fwd stage from // instability on the push interface. .EnableCoverPushBackpressure(1), - .EnableAssertPushValidStability(1), - .EnableAssertPushDataStability(1), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_reg_fwd ( diff --git a/flow/rtl/br_flow_reg_fwd.sv b/flow/rtl/br_flow_reg_fwd.sv index fe583e7f8..468db9208 100644 --- a/flow/rtl/br_flow_reg_fwd.sv +++ b/flow/rtl/br_flow_reg_fwd.sv @@ -27,10 +27,6 @@ module br_flow_reg_fwd #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -57,8 +53,8 @@ module br_flow_reg_fwd #( .NumFlows(1), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( diff --git a/flow/rtl/br_flow_reg_none.sv b/flow/rtl/br_flow_reg_none.sv index 8ac9ad848..0742a0cbe 100644 --- a/flow/rtl/br_flow_reg_none.sv +++ b/flow/rtl/br_flow_reg_none.sv @@ -30,10 +30,6 @@ module br_flow_reg_none #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -60,8 +56,8 @@ module br_flow_reg_none #( .NumFlows(1), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( diff --git a/flow/rtl/br_flow_reg_rev.sv b/flow/rtl/br_flow_reg_rev.sv index 5e566d8c0..91e18cc01 100644 --- a/flow/rtl/br_flow_reg_rev.sv +++ b/flow/rtl/br_flow_reg_rev.sv @@ -27,10 +27,6 @@ module br_flow_reg_rev #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -57,8 +53,8 @@ module br_flow_reg_rev #( .NumFlows(1), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( diff --git a/flow/rtl/br_flow_xbar_fixed.sv b/flow/rtl/br_flow_xbar_fixed.sv index 01af495e2..5a56dc8ea 100644 --- a/flow/rtl/br_flow_xbar_fixed.sv +++ b/flow/rtl/br_flow_xbar_fixed.sv @@ -34,13 +34,6 @@ module br_flow_xbar_fixed #( // If 1, cover that the push_ready signal can be backpressured. // If 0, assert that push backpressure is not possible. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that push_dest_id is stable. - // Otherwise, cover that push_dest_id can be unstable. - parameter bit EnableAssertPushDestinationStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, assert that push_valid is 1 and all intermediate @@ -82,9 +75,6 @@ module br_flow_xbar_fixed #( .RegisterDemuxOutputs(RegisterDemuxOutputs), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertPushDestinationStability(EnableAssertPushDestinationStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_xbar_core_inst ( diff --git a/flow/rtl/br_flow_xbar_lru.sv b/flow/rtl/br_flow_xbar_lru.sv index 72a716b5d..c92fd0da0 100644 --- a/flow/rtl/br_flow_xbar_lru.sv +++ b/flow/rtl/br_flow_xbar_lru.sv @@ -33,13 +33,6 @@ module br_flow_xbar_lru #( // If 1, cover that the push_ready signal can be backpressured. // If 0, assert that push backpressure is not possible. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that push_dest_id is stable. - // Otherwise, cover that push_dest_id can be unstable. - parameter bit EnableAssertPushDestinationStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, assert that push_valid is 1 and all intermediate @@ -82,9 +75,6 @@ module br_flow_xbar_lru #( .RegisterDemuxOutputs(RegisterDemuxOutputs), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertPushDestinationStability(EnableAssertPushDestinationStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_xbar_core_inst ( diff --git a/flow/rtl/br_flow_xbar_rr.sv b/flow/rtl/br_flow_xbar_rr.sv index 6fbb3e0fc..964024891 100644 --- a/flow/rtl/br_flow_xbar_rr.sv +++ b/flow/rtl/br_flow_xbar_rr.sv @@ -36,13 +36,6 @@ module br_flow_xbar_rr #( // If 1, cover that the push_ready signal can be backpressured. // If 0, assert that push backpressure is not possible. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable. - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - // If 1, assert that push_data is stable. - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - // If 1, assert that push_dest_id is stable. - // Otherwise, cover that push_dest_id can be unstable. - parameter bit EnableAssertPushDestinationStability = EnableAssertPushValidStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, assert that push_valid is 1 and all intermediate @@ -85,9 +78,6 @@ module br_flow_xbar_rr #( .RegisterDemuxOutputs(RegisterDemuxOutputs), .RegisterPopOutputs(RegisterPopOutputs), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertPushDestinationStability(EnableAssertPushDestinationStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_xbar_core_inst ( diff --git a/flow/rtl/internal/br_flow_arb_core.sv b/flow/rtl/internal/br_flow_arb_core.sv index 430e64ec8..0a72d2252 100644 --- a/flow/rtl/internal/br_flow_arb_core.sv +++ b/flow/rtl/internal/br_flow_arb_core.sv @@ -18,9 +18,6 @@ module br_flow_arb_core #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - // If 0, cover that push_valid can be unstable when backpressured. - parameter bit EnableAssertPushValidStability = 1, // If 1, then assert there are no valid bits asserted at the end of the test. parameter bit EnableAssertFinalNotValid = 1, // If 1, cover that the pop side experiences backpressure. @@ -53,9 +50,8 @@ module br_flow_arb_core #( .NumFlows(NumFlows), .Width(1), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - // Data is always stable when valid is stable since it is constant. - .EnableAssertDataStability(EnableAssertPushValidStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( .clk, @@ -92,19 +88,14 @@ module br_flow_arb_core #( //------------------------------------------ // Implementation checks //------------------------------------------ - localparam bit EnableAssertPopValidStability = - EnableCoverPopBackpressure && - EnableAssertPushValidStability; - br_flow_checks_valid_data_impl #( .NumFlows(1), .Width(1), // Since push_ready can only be true if pop_ready is, // pop side can only have backpressure if push side has backpressure. .EnableCoverBackpressure(EnableCoverPopBackpressure), - .EnableAssertValidStability(EnableAssertPopValidStability), - // Data is always stable when valid is stable since it is constant. - .EnableAssertDataStability(EnableAssertPopValidStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_impl ( .clk, @@ -120,6 +111,10 @@ module br_flow_arb_core #( |(push_valid & push_ready) |-> (pop_valid_unstable & pop_ready)) for (genvar i = 0; i < NumFlows; i++) begin : gen_per_flow_impl_checks `BR_ASSERT_IMPL(only_accept_on_grant_a, (push_valid[i] & push_ready[i]) |-> grant[i]) + if (EnableCoverPopBackpressure) begin : gen_cover_pop_unstable + `BR_COVER_IMPL(pop_unstable_c, + !pop_ready && pop_valid_unstable ##1 !$stable(pop_valid_unstable)) + end end endmodule : br_flow_arb_core diff --git a/flow/rtl/internal/br_flow_mux_core.sv b/flow/rtl/internal/br_flow_mux_core.sv index 78a3a2cc3..a7ffa2180 100644 --- a/flow/rtl/internal/br_flow_mux_core.sv +++ b/flow/rtl/internal/br_flow_mux_core.sv @@ -21,10 +21,6 @@ module br_flow_mux_core #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = 1, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = 1, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -69,8 +65,8 @@ module br_flow_mux_core #( .NumFlows(NumFlows), .Width(Width), .EnableCoverBackpressure(EnableCoverPushBackpressure), - .EnableAssertValidStability(EnableAssertPushValidStability), - .EnableAssertDataStability(EnableAssertPushDataStability), + .EnableAssertValidStability(0), + .EnableAssertDataStability(0), .EnableAssertDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_intg ( @@ -88,7 +84,6 @@ module br_flow_mux_core #( br_flow_arb_core #( .NumFlows(NumFlows), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), .EnableAssertFinalNotValid(EnableAssertFinalNotValid), .EnableCoverPopBackpressure(EnableCoverPopBackpressure), .ArbiterAlwaysGrants(ArbiterAlwaysGrants) @@ -117,16 +112,11 @@ module br_flow_mux_core #( //------------------------------------------ // Implementation checks //------------------------------------------ - localparam bit EnableAssertPopValidStability = - EnableCoverPopBackpressure && - EnableAssertPushValidStability; - br_flow_checks_valid_data_impl #( .NumFlows(1), .Width(Width), .EnableCoverBackpressure(EnableCoverPopBackpressure), - .EnableAssertValidStability(EnableAssertPopValidStability), - // pop_data_unstable is unstable regardless of whether push_data is stable + .EnableAssertValidStability(0), .EnableAssertDataStability(0), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_checks_valid_data_impl ( @@ -138,7 +128,10 @@ module br_flow_mux_core #( ); if (EnableCoverPopBackpressure) begin : gen_pop_data_unstable_cover - `BR_COVER_IMPL(pop_data_unstable_c, !$stable(pop_data_unstable)) + `BR_COVER_IMPL(pop_valid_unstable_c, + !pop_ready && pop_valid_unstable ##1 !$stable(pop_valid_unstable)) + `BR_COVER_IMPL(pop_data_unstable_c, + !pop_ready && pop_valid_unstable ##1 !$stable(pop_data_unstable)) end for (genvar i = 0; i < NumFlows; i++) begin : gen_data_selected_assert diff --git a/flow/rtl/internal/br_flow_mux_core_stable.sv b/flow/rtl/internal/br_flow_mux_core_stable.sv index cfcbdb96c..2fd341249 100644 --- a/flow/rtl/internal/br_flow_mux_core_stable.sv +++ b/flow/rtl/internal/br_flow_mux_core_stable.sv @@ -25,10 +25,6 @@ module br_flow_mux_core_stable #( // If 1, cover that the push side experiences backpressure. // If 0, assert that there is never backpressure. parameter bit EnableCoverPushBackpressure = 1, - // If 1, assert that push_valid is stable when backpressured. - parameter bit EnableAssertPushValidStability = 1, - // If 1, assert that push_data is stable when backpressured. - parameter bit EnableAssertPushDataStability = 1, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, // If 1, then assert there are no valid bits asserted at the end of the test. @@ -70,8 +66,6 @@ module br_flow_mux_core_stable #( .NumFlows(NumFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_core ( @@ -93,9 +87,6 @@ module br_flow_mux_core_stable #( br_flow_reg_both #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - // internal_pop_data cannot be stable - .EnableAssertPushDataStability(0), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_reg_both ( @@ -112,9 +103,6 @@ module br_flow_mux_core_stable #( br_flow_reg_fwd #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - // internal_pop_data cannot be stable - .EnableAssertPushDataStability(0), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_reg_fwd ( diff --git a/flow/rtl/internal/br_flow_xbar_core.sv b/flow/rtl/internal/br_flow_xbar_core.sv index e0f3ce697..c6209e124 100644 --- a/flow/rtl/internal/br_flow_xbar_core.sv +++ b/flow/rtl/internal/br_flow_xbar_core.sv @@ -12,9 +12,6 @@ module br_flow_xbar_core #( parameter bit RegisterDemuxOutputs = 0, parameter bit RegisterPopOutputs = 0, parameter bit EnableCoverPushBackpressure = 1, - parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure, - parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability, - parameter bit EnableAssertPushDestinationStability = EnableAssertPushDataStability, // If 1, assert that push_data is always known (not X) when push_valid is asserted. parameter bit EnableAssertPushDataKnown = 1, parameter bit EnableAssertFinalNotValid = 1, @@ -67,9 +64,6 @@ module br_flow_xbar_core #( .NumFlows(NumPopFlows), .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability(EnableAssertPushValidStability), - .EnableAssertPushDataStability(EnableAssertPushDataStability), - .EnableAssertSelectStability(EnableAssertPushDestinationStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_demux_select_unstable_push ( @@ -89,10 +83,6 @@ module br_flow_xbar_core #( br_flow_reg_fwd #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure), - .EnableAssertPushValidStability( - EnableAssertPushValidStability && EnableAssertPushDestinationStability), - .EnableAssertPushDataStability( - EnableAssertPushDataStability && EnableAssertPushDestinationStability), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_reg_fwd_demux_to_mux ( @@ -121,12 +111,6 @@ module br_flow_xbar_core #( // mux_in to be backpressured and mux_in_valid/data // must be stable. .EnableCoverPushBackpressure(EnableCoverPushBackpressure || RegisterDemuxOutputs), - .EnableAssertPushValidStability( - (EnableAssertPushValidStability && EnableAssertPushDestinationStability) || - RegisterDemuxOutputs), - .EnableAssertPushDataStability( - (EnableAssertPushDataStability && EnableAssertPushDestinationStability) || - RegisterDemuxOutputs), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_mux_core_pop ( @@ -148,11 +132,6 @@ module br_flow_xbar_core #( br_flow_reg_fwd #( .Width(Width), .EnableCoverPushBackpressure(EnableCoverPushBackpressure || RegisterDemuxOutputs), - .EnableAssertPushValidStability( - (EnableAssertPushValidStability && EnableAssertPushDestinationStability) || - RegisterDemuxOutputs), - // Push data cannot be stable because it comes from the arbiter - .EnableAssertPushDataStability(0), .EnableAssertPushDataKnown(EnableAssertPushDataKnown), .EnableAssertFinalNotValid(EnableAssertFinalNotValid) ) br_flow_reg_fwd_mux_to_pop ( diff --git a/tracker/rtl/br_tracker_freelist.sv b/tracker/rtl/br_tracker_freelist.sv index 7c24946fd..baabb71d1 100644 --- a/tracker/rtl/br_tracker_freelist.sv +++ b/tracker/rtl/br_tracker_freelist.sv @@ -217,13 +217,6 @@ module br_tracker_freelist #( // Staging buffer br_flow_reg_fwd #( .Width(EntryIdWidth), - .EnableAssertPushValidStability(1), - // Since the entry ID is coming from a priority encoder, - // it could be unstable if a higher priority entry is deallocated. - // This can only happen if there are more than two entries. - // If there are only two, only one entry can be unstaged when push_ready - // is low. - .EnableAssertPushDataStability(NumEntries <= 2), // Expect that alloc_valid can be 1 at end of test (or when idle, in general) .EnableAssertFinalNotValid(0) ) br_flow_reg_fwd (