mirror of https://github.com/llvm/circt.git
539bba931f
Add the `LowerSymbolicValues` pass which converts `verif.symbolic_value` ops either to a black box instance or to a wire declaration with a `(* anyseq *)` attribute. The former is useful since most formal tools have a way of treating black boxes as internal port boundaries, such that black box output ports behave the same as top-level input ports. The latter is useful for interoperability with Yosys which has a custom Verilog attribute "anyseq" that marks a wire declaration as a symbolic value. |
||
|---|---|---|
| .. | ||
| 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 | ||