[HWToSMT] Support hw.array_create and hw.array_get
Closed this issue · 0 comments
uenoku commented
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