mirror of https://github.com/llvm/circt.git
b79242dc8d
verif.assume can be used to annotate pre-condtion directly in the IR. This is quite useful when verifying transformation which involves undefined values. For example when lowering comb.shl to AIG, the conversion pass chooses arbitary values for out-of-bounds situation. So we cannot verify the equivalence unless we specify the pre-condtion with verif.assume |
||
|---|---|---|
| .. | ||
| comb.mlir | ||
| commandline.mlir | ||
| hw.mlir | ||