[NFCI] Document division and the rational for the handling of divide by zero

[darthscsi]

Be explicit that divide by zero is undefined and show examples of how different semantics for source or target languages can be achieved.

[seldridge]

LGTM

Thanks for keeping the rationales up to date. 💯

[fzi-hielscher]

Is there a reason to go straight for undefined behavior on division by zero, instead of just stating that the result is undefined (like the FIRRTL spec does)? IMHO invoking UB - and taking it seriously - puts us on a slippery slope regarding side effects and evaluation rules that we'd rather avoid in comb.

Also, modu / mods should probably be mentioned, too.

[darthscsi]

Is there a reason to go straight for undefined behavior on division by zero, instead of just stating that the result is undefined

The main motivation is so that targets which produce runtime-traps in these ops don't need code to be generated to avoid them. VHDL I believe traps on divide by zero, so to implement comb semantics, you would have to codegenerate control flow (not data flow) which avoided the trap.

[darthscsi]

Take a look again. I did like what I did for FIRRTL and took @fzi-hielscher 's suggestion to reuse that. The main thing is this precludes simulation-time traps and makes mapping to vhdl potentially more expensive.

[fzi-hielscher]

Thank you for the update. I think it makes perfect sense to define division by zero as an arbitrary combinatorial function on the numerator. I guess this also means that division on i0 would produce a well-defined zero after all, since this would be the only possible function (ping #6959 ).

The situation on the VHDL front is actually a bit more nuanced. Assuming we are using the standard numeric_std library, a division by zero should cause an assertion violation of severity 'error'. Going by the 2008 version of the standard, execution is expected to continue after such a violation, but implementations may still chose to terminate.
So basically, we have no clue what is actually going to happen and IMHO we are better off not even trying to reason about non-dataflow semantics in comb. Otherwise, we"ll paint ourselves in a corner regarding the legality of transformations that end up changing the sequence of evaluation. Perhaps the 'sim' dialect could/should handle this?

[darthscsi]

. I guess this also means that division on i0 would produce a well-defined zero after all, since this would be the only possible function

there are several: F(i0) = x, f(i0) = z, f(i0) = 0

[Moxinilian]

. I guess this also means that division on i0 would produce a well-defined zero after all, since this would be the only possible function

there are several: F(i0) = x, f(i0) = z, f(i0) = 0

I'm really not sure about giving x and z semantics to i0. The x and z abstraction works well to say that a given bit is z or x, not really on a whole value. In particular i0 has no bits, so saying its value is x or z seems a bit weird. What meaning would you give to an i0 in being x when i0 carries no information?

This approach to undefined values feels a lot like undef to me and I'm still not sure on whether that's an issue or not.

[maerhart]

This is also a bit unclear to me. The doc says: "return any value in the target's type system". If we assume that iN represents 4-valuedness, then for i1, the only valid return values would be 0, 1, x, and z. Combinatorially, for an N digit value, we have 4^N possible return values, i.e., for i0 it'd be 4^0=1. On discourse, we defined this singleton to be 0.