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

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions src/axi_burst_splitter_gran.sv
Original file line number Diff line number Diff line change
Expand Up @@ -396,6 +396,7 @@ module axi_burst_splitter_gran #(
// --------------------------------------------------
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
// pragma translate_off
default disable iff (!rst_ni);
// Inputs
Expand All @@ -414,6 +415,7 @@ module axi_burst_splitter_gran #(
// pragma translate_on
`endif
`endif
`endif

endmodule

Expand Down
2 changes: 2 additions & 0 deletions src/axi_burst_unwrap.sv
Original file line number Diff line number Diff line change
Expand Up @@ -365,6 +365,7 @@ module axi_burst_unwrap #(
// --------------------------------------------------
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
// pragma translate_off
default disable iff (!rst_ni);
// Inputs
Expand All @@ -381,6 +382,7 @@ module axi_burst_unwrap #(
// pragma translate_on
`endif
`endif
`endif

endmodule

Expand Down
2 changes: 2 additions & 0 deletions src/axi_demux_id_counters.sv
Original file line number Diff line number Diff line change
Expand Up @@ -133,13 +133,15 @@ module axi_demux_id_counters #(
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
// Validate parameters.
cnt_underflow: assert property(
@(posedge clk_i) disable iff (~rst_ni) (pop_en[i] |=> !overflow)) else
$fatal(1, "axi_demux_id_counters > Counter: %0d underflowed.\
The reason is probably a faulty AXI response.", i);
`endif
`endif
`endif
// pragma translate_on
end
endmodule
Expand Down
2 changes: 2 additions & 0 deletions src/axi_demux_simple.sv
Original file line number Diff line number Diff line change
Expand Up @@ -469,6 +469,7 @@ module axi_demux_simple #(
$fatal(1, "AxiIdBits has to be equal or smaller than AxiIdWidth.");
end
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (!rst_ni);
aw_select: assume property( @(posedge clk_i) (slv_req_i.aw_valid |->
(slv_aw_select_i < NoMstPorts))) else
Expand Down Expand Up @@ -507,6 +508,7 @@ module axi_demux_simple #(
`ASSUME(NoAtopAllowed, !AtopSupport && slv_req_i.aw_valid |-> slv_req_i.aw.atop == '0)
`endif
`endif
`endif
// pragma translate_on
end
endmodule
2 changes: 2 additions & 0 deletions src/axi_err_slv.sv
Original file line number Diff line number Diff line change
Expand Up @@ -249,13 +249,15 @@ module axi_err_slv #(
$fatal(1, "This module may only generate RESP_DECERR or RESP_SLVERR responses!");
end
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (!rst_ni);
if (!ATOPs) begin : gen_assert_atops_unsupported
assume property( @(posedge clk_i) (slv_req_i.aw_valid |-> slv_req_i.aw.atop == '0)) else
$fatal(1, "Got ATOP but not configured to support ATOPs!");
end
`endif
`endif
`endif
// pragma translate_on

endmodule
4 changes: 4 additions & 0 deletions src/axi_id_remap.sv
Original file line number Diff line number Diff line change
Expand Up @@ -383,6 +383,7 @@ module axi_id_remap #(
assert ($bits(mst_resp_i.r.id) == AxiMstPortIdWidth);
end
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (!rst_ni);
assert property (@(posedge clk_i) slv_req_i.aw_valid && slv_resp_o.aw_ready
|-> mst_req_o.aw_valid && mst_resp_i.aw_ready);
Expand All @@ -400,6 +401,7 @@ module axi_id_remap #(
|=> mst_req_o.aw_valid && $stable(mst_req_o.aw.id));
`endif
`endif
`endif
// pragma translate_on
endmodule

Expand Down Expand Up @@ -555,6 +557,7 @@ module axi_id_remap_table #(
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (!rst_ni);
assume property (@(posedge clk_i) push_i |->
table_q[push_oup_id_i].cnt == '0 || table_q[push_oup_id_i].inp_id == push_inp_id_i)
Expand All @@ -574,6 +577,7 @@ module axi_id_remap_table #(
end
`endif
`endif
`endif
// pragma translate_on

