Equivalence Check through Hierarchy

[se-bi]

Hey there!

We are currently working on getting the equivalence checker running, but run into some issues.
We are not sure if we are misunderstanding the functions that we are using in our yosys scripts or if the required capabilities are not yet given in the toolsuit.
We are looking for a framework that is able to equivalence check two designs that might have the same topmodule and/or submodule names and had also a look at #639.

In the link below you can find some test cases and a description of those in this README.
As it seems, the tool is not checking the logical functionality of submodules at all,
but is more interested in the naming of the submodule / instance of the submodule.
We are not sure whether that is due to a misuse of the commands in the yoysys scripts or if there are any other problems.

We would be happy if you could help us with our issue and are eager to help if you have any questions concerning our test or use cases!

Cheers,
Lennart & Sebastian

Steps to reproduce the issue

Check in se-bi/yosys-examples/formal:

• example-from-issue639-run-all-yosys-equiv.sh
• example-from-issue639-check-results.sh
• example-from-issue639-show-diffs.sh

(TBD see the github-workflow)

Expected behavior / Actual behavior

dir/version	equiv result	equiv expected	Name top	Name sub	Impl Top	Impl sub
orig #639	false	false	same	same	diff	same
v1	true	false	same	same	same	diff
v2	false	false	same	same	diff	same
v3	false	false	same	same	diff	same
v4	true	false	same	same	same	diff
v5	false	false	same	diff	same	diff
v6	false	true	same	diff	same	same
v7	true	true	diff	same	same	same
v8	true	false	diff	same	same	diff
v9	false	false	diff	diff	same	diff
v10	false	true	diff	diff	same	same
v11	false	true	same	instance name only	same	same