Enable assertions in Verilator after migrating to Verilator v5. (#1185)

This commit is contained in:
Zbigniew Chamski 2023-04-19 09:35:40 +02:00 committed by GitHub
parent 6c8b4a9566
commit a0893bce2b
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
6 changed files with 15 additions and 27 deletions

View file

@ -293,14 +293,12 @@ module axi_shim #(
// ----------------
//pragma translate_off
`ifndef VERILATOR
initial begin
assert (AxiNumWords >= 1) else
$fatal(1, "[axi adapter] AxiNumWords must be >= 1");
assert (AxiIdWidth >= 2) else
$fatal(1, "[axi adapter] AXI id width must be at least 2 bit wide");
end
`endif
initial begin
assert (AxiNumWords >= 1) else
$fatal(1, "[axi adapter] AxiNumWords must be >= 1");
assert (AxiIdWidth >= 2) else
$fatal(1, "[axi adapter] AXI id width must be at least 2 bit wide");
end
//pragma translate_on
endmodule // axi_adapter2

View file

@ -1275,11 +1275,9 @@ module csr_regfile import ariane_pkg::*; #(
// Assertions
//-------------
//pragma translate_off
`ifndef VERILATOR
// check that eret and ex are never valid together
assert property (
@(posedge clk_i) disable iff (!rst_ni !== '0) !(eret_o && ex_i.valid))
// check that eret and ex are never valid together
assert property (
@(posedge clk_i) disable iff (!rst_ni !== '0) !(eret_o && ex_i.valid))
else begin $error("eret and exception should never be valid at the same time"); $stop(); end
`endif
//pragma translate_on
endmodule

View file

@ -526,17 +526,15 @@ module issue_read_operands import ariane_pkg::*; #(
end
//pragma translate_off
`ifndef VERILATOR
initial begin
assert (NR_RGPR_PORTS == 2 || (NR_RGPR_PORTS == 3 && CVXIF_PRESENT))
else $fatal(1, "If CVXIF is enable, ariane regfile can have either 2 or 3 read ports. Else it has 2 read ports.");
end
assert property (
assert property (
@(posedge clk_i) (branch_valid_q) |-> (!$isunknown(operand_a_q) && !$isunknown(operand_b_q)))
else $warning ("Got unknown value in one of the operands");
`endif
//pragma translate_on
endmodule

View file

@ -381,12 +381,11 @@ module load_unit import ariane_pkg::*; #(
end
// end result mux fast
///////////////////////////////////////////////////////
// assertions
///////////////////////////////////////////////////////
///////////////////////////////////////////////////////
// assertions
///////////////////////////////////////////////////////
//pragma translate_off
`ifndef VERILATOR
//pragma translate_off
// check invalid offsets
addr_offset0: assert property (@(posedge clk_i) disable iff (~rst_ni)
valid_o |-> (load_data_q.operation inside {ariane_pkg::LW, ariane_pkg::LWU}) |-> load_data_q.address_offset < 5) else $fatal (1,"invalid address offset used with {LW, LWU}");
@ -394,7 +393,6 @@ module load_unit import ariane_pkg::*; #(
valid_o |-> (load_data_q.operation inside {ariane_pkg::LH, ariane_pkg::LHU}) |-> load_data_q.address_offset < 7) else $fatal (1,"invalid address offset used with {LH, LHU}");
addr_offset2: assert property (@(posedge clk_i) disable iff (~rst_ni)
valid_o |-> (load_data_q.operation inside {ariane_pkg::LB, ariane_pkg::LBU}) |-> load_data_q.address_offset < 8) else $fatal (1,"invalid address offset used with {LB, LBU}");
`endif
//pragma translate_on
//pragma translate_on
endmodule

View file

@ -404,7 +404,6 @@ module scoreboard #(
end
//pragma translate_off
`ifndef VERILATOR
initial begin
assert (NR_ENTRIES == 2**BITS_ENTRIES) else $fatal(1, "Scoreboard size needs to be a power of two.");
end
@ -436,6 +435,5 @@ module scoreboard #(
else $fatal (1,"Two or more functional units are retiring instructions with the same transaction id!");
end
end
`endif
//pragma translate_on
endmodule

View file

@ -258,7 +258,6 @@ module store_buffer import ariane_pkg::*; (
///////////////////////////////////////////////////////
//pragma translate_off
`ifndef VERILATOR
// assert that commit is never set when we are flushing this would be counter intuitive
// as flush and commit is decided in the same stage
commit_and_flush: assert property (
@ -276,7 +275,6 @@ module store_buffer import ariane_pkg::*; (
commit_buffer_overflow: assert property (
@(posedge clk_i) rst_ni && (commit_status_cnt_q == DEPTH_COMMIT) |-> !commit_i)
else $error("[Commit Queue] You are trying to commit a store although the buffer is full");
`endif
//pragma translate_on
endmodule