Skip to content

Commit

Permalink
[rtl] Trigger C decoder assertions only if instr valid
Browse files Browse the repository at this point in the history
This commit ensures that the assertions in the compressed decoder do
not fire if the compressed decoder sees invalid data from the prefetch
buffer.

Signed-off-by: Pirmin Vogel <[email protected]>
  • Loading branch information
vogelpi committed Jan 3, 2020
1 parent 17d69d1 commit 7e22830
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 8 deletions.
25 changes: 17 additions & 8 deletions rtl/ibex_compressed_decoder.sv
Original file line number Diff line number Diff line change
Expand Up @@ -13,13 +13,19 @@
module ibex_compressed_decoder (
input logic clk_i,
input logic rst_ni,
input logic valid_i,
input logic [31:0] instr_i,
output logic [31:0] instr_o,
output logic is_compressed_o,
output logic illegal_instr_o
);
import ibex_pkg::*;

// valid_i indicates if instr_i is valid and is used for assertions only.
// The following signal is used to avoid possible lint errors.
logic unused_valid;
assign unused_valid = valid_i;

////////////////////////
// Compressed decoder //
////////////////////////
Expand Down Expand Up @@ -274,15 +280,18 @@ module ibex_compressed_decoder (
////////////////

// Selectors must be known/valid.
`ASSERT_KNOWN(IbexInstrLSBsKnown, instr_i[1:0], clk_i, !rst_ni)
`ASSERT(IbexC0Known1, (instr_i[1:0] == 2'b00) |-> !$isunknown(instr_i[15:13]), clk_i, !rst_ni)
`ASSERT(IbexC1Known1, (instr_i[1:0] == 2'b01) |-> !$isunknown(instr_i[15:13]), clk_i, !rst_ni)
`ASSERT(IbexC1Known2,
((instr_i[1:0] == 2'b01) && (instr_i[15:13] == 3'b100)) |->
`ASSERT(IbexInstrLSBsKnown, valid_i |->
!$isunknown(instr_i[1:0]), clk_i, !rst_ni)
`ASSERT(IbexC0Known1, (valid_i && (instr_i[1:0] == 2'b00)) |->
!$isunknown(instr_i[15:13]), clk_i, !rst_ni)
`ASSERT(IbexC1Known1, (valid_i && (instr_i[1:0] == 2'b01)) |->
!$isunknown(instr_i[15:13]), clk_i, !rst_ni)
`ASSERT(IbexC1Known2, (valid_i && (instr_i[1:0] == 2'b01) && (instr_i[15:13] == 3'b100)) |->
!$isunknown(instr_i[11:10]), clk_i, !rst_ni)
`ASSERT(IbexC1Known3,
((instr_i[1:0] == 2'b01) && (instr_i[15:13] == 3'b100) && (instr_i[11:10] == 2'b11)) |->
`ASSERT(IbexC1Known3, (valid_i &&
(instr_i[1:0] == 2'b01) && (instr_i[15:13] == 3'b100) && (instr_i[11:10] == 2'b11)) |->
!$isunknown({instr_i[12], instr_i[6:5]}), clk_i, !rst_ni)
`ASSERT(IbexC2Known1, (instr_i[1:0] == 2'b10) |-> !$isunknown(instr_i[15:13]), clk_i, !rst_ni)
`ASSERT(IbexC2Known1, (valid_i && (instr_i[1:0] == 2'b10)) |->
!$isunknown(instr_i[15:13]), clk_i, !rst_ni)

endmodule
1 change: 1 addition & 0 deletions rtl/ibex_if_stage.sv
Original file line number Diff line number Diff line change
Expand Up @@ -219,6 +219,7 @@ module ibex_if_stage #(
ibex_compressed_decoder compressed_decoder_i (
.clk_i ( clk_i ),
.rst_ni ( rst_ni ),
.valid_i ( fetch_valid ),
.instr_i ( fetch_rdata ),
.instr_o ( instr_decompressed ),
.is_compressed_o ( instr_is_compressed_int ),
Expand Down

0 comments on commit 7e22830

Please sign in to comment.