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

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion arb/fpv/arb_basic_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,6 @@
`include "br_fv.svh"

module arb_basic_fpv_monitor #(
// Must be at least 1
parameter int NumRequesters = 1
) (
input logic clk,
Expand Down
1 change: 0 additions & 1 deletion arb/fpv/br_arb_fixed_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,6 @@
`include "br_fv.svh"

module br_arb_fixed_fpv_monitor #(
// Must be at least 1
parameter int NumRequesters = 1
) (
input logic clk,
Expand Down
4 changes: 2 additions & 2 deletions arb/fpv/lru_basic_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@
`include "br_fv.svh"

module lru_basic_fpv_monitor #(
// Must be at least 2
parameter int NumRequesters = 2,
// Must be at least 1
parameter int NumRequesters = 1,
// If 1, cover that request is multihot,
// Otherwise, assume that it is onehot
parameter bit EnableCoverRequestMultihot = 1
Expand Down
38 changes: 22 additions & 16 deletions arb/fpv/rr_basic_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@
`include "br_fv.svh"

module rr_basic_fpv_monitor #(
// Must be at least 2
parameter int NumRequesters = 2,
// Must be at least 1
parameter int NumRequesters = 1,
parameter bit EnableAssertPushValidStability = 1
) (
input logic clk,
Expand All @@ -21,29 +21,35 @@ module rr_basic_fpv_monitor #(

// ----------FV Modeling Code----------
logic [$clog2(NumRequesters)-1:0] i, j;
if (NumRequesters > 1) begin : gen_ij
`BR_FV_2RAND_IDX(i, j, NumRequesters)
end else begin : gen_i
assign i = 0;
end
logic [NumRequesters-1:0] high_priority_request;

`BR_FV_2RAND_IDX(i, j, NumRequesters)
`BR_REGL(high_priority_request,
(grant == 1 << (NumRequesters - 1)) ? NumRequesters'(1) : grant << 1,
`BR_REGL(high_priority_request, (grant == 1 << (NumRequesters - 1)) ? 'd1 : grant << 1,
(grant != 0) && enable_priority_update)

// ----------Sanity Check----------
// High priority request must be grant the same cycle
`BR_ASSERT(high_priority_grant_a, request[i] && high_priority_request[i] |-> grant[i])

// ----------Fairness Check----------
`BR_ASSERT(arb_priority_a,
grant[j] |-> !request[i] || // high_priority ... j ... i
((2 ** j >= high_priority_request) && (2 ** i > high_priority_request) && (j < i)) ||
// i ... high_priority ... j
((2 ** j >= high_priority_request) && (2 ** i < high_priority_request)) ||
// j ... i ... high_priority ...
((2 ** j <= high_priority_request) && (2 ** i < high_priority_request) && (j < i)))

if (EnableAssertPushValidStability) begin : gen_req_stable
`BR_ASSERT(round_robin_a,
request[i] |-> not (!grant[i] && enable_priority_update throughout grant[j] [-> 2]))
if (NumRequesters > 1) begin : gen_multi_req
`BR_ASSERT(arb_priority_a,
grant[j] |-> !request[i] || // high_priority ... j ... i
((2 ** j >= high_priority_request) && (2 ** i > high_priority_request) && (j < i)) ||
// i ... high_priority ... j
((2 ** j >= high_priority_request) && (2 ** i < high_priority_request)) ||
// j ... i ... high_priority ...
((2 ** j <= high_priority_request) && (2 ** i < high_priority_request) && (j < i)))

if (EnableAssertPushValidStability) begin : gen_req_stable
`BR_ASSERT(
round_robin_a,
request[i] |-> not (!grant[i] && enable_priority_update throughout grant[j] [-> 2]))
end
end

// ----------Critical Covers----------
Expand Down
3 changes: 3 additions & 0 deletions flow/fpv/arb/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -101,6 +102,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -152,6 +154,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down
2 changes: 1 addition & 1 deletion flow/fpv/arb/br_flow_arb_basic_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
`include "br_fv.svh"

module br_flow_arb_basic_fpv_monitor #(
parameter int NumFlows = 2, // Must be at least 2
parameter int NumFlows = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure
) (
Expand Down
16 changes: 9 additions & 7 deletions flow/fpv/arb/br_flow_arb_fixed_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
`include "br_fv.svh"

module br_flow_arb_fixed_fpv_monitor #(
parameter int NumFlows = 2, // Must be at least 2
parameter int NumFlows = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
parameter bit EnableAssertFinalNotValid = 1
Expand Down Expand Up @@ -36,13 +36,15 @@ module br_flow_arb_fixed_fpv_monitor #(
.pop_valid_unstable
);

// ----------FV Modeling Code----------
logic [$clog2(NumFlows)-1:0] i, j;
`BR_FV_2RAND_IDX(i, j, NumFlows)
if (NumFlows > 1) begin : gen_multi_req
// ----------FV Modeling Code----------
logic [$clog2(NumFlows)-1:0] i, j;
`BR_FV_2RAND_IDX(i, j, NumFlows)

// ----------Fairness Check----------
if (EnableCoverPushBackpressure) begin : gen_strict_priority_check
`BR_ASSERT(strict_priority_a, (i < j) && push_valid[i] && push_valid[j] |-> !grant[j])
// ----------Fairness Check----------
if (EnableCoverPushBackpressure) begin : gen_strict_priority_check
`BR_ASSERT(strict_priority_a, (i < j) && push_valid[i] && push_valid[j] |-> !grant[j])
end
end

endmodule : br_flow_arb_fixed_fpv_monitor
Expand Down
2 changes: 1 addition & 1 deletion flow/fpv/arb/br_flow_arb_lru_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
`include "br_fv.svh"

module br_flow_arb_lru_fpv_monitor #(
parameter int NumFlows = 2, // Must be at least 2
parameter int NumFlows = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
parameter bit EnableAssertFinalNotValid = 1
Expand Down
2 changes: 1 addition & 1 deletion flow/fpv/arb/br_flow_arb_rr_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@
`include "br_fv.svh"

module br_flow_arb_rr_fpv_monitor #(
parameter int NumFlows = 2, // Must be at least 2
parameter int NumFlows = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
parameter bit EnableAssertFinalNotValid = 1
Expand Down
2 changes: 2 additions & 0 deletions flow/fpv/demux/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -143,6 +144,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down
4 changes: 2 additions & 2 deletions flow/fpv/demux/br_flow_demux_basic_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
`include "br_fv.svh"

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 int NumFlows = 1,
parameter int Width = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability,
Expand Down
4 changes: 2 additions & 2 deletions flow/fpv/demux/br_flow_demux_select_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -8,8 +8,8 @@
`include "br_fv.svh"

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 int NumFlows = 1,
parameter int Width = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability,
Expand Down
4 changes: 2 additions & 2 deletions flow/fpv/demux/br_flow_demux_select_unstable_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
`include "br_fv.svh"

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 int NumFlows = 1,
parameter int Width = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability,
Expand Down
2 changes: 2 additions & 0 deletions flow/fpv/fork/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -90,6 +91,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down
2 changes: 1 addition & 1 deletion flow/fpv/fork/br_flow_fork_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
`include "br_asserts.svh"

module br_flow_fork_fpv_monitor #(
parameter int NumFlows = 2, // Must be at least 2
parameter int NumFlows = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
parameter bit EnableAssertFinalNotValid = 1
Expand Down
2 changes: 1 addition & 1 deletion flow/fpv/fork/br_flow_fork_select_multihot_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@
`include "br_asserts.svh"

module br_flow_fork_select_multihot_fpv_monitor #(
parameter int NumFlows = 2, // Must be at least 2
parameter int NumFlows = 1,
parameter bit EnableCoverSelectMultihot = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
Expand Down
8 changes: 8 additions & 0 deletions flow/fpv/mux/BUILD.bazel
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -123,6 +124,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -188,6 +190,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -262,6 +265,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -336,6 +340,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -399,6 +404,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -468,6 +474,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down Expand Up @@ -537,6 +544,7 @@ br_verilog_fpv_test_tools_suite(
"1",
],
"NumFlows": [
"1",
"2",
"4",
"5",
Expand Down
4 changes: 2 additions & 2 deletions flow/fpv/mux/br_flow_mux_basic_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
`include "br_fv.svh"

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 int NumFlows = 1,
parameter int Width = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability,
Expand Down
22 changes: 14 additions & 8 deletions flow/fpv/mux/br_flow_mux_fixed_fpv_monitor.sv
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@
`include "br_fv.svh"

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 int NumFlows = 1,
parameter int Width = 1,
parameter bit EnableCoverPushBackpressure = 1,
parameter bit EnableAssertPushValidStability = EnableCoverPushBackpressure,
parameter bit EnableAssertPushDataStability = EnableAssertPushValidStability,
Expand Down Expand Up @@ -47,15 +47,21 @@ module br_flow_mux_fixed_fpv_monitor #(

// ----------FV Modeling Code----------
logic [$clog2(NumFlows)-1:0] i, j;
`BR_FV_2RAND_IDX(i, j, NumFlows)
if (NumFlows > 1) begin : gen_ij
`BR_FV_2RAND_IDX(i, j, NumFlows)
end else begin : gen_i
assign i = '0;
end

// ----------Fairness Check----------
// verilog_lint: waive-start line-length
if (EnableCoverPushBackpressure) begin : gen_strict_priority_check
`BR_ASSERT(strict_priority_a,
(i < j) && push_valid[i] && push_valid[j] |-> (pop_data_unstable == push_data[i]) || !push_ready[i])
end else begin : gen_no_conflict_check
`BR_ASSERT(no_conflict_a, i != j |-> !(push_valid[i] && push_valid[j]))
if (NumFlows > 1) begin : gen_multi_req
if (EnableCoverPushBackpressure) begin : gen_strict_priority_check
`BR_ASSERT(strict_priority_a,
(i < j) && push_valid[i] && push_valid[j] |-> (pop_data_unstable == push_data[i]) || !push_ready[i])
end else begin : gen_no_conflict_check
`BR_ASSERT(no_conflict_a, i != j |-> !(push_valid[i] && push_valid[j]))
end
end
// verilog_lint: waive-stop line-length

Expand Down
Loading