Logical Equivalence Check (LEC)

[sebinho]

Hi Guys,

I am currently trying to use the existing LEC module of Yosys to perform Logical Equivalence Checks.
I can't seem to get it working properly.

Is this still work in progress? I am still trying to get my hands around SiliconCompiler and would like to integrate LEC in the ASIC flow.

Thanks for your help!

[gadfort]

@sebinho I recall looking at it back in August of last year. It works in the trivial testcase we have, but I recall it needing more work to be able to handle something more complex.
Do you have an example of what you are trying to do? Maybe I can take a look at fixing it.

[gadfort]

Here is a branch I started working on a while ago: https://github.com/siliconcompiler/siliconcompiler/tree/yosys-lec

[sebinho]

Thanks, I will have a look at it

[gadfort]

Great. I'm sure there will be things that need to be fixed, this is somewhat unrefined at the moment. But the idea back in August was to add lec to the asic flow to check for correctness (optional, since that can take a lot of time to complete on larger designs).

[sebinho]

What I would like to do is what we typically do using an EDA tool like Synopsys Formality. To check logical equivalence between a design and for example a post-synthesis netlist.
This is a good check to be done in the flow especially when we insert scan-chains that could potentially alter the design if not done properly.
I have pulled your branch, did not get a chance to run it yet.
Do you maybe have a short snippet on how to use it? Is it enabled if I run for example the asicflow?

Thanks!

[gadfort]

You can see how I added it for testing to asicflow:
https://github.com/siliconcompiler/siliconcompiler/blob/8923c0ce65fe40fe261498575863dc523b0fc39b/siliconcompiler/flows/asicflow.py

This makes it run between some of the steps. You can move around where it is and see what works

[sebinho]

@gadfort, I have been playing a bit with your dedicated branch for LEC. From my side, it is actually quite useful and working quite well (I use my own proprietary PDK).
I used to actually do this with Yosys and some small scripts, but this would be great to have this integrated in the main branch at some point.
Any idea if the integration of LEC is planned anytime soon?

It works on my own simple design but it does for example fail on picorv32 example (due to the presence of memories in the design).
Maybe adding the command yosys memory in sc_lec.tcl will solve the issue.

Thanks

[gadfort]

@sebinho I'd love to get this added in, but I don't know if I have the time at the moment. In my testing it fails on several fairly simple things, which indicates me to it's not correctly setup (memory would be one thing to add).
It's good to know it works for your design.

[sebinho]

@gadfort my test design is quite simple at the moment and does not contain any memories or complex IPs. So I could understand that it might still fail in some more advanced cases.