+ # Invariant check
+ # For every instruction issued, at any point in time,
+ # each operand was either:
+ # 1) Already read
+ # 2) Not read yet, but the read is pending (rel_o high)
+ # 3) Masked
+ for i in range(dut.n_src):
+ sum_read = Signal(4)
+ m.d.comb += sum_read.eq(
+ cnt_read[i] + cnt_masked_read[i] + dut.cu.rd.rel_o[i])
+ m.d.comb += Assert(sum_read == cnt_issue)
+