[enhancement] Enable equivalence checking in DSLX files

[rw1nkler]

What's hard to do? (limit 100 words)

There is no simple way in DSLX to check if two different function implementations are equivalent. The check_ir_equivalence tool can verify this at the IR level, but it must be called manually. This makes it hard to confirm that an optimized or alternative version of a function behaves exactly the same as the original, especially when testing refactors or hardware optimizations.

Current best alternative workaround (limit 100 words)

Currently, both functions must be compiled to IR separately, and the check_ir_equivalence tool has to be run manually on the generated files. This process requires several steps, and doesn’t integrate with the regular DSLX test framework. It also becomes cumbersome when checking many function pairs.

DSLX also provides the #[quickcheck] attribute, which can verify functions over a large range of input values to check if the implementations behave the same way. However, this approach can become impractical when operands are large or when the function’s input space is too big to explore exhaustively. In such cases, a formal equivalence check would provide much stronger guarantees with possibly less computation.

Your view of the "best case XLS enhancement" (limit 100 words)

It would be useful to expose the check_ir_equivalence functionality directly to the DSLX frontend. A new test attribute could allow marking a function to be automatically compared against another implementation for behavioral equivalence.

For example:

#[check_equivalence=reference_function]
fn optimized_function(a: u32, b: u32) -> u32 { ... }

This would tell the DSLX frontend to automatically compare the IR of optimized_function to reference_function using the internal equivalence checking tool, and fail the test if they are not functionally identical.

A common use case would be when implementing mathematical functions that can be pipelined for better hardware performance. For example, a simple integer multiplication can be rewritten as a sum of partial products so the work is split into smaller operations on shorter bit-widths. This can improve timing and throughput, at a cost of increased resource utilization. The check would make sure both versions still give the same result for every input.