[Arc] Generates signalling code

[hovind]

comb.divs (and probably comb.divu) generate code that causes a SIGFPE signal on my system, due to division by zero.

Below is a small sample that should be equivalent to b == 0 ? 0 : a / b, which results in

$ ./build/bin/arcilator --jit-entry=main --run build/bin/div.mlir 
output = 7ffeb8e6e2a0

when run with --jit.

// RUN: arcilator %s --run --jit-entry=main | FileCheck %s
// REQUIRES: arcilator-jit
// CHECK: output = 0

hw.module @Baz(in %a: i8, in %b: i8, out c: i8) {
  %zero = hw.constant 0 : i8
  %0 = comb.divs %a, %b : i8
  %2 = comb.icmp bin eq %zero, %b : i8
  %3 = comb.mux bin %2, %zero, %0 : i8
  hw.output %3: i8
}

func.func @main() {
  %eight = arith.constant 8 : i8
  %zero = arith.constant 0 : i8

  arc.sim.instantiate @Baz as %model {
    arc.sim.set_input %model, "a" = %eight : i8, !arc.sim.instance<@Baz>
    arc.sim.set_input %model, "b" = %zero : i8, !arc.sim.instance<@Baz>
    
    arc.sim.step %model : !arc.sim.instance<@Baz>
  
    %res = arc.sim.get_port %model, "c" : i8, !arc.sim.instance<@Baz>
    arc.sim.emit "output", %res : i8
  }

  return
}

[fabianschuiki]

Fantastic find, thanks! The Comb-to-LLVM lowering should probably insert the necessary code around divisions to ensure the semantics of comb.div* are preserved. I'm not even sure if we currently specify what division by zero is.

[maerhart]

Thanks for reporting this so nicely @hovind!

AFAIK, we don't have a definition for division-by-zero semantics, which would be necessary to fix this properly.
It would be great if the CIRCT community could agree on some semantics so that all backends are consistent. Currently,

• the ExportVerilog directly lowers the operation to the / SV operation, which, I think, returns a 4-state 'x' (even if both inputs are 2-state).
• the lowering to SMT (thus circt-lec) defines it to be 1 (the SMT default for div-by-zero)
• Arcilator uses UB as in LLVM IR (which it really shouldn't do)

As an intermediate solution, we could lower a %0 = comb.divu/s %a, %b : i32 to

%zero = hw.constant 0 : i32
%is_zero = comb.icmp eq, %b, %zero : i32
%divisor = comb.mux %is_zero, %a, %b : i32
%0 = comb.divu/s %a, %divisor : i32

This means a div-by-zero results in 1, which is very arbitrary but eliminates the (propagating) UB and aligns with the SMT lowering.

Maybe that's worth a discussion in a CIRCT ODM?