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 @@ -397,6 +397,7 @@ module axi_burst_splitter_gran #(
// Assumptions and assertions
// --------------------------------------------------
`ifndef VERILATOR
`ifndef XSIM
// pragma translate_off
default disable iff (!rst_ni);
// Inputs
Expand All @@ -414,6 +415,7 @@ module axi_burst_splitter_gran #(
else $fatal(1, "AR burst longer than a single beat emitted!");
// pragma translate_on
`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 @@ -364,6 +364,7 @@ module axi_burst_unwrap #(
// Assumptions and assertions
// --------------------------------------------------
`ifndef VERILATOR
`ifndef XSIM
// pragma translate_off
default disable iff (!rst_ni);
// Inputs
Expand All @@ -379,6 +380,7 @@ module axi_burst_unwrap #(
cannot respond in protocol-compliant manner!");
// pragma translate_on
`endif
`endif

endmodule

Expand Down
2 changes: 1 addition & 1 deletion src/axi_demux_simple.sv
Original file line number Diff line number Diff line change
Expand Up @@ -460,13 +460,13 @@ module axi_demux_simple #(
// Validate parameters.
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
initial begin: validate_params
no_mst_ports: assume (NoMstPorts > 0) else
$fatal(1, "The Number of slaves (NoMstPorts) has to be at least 1");
AXI_ID_BITS: assume (AxiIdWidth >= AxiLookBits) else
$fatal(1, "AxiIdBits has to be equal or smaller than AxiIdWidth.");
end
`ifndef XSIM
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
2 changes: 1 addition & 1 deletion src/axi_err_slv.sv
Original file line number Diff line number Diff line change
Expand Up @@ -244,11 +244,11 @@ module axi_err_slv #(

// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
initial begin
assert (Resp == axi_pkg::RESP_DECERR || Resp == axi_pkg::RESP_SLVERR) else
$fatal(1, "This module may only generate RESP_DECERR or RESP_SLVERR responses!");
end
`ifndef XSIM
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
Expand Down
4 changes: 4 additions & 0 deletions src/axi_id_remap.sv
Original file line number Diff line number Diff line change
Expand Up @@ -382,6 +382,7 @@ module axi_id_remap #(
assert ($bits(mst_req_o.ar.id) == AxiMstPortIdWidth);
assert ($bits(mst_resp_i.r.id) == AxiMstPortIdWidth);
end
`ifndef XSIM
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 @@ -398,6 +399,7 @@ module axi_id_remap #(
assert property (@(posedge clk_i) mst_req_o.aw_valid && !mst_resp_i.aw_ready
|=> mst_req_o.aw_valid && $stable(mst_req_o.aw.id));
`endif
`endif
// pragma translate_on
endmodule

Expand Down Expand Up @@ -552,6 +554,7 @@ module axi_id_remap_table #(
// Assertions
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
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 @@ -570,6 +573,7 @@ module axi_id_remap_table #(
assert (IdxWidth >= 1);
end
`endif
`endif
// pragma translate_on

endmodule
Expand Down
2 changes: 2 additions & 0 deletions src/axi_isolate.sv
Original file line number Diff line number Diff line change
Expand Up @@ -392,6 +392,7 @@ module axi_isolate_inner #(
initial begin
assume (NumPending > 0) else $fatal(1, "At least one pending transaction required.");
end
`ifndef XSIM
default disable iff (!rst_ni);
aw_overflow: assert property (@(posedge clk_i)
(pending_aw_q == '1) |=> (pending_aw_q != '0)) else
Expand All @@ -406,6 +407,7 @@ module axi_isolate_inner #(
(pending_ar_q == '0) |=> (pending_ar_q != '1)) else
$fatal(1, "pending_ar_q underflowed");
`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 @@ -442,6 +442,7 @@ module axi_lite_demux #(

// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
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 @@ -464,6 +465,7 @@ module axi_lite_demux #(
|=> $stable(slv_ar_chan)) else
$fatal(1, "slv_aw_chan_select unstable with valid set.");
`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 @@ -464,6 +464,7 @@ module axi_lite_dw_converter #(
assume ($onehot(AxiSlvPortDataWidth)) else $fatal(1, "AxiSlvPortDataWidth must be power of 2");
assume ($onehot(AxiMstPortDataWidth)) else $fatal(1, "AxiMstPortDataWidth must be power of 2");
end
`ifndef XSIM
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 @@ -481,6 +482,7 @@ module axi_lite_dw_converter #(
(slv_res_o.r_valid && !slv_req_i.r_ready) |=> $stable(slv_res_o.r)) else
$fatal(1, "R must remain stable until handshake happened.");
`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 @@ -235,6 +235,7 @@ module axi_lite_from_mem #(
assert (DataWidth == $bits(axi_rsp_i.r.data)) else
$fatal(1, "DataWidth has to match axi_rsp_i.r.data!");
end
`ifndef XSIM
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 @@ -248,5 +249,6 @@ module axi_lite_from_mem #(
$fatal(1, "mem_be_i has to be stable if request is not granted!");
`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 @@ -380,6 +380,7 @@ module axi_lite_regs #(
// Validate parameters.
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
initial begin: p_assertions
assert (RegNumBytes > 32'd0) else
$fatal(1, "The number of bytes must be at least 1!");
Expand All @@ -402,6 +403,7 @@ module axi_lite_regs #(
else $fatal(1, "Read-only register at `byte_index: %0d` was changed by AXI!", i);
end
`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 @@ -114,6 +114,7 @@ module axi_lite_xbar #(
// make sure that the default slave does not get changed, if there is an unserved Ax
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
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 @@ -136,6 +137,7 @@ module axi_lite_xbar #(
else $fatal (1, $sformatf("It is not allowed to change the default mst port\
when there is an unserved Ar beat. Slave Port: %0d", i));
`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 @@ -197,6 +197,7 @@ module axi_serializer #(
assert (MaxWriteTxns >= 1)
else $fatal(1, "Maximum number of write transactions must be >= 1!");
end
`ifndef XSIM
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 @@ -214,6 +215,7 @@ module axi_serializer #(
(mst_resp_i.r_valid & mst_req_o.r_ready |-> slv_resp_o.r_valid & slv_req_i.r_ready))
else $error("R beat lost.");
`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 @@ -567,6 +567,7 @@ module axi_to_detailed_mem #(
// Assertions
// pragma translate_off
`ifndef VERILATOR
`ifndef XSIM
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 @@ -592,6 +593,7 @@ module axi_to_detailed_mem #(
assert property (@(posedge clk_i) meta_valid && meta.atop != '0 |-> meta.write)
else $warning("Unexpected atomic operation on read.");
`endif
`endif
// pragma translate_on
endmodule

Expand Down