Skip to content

[enhancement] Invariant assertion for one-hot selector should codegen with the RTL net reference, not the IR node. #3289

@mikex-oss

Description

@mikex-oss

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

It is confusing for the generated assertion to reference the XLS IR node name in the RTL assertion. E.g. from #3288, we get:

 `ifdef ASSERT_ON
  __xls_invariant_x26_squeezed_selector_one_hot_A: assert property (@(posedge clk) disable iff ($sampled(rst !== 1'h0 || $isunknown(p2_and_2553_comb))) p2_and_2553_comb) else $fatal(0, "Selector concat.124 was expected to be one-hot, and is not.");
  `endif  // ASSERT_ON

But concat.124 is not found in the RTL, only in the .opt.ir file. This can be particularly surprising to hardware engineers whose first reaction is to debug the RTL.

Current best alternative workaround (limit 100 words)

Refer back to the opt IR file.

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

@grebe made the following comment in chat:

Yeah, this happens because we bake the string when the assert is first made. You could imagine something like how trace does format strings with a format specifier for "name of arg". My guess is it wouldn't be too much work. It might make the assert more of an optimization barrier?

Metadata

Metadata

Assignees

No one assigned

    Labels

    enhancementNew feature or request

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions