Skip to content

Commit

Permalink
[fpv] Assume icache req_i input is low when in reset
Browse files Browse the repository at this point in the history
This avoids spurious requests going out on the instruction bus.
  • Loading branch information
rswarbrick authored and tomeroberts committed Dec 2, 2020
1 parent afb21c2 commit 38a6b59
Showing 1 changed file with 3 additions and 0 deletions.
3 changes: 3 additions & 0 deletions formal/icache/formal_tb.sv
Original file line number Diff line number Diff line change
Expand Up @@ -12,6 +12,9 @@
`define IS_ONE_HOT(expr, width) \
!((expr) & ((expr) - {{(width)-1{1'b0}}, 1'b1}))

`define ASSUME_ZERO_IN_RESET(name) \
`ASSUME(name``_zero_in_reset, `IMPLIES(!rst_ni, ~|(name)), clk_i, 1'b0)

module formal_tb #(
// DUT parameters
parameter int unsigned BusWidth = 32,
Expand Down

0 comments on commit 38a6b59

Please sign in to comment.