Under the OSVISE project, Yosys is growing a direct connection to the CIRCT project. CIRCT, notably used in the implementation of Chisel, extends MLIR for the purposes of hardware synthesis and formal verification.
Currently, to use Yosys with designs written with Chisel, Verilog gets emitted by Chisel, and read in by Yosys. By translating between CIRCT core dialects and Yosys, this bottleneck can be removed. Advanced formal verification flows could then be implemented by evolving Yosys to represent complex properties from the LTL dialect. In the opposite direction, the connection could eventually be usable by using Yosys as a frontend to the CIRCT ecosystem.
The dialect had previously been at GitHub - YosysHQ/rtlil-mlir: Yosys RTLIL dialect for MLIR and is from now on canonically developed at GitHub - hm-aemy/chosys: CIRCT and Yosys interoperability, demonstrated with CHISEL . The goal is to upstream the dialect to the CIRCT project once a bit more of the early stage work is figured out.
The development is in an early stage. There are no stability guarantees. Until declared otherwise, expect all sorts of bugs in the translation, from unimplemented ops to subtle correctness bugs. But I invite anybody interested to take a look. Feel free to ask for more information in a new thread on this forum in the developers section with the new CIRCT tag