llvm/circt

[HWToSMT] Support hw.array_create and hw.array_get

Closed this issue · 0 comments

Currently we cannot verify LEC between following two modules:

  hw.module @MultibitMux(in %a_0 : i1, in %a_1 : i1, in %sel : i1, out b : i1) {
    %0 = hw.array_create %a_1, %a_0 : i1
    %1 = hw.array_get %0[%sel] : !hw.array<2xi1>, i1
    hw.output %1 : i1
  }

  hw.module @MultibitMux2(in %a_0 : i1, in %a_1 : i1, in %sel : i1, out b : i1) {
    %0 = comb.mux bin %sel, %a_1, %a_0 : i1
    hw.output %0 : i1
  }
$  circt-lec bar.mlir --c1 MultibitMux --c2 MultibitMux2
bar.mlir:2:10: error: failed to legalize operation 'hw.array_create' that was explicitly marked illegal
    %0 = hw.array_create %a_1, %a_0 : i1