PrioritySelect specialization can be improved

[grebe]

Problem Statement

Here are a few different issues that are all interrelated.

PrioritySelect codegen should be specialized when selector!=0, in which case we want codegen to specify output as X when selector==0. If we perform this specialization, we want to add an assertion that selector!=0 and this assertion should be conditioned on the input being valid (e.g. stage_valid).

There are some challenges making the desired assertion. Assertions are codegen'd in a bit of a complex way (in part because they can have user-defined codegen via format string)- it's a bit tricky to codegen without having a convenient op lying around. Furthermore, the side-effect conditioning pass already does the work to condition assertions on the input being valid, and trying to shoehorn an assertion into priority select's codegen makes that hard to leverage.

My current approach is to stuff an ``ifdef SYNTHESIS $error() endif into the undesired case arm. This `$error()` call is not predicated on having valid inputs! It's not an easily-disabled named assertion! It doesn't have a notion of verbosity! Formal methods may trivially prove it by choosing reset state! It's a bad solution, but it seems better to have a check than to silently propagate `X`, which is very abstraction breaking (we only should propagate `X` when at least some input is already `X`).

Proposal

This is a good use-case for an assume op (#542). If selector != 0 holds, we should encode this in an assume op before block->vast conversion. The side-effect conditioning pass should operate on assume just like asserts (or assume should be lowered to assert before).

Using an assume has the added advantage of making it easier to find cases where the property holds (see also #1446). Using the query engine after block conversion limits opportunities to determine properties, but with an assume we could perform the analysis during opt (before block conversion) and see through pipeline registers.

Note that the specialization for selector being one-hot is a bit different as unique casez models the one-hot property nicely, but you could imagine using an assume op to encode the property anyways.