Minimum sel property doesn't really do what it's intended to do

[tudortimi]

The property checks that sel doesn't go down one cycle after it goes up:

property amiq_apb_sel_minimum_time_p;
  @(posedge clk) disable iff(!reset_n || !en_protocol_checks)
    $rose(|sel) |-> not(##1 $fell(|sel));
endproperty

Since what it's checking is the or reduce of sel, what is still allowed by the property is that sel changes to a different slave, but doesn't go down completely. Moreover, the not operator seems to cause problems with strong/weak semantics in certain simulators. The use of overlapping implication followed by a delay also spawns extra threads, which might cause some performance overhead. You could rewrite the assertion as:

$rose(|sel) |=> $stable(sel));

[amiq-consulting]

In general, digital simulations use the 4-value logic. VHDL's 9 levels of strength are used mostly for analogue modeling or low level component modelling. So I think using not, is quite safe. It is indeed better to use $stable instead of current implementation.