Eqy check

[openroadie]

This PR will fail since CI/CD does not have yosys/eqy etc but it is to provide a general idea of how we can add equivalency checks to our unit tests. The scripts etc need to be made more flexible to handle different top modules and some more cells would probably need to be added to cells.v but we at least have a couple of regressions where it is already working (provided the machine has yosys and eqy installed correctly ... and available on the path).

cc: @tspyrou @maliberty @QuantamHD

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[QuantamHD]

@gadfort Can you help review this as well

[QuantamHD]

Do you actually have the implementation of run_equivalence_test done, or is this just a sketch?

[gadfort]

I think we'd need to see the eqy scripts to be able to review properly. Why are the FFs empty in the cells.v? What happens if they are resized? Would eqy be able to verify that?

[maliberty]

Perhaps you need to 'git add' some new files?

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[openroadie]

Perhaps you need to 'git add' some new files?

@maliberty you are right :). I needed to "git push" some files.

@gadfort I will look into adding the the body of the FFs and other info.

@QuantamHD I will push the equivalence script. I need to add some code around it so we can run on different top cells (right now hardcoded to one cell name) etc.. Please note that to run this script you need to do the following:

https://github.com/YosysHQ/yosys sudo make install https://github.com/YosysHQ/eqy sudo make install

I tried running equivalence on some of the smaller designs we have in ORFS and at least from my experience, these tools are not ready for anything other than toy designs. On jpeg, using the same netlist twice to do equivalence checking, the run took 2 to 15 hours (depending on the recipe you use for equivalence) and created roughly 10 million files. At the end, during the report generation step, the tool error-ed out because there were too many files. Here is a summary of the various strategies used. Please note that other tools may need to be installed to get some of these to work

#=======================================================
[strategy A]   # 15 hours
use sat
depth 10
#=======================================================
[strategy B] # 10+ hours
use sby
engine abc pdr
depth 10
#======================================================
[strategy C] # 15 hours.
use sby
depth 2
engine smtbmc bitwuzla
#======================================================
[strategy basic] # 3 hours.
use sat
depth 10
#======================================================