endmodule
Expand Down
4 changes: 4 additions & 0 deletions src/axi_interleaved_xbar.sv
Original file line number Diff line number Diff line change
Expand Up @@ -164,6 +164,7 @@ import cf_math_pkg::idx_width;
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (~rst_ni);
default_aw_mst_port_en: assert property(
@(posedge clk_i) (slv_ports_req_i[i].aw_valid && !slv_ports_resp_o[i].aw_ready)
Expand All @@ -187,6 +188,7 @@ import cf_math_pkg::idx_width;
"when there is an unserved Ar beat. Slave Port: %0d"}, i));
`endif
`endif
`endif
// pragma translate_on
axi_demux #(
.AxiIdWidth ( Cfg.AxiIdWidthSlvPorts ), // ID Width
Expand Down Expand Up @@ -303,6 +305,7 @@ import cf_math_pkg::idx_width;
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
initial begin : check_params
id_slv_req_ports: assert ($bits(slv_ports_req_i[0].aw.id ) == Cfg.AxiIdWidthSlvPorts) else
$fatal(1, $sformatf("Slv_req and aw_chan id width not equal."));
Expand All @@ -311,6 +314,7 @@ import cf_math_pkg::idx_width;
end
`endif
`endif
`endif
// pragma translate_on
endmodule : axi_interleaved_xbar

Expand Down
2 changes: 2 additions & 0 deletions src/axi_isolate.sv
Original file line number Diff line number Diff line change
Expand Up @@ -393,6 +393,7 @@ module axi_isolate_inner #(
assume (NumPending > 0) else $fatal(1, "At least one pending transaction required.");
end
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (!rst_ni);
aw_overflow: assert property (@(posedge clk_i)
(pending_aw_q == '1) |=> (pending_aw_q != '0)) else
Expand All @@ -408,6 +409,7 @@ module axi_isolate_inner #(
$fatal(1, "pending_ar_q underflowed");
`endif
`endif
`endif
// pragma translate_on
endmodule

Expand Down
2 changes: 2 additions & 0 deletions src/axi_lite_demux.sv
Original file line number Diff line number Diff line change
Expand Up @@ -443,6 +443,7 @@ module axi_lite_demux #(
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (!rst_ni);
aw_select: assume property( @(posedge clk_i) (slv_req_i.aw_valid |->
(slv_aw_select_i < NoMstPorts))) else
Expand All @@ -466,6 +467,7 @@ module axi_lite_demux #(
$fatal(1, "slv_aw_chan_select unstable with valid set.");
`endif
`endif
`endif
// pragma translate_on
end

Expand Down
2 changes: 2 additions & 0 deletions src/axi_lite_dw_converter.sv
Original file line number Diff line number Diff line change
Expand Up @@ -465,6 +465,7 @@ module axi_lite_dw_converter #(
assume ($onehot(AxiMstPortDataWidth)) else $fatal(1, "AxiMstPortDataWidth must be power of 2");
end
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (~rst_ni);
stable_aw: assert property (@(posedge clk_i)
(mst_req_o.aw_valid && !mst_res_i.aw_ready) |=> $stable(mst_req_o.aw)) else
Expand All @@ -483,6 +484,7 @@ module axi_lite_dw_converter #(
$fatal(1, "R must remain stable until handshake happened.");
`endif
`endif
`endif
// pragma translate_on
endmodule

Expand Down
2 changes: 2 additions & 0 deletions src/axi_lite_from_mem.sv
Original file line number Diff line number Diff line change
Expand Up @@ -236,6 +236,7 @@ module axi_lite_from_mem #(
$fatal(1, "DataWidth has to match axi_rsp_i.r.data!");
end
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (~rst_ni);
assert property (@(posedge clk_i) (mem_req_i && !mem_gnt_o) |=> mem_req_i) else
$fatal(1, "It is not allowed to deassert the request if it was not granted!");
Expand All @@ -250,5 +251,6 @@ module axi_lite_from_mem #(
`endif
`endif
`endif
`endif
// pragma translate_on
endmodule
2 changes: 2 additions & 0 deletions src/axi_lite_regs.sv
Original file line number Diff line number Diff line change
Expand Up @@ -381,6 +381,7 @@ module axi_lite_regs #(
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
initial begin: p_assertions
assert (RegNumBytes > 32'd0) else
$fatal(1, "The number of bytes must be at least 1!");
Expand All @@ -404,6 +405,7 @@ module axi_lite_regs #(
end
`endif
`endif
`endif
// pragma translate_on
endmodule

