Commits on May 12, 2024

1. [CombToSMT] Make result of div-by-zero undefined …

   This adapts the conversion pass to match the recently agreed upon definition for division by zero. Integration tests for circt-lec are added to check the behavior. Note that two syntactically equivalent modules are not considered equivalent if they aren't guaranteed to deterministically produce the same outputs. Alternatively, we could consider two undefined output values equivalent by modeling each value as a pair of a boolean and the bit-vector where the boolean determines if the value is undefined, then two outputs are equivalent if either the boolean is true or the boolean is false and the bitvectors match. There are probably use-cases for both, so maybe we'd want a flag to let the user decide.

   

   maerhart committed May 12, 2024
   Configuration menu

   • View commit details
   • Copy full SHA for 51bfb5c
   • Browse repository at this point

   Copy the full SHA

   51bfb5c View commit details

   Browse the repository at this point in the history