mirror of https://github.com/llvm/circt.git
71dec45d65
This PR adds the RefinementCheckingOp to the verif dialect. The motivation behind this operation is to be able to automatically check whether a 'target' circuit is a refinement of a 'source' circuit. This should be a small step towards performing translation validation comparable to Alive2. The operation is structurally identical to the LogicEquivalenceCheckingOp, so I factored out most of the ODS into a common CircuitRelationCheckOp. If there is no non-determinism present in the circuits, the operation is also functionally identical to LogicEquivalenceCheckingOp. Co-authored-by: Bea Healy <57840981+TaoBi22@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| basic.mlir | ||
| canonicalization.mlir | ||
| cse.mlir | ||
| errors.mlir | ||
| lower-contracts.mlir | ||
| lower-formal-to-hw.mlir | ||
| lower-symbolic-values-errors.mlir | ||
| lower-symbolic-values.mlir | ||
| prepare-for-formal.mlir | ||
| strip-contracts.mlir | ||
| verify.mlir | ||