All these runs failed with too many files to consolidate for reporting. Other tools that may need to be installed (again just the standard yosys way since they don't support any other paths easily):

https://github.com/YosysHQ/sby https://bitwuzla.github.io/download.html # Place binary in /use/local/bin

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[QuantamHD]

@openroadie I think that there's probably some optimization required to use these tools optimally on larger designs, but I think we should actually take a different tact that just running our CI designs through resizer, and seeing if they're equivalent.

I think it would be more effective to generate random netlists with ABC or another tool of some reasonable size, and running 100-1000s through the resizer, and check their equivalence in parallel. Essentially fuzzing the resizer.

We should still develop a strategy for larger blocks, but I think the strategy above is more likely to be successful in the short term.

Also I would request that we use a real cell library. https://github.com/google/skywater-pdk-libs-sky130_fd_sc_hd/blob/ac7fb61f06e6470b94e8afdf7c25268f62fbd7b1/cells/a21bo/sky130_fd_sc_hd__a21bo.functional.v

Or similar from another library. I worry that reducing the cell choices too much could hide bugs in more filled out libraries. Totally fine to test with this simplified model though

[openroadie]

@QuantamHD are you saying that running equivalence check on unit tests as a first cut is not worth doing?

As I already explained, I had no luck so far running the eqy check on the jpeg design with 54000 cells (post synthesis).

Do we have any data that would indicate that the yosys equivalence checks have been sucessfully used for 10k+ sized netlists?

Our unit tests do have a couple of hundred instances and since they were designed to test various transforms .... I am not entirely sure that starting with them is all that bad.

[QuantamHD]

I think a first pass of the unit tests are totally fine, but running it on significantly larger designs like JPEG should be more rare.

My hypothesis is that we can find more bugs with stochastically generated netlists of a more reasonable size.

[openroadie]

@QuantamHD Agreed on real library (easier in some ways since I do not have to write cell verilog). Let me see if we have any sky

Larger designs == more bugs is also correct and inevitable as we add more complex transforms. It should be noted that the one bug we found would have been caught by a few dozen of our unit tests if we were doing equivalence checking. So adding the checks there makes everybody's life easier instead of debugging some large design.

We need to figure out a strategy for larger blocks but we do not have enough data at this point to set the size bar under which the open source equivalence checking tools work reasonably well. The limits right now are 300-500 (works fine) and 55000 (more or less unusable in it's current state).

One last thing to figure out is whether we want OR dev environment dependent on one or more yosys repos @tspyrou @maliberty or should we have an option to run equivalence checks (then we either need to have two sets of ok files or put in a fake "equivalence checks passed" for the case where we are not running them). If we go with this approach we may have issues slip in from the developer end and only be caught in CI/CD (which might be ok). In short.... a lot of logistical details are not clear at this point (none of them is a blocker for now).

[gadfort]

@openroadie @QuantamHD it's not clear to me that you would want to run this on every test (if it's fast then it might be okay to add to the tools that might modify the designs). If there was a way to trigger the gate cloning and undo logic, then a specific set of tests could be used there to ensure it doesn't modify the logic. I suspect the issue with undo in the rsz are more pronounced on larger designs, so those are where it would be the most interesting.

Maybe running some of these as part of the secure- or nightly CI's might make sense to ensure some coverage on larger tests without being a burden on initial CI's.

[openroadie]

@QuantamHD : I took a look at the sky130hd functional verilog for cells. We do have some unit tests which use this library. A few caveats/issues that need resolution:

• the eqy/yosys verilog reader is not the most bulletproof piece of code. I had to to significant hand editing of the verilog definitions for ASAP7 to get it into a working condition. The same may be needed for sky130hd.
• Once we copy/hand modify these files as needed, we run the risk of the functional verilog we are using for equivalence being out of sync with the source controlled version. For now I think this is acceptable.

@gadfort This test is fast enough that it is worthwhile to do it on all unit tests at least for sky130hd and Nangate45 (which is what most unit tests seem to be using). Gate cloning had the bug that you found but I don't think I can make the claim that all the other transforms (or any combination thereof) have no issues especially since we end up using "undo" pretty heavily.

I also found a small enough test (aes) which only takes about 30-40m to run equivalence checking on (but I still have the problem with the final reporting code which is going something like "ls *" in a directory and errors out with "list of arguments too large"). I will take a look at the code to see if we can fix this.

[openroadie]

@QuantamHD do you have any pointers on how to scholastically generate a netlist that has clocks (so the resizer is actually called). I will start taking a look at that as well while we work on getting nangate45 and sky130hd based unit tests working.

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[QuantamHD]

@openroadie This abc command generates combinatorial netlists. https://github.com/berkeley-abc/abc/blob/master/src/base/abci/abc.c#L13541

I think it would be easy enough to put random registers in these netlists to get the sequential bits as a starting point.

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[jix]

• The same may be needed for sky130hd.

Note that the EQY repository already has a sky130 example that comes with a script to pre-process the simulation models to make them suitable for formal verification (including equality checking): https://github.com/YosysHQ/eqy/blob/main/examples/spm/formal_pdk_proc.py

If you run into any sky130 gate level netlists that do not work with it, feel free to file an issue on the EQY repository, even if it's not strictly part of EQY but rather used as an example.

[QuantamHD]

@openroadie I ran a pretty large test with just the ABC cec commands, and I found that they're very fast. 33k nodes proved equivalent in 0.39 seconds. I think we just need to figure out how to best leverage the commands from OpenROAD either through eqy or a custom solution.

abc 02> &ps
Multi64  : i/o =    128/    128  and =   33078  lev =  383 (226.45)  mem = 0.38 MB
abc 02> &cec booth.aig
Networks are equivalent.  Time =     0.39 sec

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[openroadie]

@vvbandeira We need the same thing for the container that runs the CI/CD code in OR and ORFS

https://github.com/The-OpenROAD-Project/OpenROAD-flow-scripts/pull/1447#issuecomment-1710704690

To repeat the info here:

The CI/CD container needs these repos installed as the default (sudo make install). Please follow the order the repos are mentioned in:

https://github.com/YosysHQ/yosys https://github.com/YosysHQ/eqy https://github.com/YosysHQ/sby

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[openroadie]

@maliberty @tspyrou @QuantamHD : This PR with 12 unit tests enabled for eqy is now ready for merge.

@QuantamHD We are using sky130hd for two of the tests.

Thanks to @jix for all the help with using eqy and supplying us a equivalency checking verilog for sky130hd and to @vitor for enhancing the docker container to get all this to work :+1:

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"

[github-actions[bot]]

clang-tidy review says "All clean, LGTM! :+1:"