Expand Down
2 changes: 2 additions & 0 deletions src/axi_lite_xbar.sv
Original file line number Diff line number Diff line change
Expand Up @@ -115,6 +115,7 @@ module axi_lite_xbar #(
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (~rst_ni);
default_aw_mst_port_en: assert property(
@(posedge clk_i) (slv_ports_req_i[i].aw_valid && !slv_ports_resp_o[i].aw_ready)
Expand All @@ -138,6 +139,7 @@ module axi_lite_xbar #(
when there is an unserved Ar beat. Slave Port: %0d", i));
`endif
`endif
`endif
// pragma translate_on
axi_lite_demux #(
.aw_chan_t ( aw_chan_t ), // AW Channel Type
Expand Down
2 changes: 2 additions & 0 deletions src/axi_serializer.sv
Original file line number Diff line number Diff line change
Expand Up @@ -198,6 +198,7 @@ module axi_serializer #(
else $fatal(1, "Maximum number of write transactions must be >= 1!");
end
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (~rst_ni);
aw_lost : assert property( @(posedge clk_i)
(slv_req_i.aw_valid & slv_resp_o.aw_ready |-> mst_req_o.aw_valid & mst_resp_i.aw_ready))
Expand All @@ -216,6 +217,7 @@ module axi_serializer #(
else $error("R beat lost.");
`endif
`endif
`endif
// pragma translate_on
endmodule

Expand Down
2 changes: 2 additions & 0 deletions src/axi_to_detailed_mem.sv
Original file line number Diff line number Diff line change
Expand Up @@ -568,6 +568,7 @@ module axi_to_detailed_mem #(
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (!rst_ni);
assume property (@(posedge clk_i)
axi_req_i.ar_valid && !axi_resp_o.ar_ready |=> $stable(axi_req_i.ar))
Expand All @@ -594,6 +595,7 @@ module axi_to_detailed_mem #(
else $warning("Unexpected atomic operation on read.");
`endif
`endif
`endif
// pragma translate_on
endmodule

Expand Down
4 changes: 4 additions & 0 deletions src/axi_xbar_unmuxed.sv
Original file line number Diff line number Diff line change
Expand Up @@ -137,6 +137,7 @@ import cf_math_pkg::idx_width;
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
default disable iff (~rst_ni);
default_aw_mst_port_en: assert property(
@(posedge clk_i) (slv_ports_req_i[i].aw_valid && !slv_ports_resp_o[i].aw_ready)
Expand All @@ -160,6 +161,7 @@ import cf_math_pkg::idx_width;
when there is an unserved Ar beat. Slave Port: %0d", i));
`endif
`endif
`endif
// pragma translate_on
axi_demux #(
.AxiIdWidth ( Cfg.AxiIdWidthSlvPorts ), // ID Width
Expand Down Expand Up @@ -256,6 +258,7 @@ import cf_math_pkg::idx_width;
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
`ifndef XILINX_SIMULATOR
initial begin : check_params
id_slv_req_ports: assert ($bits(slv_ports_req_i[0].aw.id ) == Cfg.AxiIdWidthSlvPorts) else
$fatal(1, $sformatf("Slv_req and aw_chan id width not equal."));
Expand All @@ -264,6 +267,7 @@ import cf_math_pkg::idx_width;
end
`endif
`endif
`endif
// pragma translate_on
endmodule

Expand Down