Google/xls | Random GitHub Issue

Google/xls

New issue in about 14 hours

XLS: Accelerated HW Synthesis

1,957C++

opt fails to propagate non-absorbing `or`/`and` sibling conditions into operand fanin#5151

Opened by mikex-oss

Describe the bug When an operand of a boolean || or && (or a reconvergent if / else if condition) is only observable when a sibling operand has its non-absorbing value (0 for or, 1 for and), the IR optimizer does not use that fact to simplify the operand's fanin, and redundant references to the sibling inside the operand are kept.

Small cases are caught incidentally by BooleanSimplificationPass when the whole expression has at most 3 inputs and simplifies to a single and/or/nand/nor/xor (e.g. c0 || (a && !c0) → or(c0, a)), but not otherwise.

To Reproduce In c0 || (a && !c0 && b), the right-hand side of || only affects the result when c0 == 0, so !c0 is redundant and the expression is equivalent to c0 || (a && b). Unlike the 2-variable case, c0 | (a & b) is not a single n-ary op, so BooleanSimplificationPass doesn't simplify it, and nothing else removes c0 from the inner term.

pub fn repro_or(c0: bool, a: bool, b: bool) -> bool {
    c0 || (a && !c0 && b)
}

top fn __repro__repro_or(c0: bits[1] id=1, a: bits[1] id=2, b: bits[1] id=3) -> bits[1] {
  not.9: bits[1] = not(a, id=9)
  not.10: bits[1] = not(b, id=10)
  nor.11: bits[1] = nor(not.9, c0, not.10, id=11)
  ret or.7: bits[1] = or(c0, nor.11, id=7)
}

pub fn repro_cond(
    sgn0: bool, n0: bool, i0: bool,
    sgn1: bool, n1: bool, i1: bool,
    x: u8,
) -> u8 {
    let f0_inf = i0 && !n0;
    let f1_inf = i1 && !n1;
    let pos_inf = (f0_inf && !sgn0) || (f1_inf && !sgn1);
    let neg_inf = (f0_inf && sgn0) || (f1_inf && sgn1);
    let is_nan = n0 || n1 || (pos_inf && neg_inf);
    let is_inf = pos_inf || neg_inf;
    if is_nan {
        u8:0xff
    } else if is_inf {
        (neg_inf as u8) | u8:0xfe
    } else {
        x
    }
}

top fn __repro__repro_cond(sgn0: bits[1] id=1, n0: bits[1] id=2, i0: bits[1] id=3, sgn1: bits[1] id=4, n1: bits[1] id=5, i1: bits[1] id=6, x: bits[8] id=7) -> bits[8] {
  not.52: bits[1] = not(i0, id=52)
  not.56: bits[1] = not(i1, id=56)
  not.59: bits[1] = not(sgn0, id=59)
  not.62: bits[1] = not(sgn1, id=62)
  nor.53: bits[1] = nor(not.52, n0, sgn0, id=53)
  nor.57: bits[1] = nor(not.56, n1, sgn1, id=57)
  nor.60: bits[1] = nor(not.52, n0, not.59, id=60)
  nor.63: bits[1] = nor(not.56, n1, not.62, id=63)
  pos_inf: bits[1] = or(nor.53, nor.57, id=16)
  neg_inf: bits[1] = or(nor.60, nor.63, id=19)
  literal.48: bits[7] = literal(value=127, id=48)
  and.21: bits[1] = and(pos_inf, neg_inf, id=21)
  is_inf: bits[1] = or(pos_inf, neg_inf, id=23)
  concat.41: bits[8] = concat(literal.48, neg_inf, id=41)
  is_nan: bits[1] = or(n0, n1, and.21, id=37)
  sel.28: bits[8] = sel(is_inf, cases=[x, concat.41], id=28)
  literal.24: bits[8] = literal(value=255, id=24)
  ret sel.29: bits[8] = sel(is_nan, cases=[sel.28, literal.24], id=29)
}