Hi Mel!
Equivalence checking against the RTLIL coming from the verific frontend sounds like a good idea. It shouldn’t pose any license issues unless you’re making a profit off the work, and it’s definitely more practical than manually creating them. Also do let us know if you identify any discrepancies or bugs in the verific frontend checker circuits!
From the technical side, just off the top of my head, it would probably still require a little bit of manual netlist manipulation: for each $assert/$assume/$cover/$live you’d have to and together the A and EN ports to get the “property active” condition (since these ports are used differently between frontends) - I don’t know if there’s any way to create $and cells with the current script commands… but after that you could use expose to add them as module ports and miter -equiv -assert to compare all the exposed conditions. (Maybe also run delete -output before expose to avoid the solver effort of comparing the normal module outputs, if your test circuits have any.)
BTW what are your plans regarding the property IR? We have had the vague plan of first completing that project before tackling SVA in yosys-slang. Since porting over the verific flow to that IR will already involve creating a frontend-independent yosys pass constructing checker circuits from $property cells, we expect it’ll be much less work to add property support to other frontends after that, because only the frontend → IR import portion is needed, and the IR concepts are much closer to SVA. In fact the motivation in that project is to be able to use CIRCT as a second frontend to import properties from, and be able to reuse the same checker generation pass in both the verific and CIRCT flows. You can of course get a head start on yosys-slang now, but I worry that some of the work might turn out redundant in the end…