Wanted to check, if "formal verification" is done while RTLtoGDS flow of openLane. In case, yes, please share details of tool it uses for formal verification.

As far as i know formal verification is not included, but I would suggest to take a look at https://www.symbioticeda.com/formal-verification

@Brajesh @Philipp Gühring I think SBY could be another option: https://github.com/YosysHQ/sby Please check this out for more info about Openlane’s arch: https://openlane.readthedocs.io/en/latest/flow_overview.html

@manili @mkk My shared pic, which is taken from https://github.com/efabless/OpenLane/ , shows that formal verification is done using "yosys + abc" combo. My confusion is whether formal verification is integrated in "rtl-to-gds" flow or not. What I mean here is, does user has to separately integrate SymbiYosys or it comes with "rtl-to-gds" flow bundle by default.

@Vijayan Krishnan any ideas?

I don't have idea on this. You may request for enhancement in https://github.com/The-OpenROAD-Project/OpenLane/issues. OpenLane team give you exact status.

Thank you @Vijayan Krishnan. Did the needful, as suggested. But I was expecting this clarification in the ongoing thread from all concerned, as it is TRL-to-GDS automated flow feature related issue as already mentioned over the page (pl refer to figure of the starting thread).