[circt-lec] Move circt-lec files to CIRCT library

[TaoBi22]

This PR is stacked on #3991 (@frog-in-the-well), and moves most of the circt-lec code into the CIRCT library, as discussed there. No existing library directories seemed appropriate, hence the addition of the Verification directories - let me know if the files would be better placed elsewhere, or if I've added anything unnecessary.

[TaoBi22]

This has now been rebased on main since the merging of #3991 so is no longer stacked.

[mikeurbach]

Thanks for pushing on this! One nitpick: the name Verification for the library is quite general, and I expect CIRCT will ultimately have lots of different libraries related to Verification. Maybe this library could use a more specific name, like LogicalEquivalence, or something?

[TaoBi22]

Thanks for pushing on this! One nitpick: the name Verification for the library is quite general, and I expect CIRCT will ultimately have lots of different libraries related to Verification. Maybe this library could use a more specific name, like LogicalEquivalence, or something?

@mikeurbach agreed! Since I'm hoping we'll be able to continue building out verification infrastructure, I would propose that the Verification directory stays, but the library contents go into a subdirectory within it, if that sounds good to you?

[TaoBi22]

Oops, misclicked!

[mikeurbach]

I would propose that the Verification directory stays, but the library contents go into a subdirectory within it, if that sounds good to you?

That seems reasonable to me, not sure if anyone else has an opinion. A counter point is we generally don't have nesting of libraries like that in CIRCT and the lib/ namespace is kind of flat. But maybe not necessary to keep it that way.

[TaoBi22]

That seems reasonable to me, not sure if anyone else has an opinion. A counter point is we generally don't have nesting of libraries like that in CIRCT and the lib/ namespace is kind of flat. But maybe not necessary to keep it that way.

That makes sense, I guess also an option to just rename the directory for now to keep things flat and reorganise appropriately if/when more verification things get upstreamed?

[mikeurbach]

I guess also an option to just rename the directory for now to keep things flat and reorganise appropriately if/when more verification things get upstreamed?

That sounds good to me, it's very much in line with how we've done things in CIRCT so far. If there comes a time where it makes sense to group these verification libraries for some reason, we can do it at that point.

[TaoBi22]

That sounds good to me, it's very much in line with how we've done things in CIRCT so far. If there comes a time where it makes sense to group these verification libraries for some reason, we can do it at that point.

Great, this is now done!

[mikeurbach]

Looks like a clean refactor to me, so I say let's merge this if the tests are passing.

[fabianschuiki]

Mergin this now with the permission of @TaoBi22