Logical Equivalence Checking with Yosys EQY

[cairo-caplan]

As discussed during the review for #284 (add X-IF 1.0) for the need a Logical Equivalence Checking (LEC) to evaluate RTL changes on the CVE2, I added the choice to use the Yosys EQY on the Sequential Logical Equivalence Checking script scripts/sec/sec.sh.

To test it, one should first obtain Yosys EQY and add it to the PATH. I got mine from a prebuilt release of the Yosys HQ's OSS CAD Suite and activated its environment with source .../oss-cad-suite/environment.

Then, to run the LEC scrip, execute from the repo's root directory cd scripts/sec && ./sec.sh -t yosys . If the design is equivalent, it will print the message SEC: The DESIGN IS SEQUENTIAL EQUIVALENT.

Some notes on it:

1. It also needs the SystemVerilog Yosys frontend yosys-slang to read the RTL files, which had already claimed to officially to support the Ibex core. The standard read_verilog -sv was not enough during my tests.
2. The script deals with differences on the IO ports between the golden and the new revised (or gate as per Yosys docs) by simply deleting the extra ports introduced by the second from analysis, otherwise they cannot be comparable. This means the script assumes that changes are always incremental regarding IO functionality.
3. The script do not set the parameters of the core, so they keep their default value. This would present a problem for future changes on the X-IF add X-IF 1.0 #284 itself , for instance, as it depends on the parameter XInterface to be 1 to be enabled.

I see points 2 and 3 as debatable if we plan to make it an automated test for future RTL pull requests

[MikeOpenHWGroup]

Other than my question about the leading / in .gitignore, this LGTM @cairo-caplan. Having said that, LEC is not my field of expertise, so I think it is a good idea for @davideschiavone to review.