This is the result of a bunch of issues I ran into and then discussed with @PeterRugg.
When comparing two implementations, they do not necessarily need to agree on all RVFI fields. For example, an out-of-order core might likely not report values for the source registers because they are not present at the reporting stage. While it is possible to forward the values to the reporting stage, this is an artificial overhead that is quite unnatural in the core development.
An equal issue arises with misaligned memory accesses. Some implementations only support misaligned accesses, whereas others do not.
In order to avoid useless and confusing failures, we propose creating profiles for implementations. Depending on the profiles, QuickCheck and the implementations are instantiated such that useful testing mechanism for a tuple of implementations is conducted.
This is the result of a bunch of issues I ran into and then discussed with @PeterRugg.
When comparing two implementations, they do not necessarily need to agree on all RVFI fields. For example, an out-of-order core might likely not report values for the source registers because they are not present at the reporting stage. While it is possible to forward the values to the reporting stage, this is an artificial overhead that is quite unnatural in the core development.
An equal issue arises with misaligned memory accesses. Some implementations only support misaligned accesses, whereas others do not.
In order to avoid useless and confusing failures, we propose creating profiles for implementations. Depending on the profiles, QuickCheck and the implementations are instantiated such that useful testing mechanism for a tuple of implementations is conducted.