[rom_ctrl, dv] Exclusions for tlul_adapter_sram and prim_fifo_sync

[KinzaQamar]

No description provided.

[rswarbrick]

I've just had a look at this item and I think it's impossible for any instance of the adapter, because the two wready signals can never be different from one another. Because of this, I've actually just opened #25905.

I think I agree that sramreqfifo_wready will never be false at all (for the reason you give). As such, we'll probably need a tweaked version of this because there will be a conditional coverage hole for "110".

But I think we can also shorten the description a bit. Maybe something like this?

// The case 1101 is cannot happen for the conditional statement below.
//
// This is because sramreqfifo_wready can never be false. The u_sramreqfifo FIFO has depth 2 and
// will contain have more than one item. The ROM always responds in exactly one cycle, so
// sramreqfifo_rready will always be true if the FIFO is nonempty and a second item can never be
// added without removing the current one.

[rswarbrick]

I had to think a bit to convince myself of why this was true and I think it can be reworded a bit to make it clearer?

    // This item is impossible because it is rready_i -> rready_o for a u_reqfifo instance in any
    // tlul_adapter_sram. This is because rready_i is driven by reqfifo_rready, which is d_ack. This
    // is only true when tl_o_int.d_valid is true, which means the ROM is responding to a request.
    // That request will have been pushed into u_reqfifo as it was sent out, so the FIFO is not
    // empty and rready_o must be true.

Does the reasoning sound right to you?

[rswarbrick]

As a general comment, I'd probably suggest harvesting these items from the PR in groups of one or two and making PRs for the groups. That way, they needn't all be dependent one one another.

We can always do the "commit merging" as part of landing the individual PRs. This is a pretty trivial file format, so it's not difficult :-)

[rswarbrick]

I think this is correct, but the logic took me a bit of time to follow. Reasoning through it myself, I ended up with this, which I think might be slightly easier to follow?

// The following item cannot happen. It requires that rvalid_o = 0 and rready_i = 1 in u_rspfifo.
//
// If rready_i is true in u_rspfifo, that means that rspfifo_rready is true in the SRAM adapter.
// This means that reqfifo_rdata.op = OpRead, that reqfifo_rdata.error is false, and that
// reqfifo_rready is true. The latter signal is d_ack, which can only be true if tl_o_int.d_valid is
// true, which implies that the d_valid signal is true. Since we know that the operation is OpRead
// and it doesn't have an error, the combinatorial logic that calculates d_valid yields
// rspfifo_rvalid. That signal is the rvalid_o output port from u_rspfifo. As a result, if rready_i
// is true in u_rspfifo then rvalid_o must also be true.

[rswarbrick]

I think there's a rather shorter chain of logic that gets here:

// We can never see rvalid_o && under_rst in u_reqfifo in any tlul_adapter_sram instance. Since the
// Pass parameter is false for u_reqfifo, rvalid_o is only true if the FIFO is nonempty. Since the
// FIFO clears on reset, this cannot be true in the first cycle after reset. But that is the only
// cycle when under_rst is true.

[rswarbrick]

I think we can refer to the previous condition to make this argument quite a bit shorter:

// By the same argument as that given for the previous condition, the u_rspfifo storage cannot be
// nonempty when the under_rst flag is true. But u_rspfifo was has a Pass parameter of 1, which
// would give another way for rvalid_o to be true. For that to apply, we would need wvalid_i to be
// true, which is rspfifo_wvalid in tlul_adapter_sram. This depends on reqfifo_rvalid, which can
// only be true when u_reqfifo is nonempty. The reasoning for the previous condition shows that this
// cannot happen.

[rswarbrick]

I think you can be lazier here, with something like this:

// Since u_sramreqfifo has Pass=0, this condition cannot happen for the same reason as the analogous
// condition for u_reqfifo, argued above.

[rswarbrick]

I thought a little bit about this and I think there's probably a shorter chain of reasoning: we don't actually need to say anything about what the ready and valid signals mean in this case. Something like this, maybe?

// The wvalid_i signal in u_reqfifo comes from reqfifo_valid in tlul_adapter_sram, which equals
// a_ack. For that to be true, tl_a_int.a_ready must be true. That signal is only true if
// reqfifo_wready is true, but that signal is wready_o.

[rswarbrick]

This took me a few seconds to properly understand, and I think that it could be explained more clearly (for me, at least!). Something like this, maybe?

// The u_rspfifo instance in tlul_adapter_sram can never give any backpressure through the wready_o
// signal. This is because u_reqfifo will always be at least as full as u_rspfifo, each item in
// u_rspfifo is a response to a request that is still stored in u_reqfifo. The request is stored in
// order to be able to supply d_size and d_source in the TL response.
//
// If w_valid_i is true in u_rspfifo, this is the response to some request which must be stored in
// u_reqfifo, which implies there is a slot to store it.

[rswarbrick]

I think you mean wready_o=0 here? I'd also say "... we only get wready_o=0 ..." to make it clear how the implication is supposed to go.