yosyshq / eqy Goto Github PK

View Code? Open in Web Editor NEW

30.0 30.0 5.0 1.04 MB

Equivalence checking with Yosys

Home Page: https://yosyshq.readthedocs.io/projects/eqy/en/latest/

License: Other

Python 47.04% Makefile 4.13% C++ 47.53% Shell 1.17% SystemVerilog 0.14%

eqy's People

Contributors

Stargazers

Watchers

Forkers

mmicko rbarzic openroadie donn doughnutsz

eqy's Issues

Rename nostop, nosplit, and noautogroup

I'd like to come up with new names for those statements, that do not contain a negation. (And in case of noautogroup, also something that's shorter. ;)

For example

nosplit -> join
nostop -> bind
noautogroup -> solo

I really like "join" as a replacement for "nosplit".

I think "bind" is okay but has potential for confusion with the SystemVerilog bind statement.

I think "solo" is really bad. 🤣 Any better ideas anyone?

Import initial values from the gold and gate design into partitions

Fix auto-grouping to not create two partitions for the same primary output net

Make install not working

Hello, I followed the instructions to install Yosys EQY on my Ubuntu 20.04 device as such:

$ git clone https://github.com/YosysHQ/eqy.git epy
$ cd eqy
$ sudo make install

Initially, it said that yosys-config had no such command, so I did some research and found that I had to install yosys-dev which I did as such:

$ sudo apt-get install yosys-dev

Then, when I run sudo make install I now get the following errors:

src/eqy_combine.cc: In member function ‘void {anonymous}::EqyCombinePass::print_ids(FILE*, Yosys::RTLIL::Module*)’:
src/eqy_combine.cc:82:25: error: ‘struct Yosys::RTLIL::Module’ has no member named ‘get_hdlname_attribute’; did you mean ‘get_bool_attribute’?
   82 |   for (string name : m->get_hdlname_attribute())
      |                         ^~~~~~~~~~~~~~~~~~~~~
      |                         get_bool_attribute
src/eqy_combine.cc:86:19: error: ‘ID’ has not been declared
   86 |    if (a.first == ID::hdlname)
      |                   ^~
src/eqy_combine.cc:96:16: error: ‘struct Yosys::RTLIL::IdString’ has no member named ‘isPublic’
   96 |    if (c->name.isPublic())
      |                ^~~~~~~~
src/eqy_combine.cc:99:27: error: ‘struct Yosys::RTLIL::Cell’ has no member named ‘get_hdlname_attribute’; did you mean ‘get_bool_attribute’?
   99 |     for (string name : c->get_hdlname_attribute())
      |                           ^~~~~~~~~~~~~~~~~~~~~
      |                           get_bool_attribute
src/eqy_combine.cc:103:21: error: ‘ID’ has not been declared
  103 |      if (a.first == ID::hdlname)
      |                     ^~
src/eqy_combine.cc:114:16: error: ‘struct Yosys::RTLIL::IdString’ has no member named ‘isPublic’
  114 |    if (w->name.isPublic())
      |                ^~~~~~~~
src/eqy_combine.cc:117:27: error: ‘struct Yosys::RTLIL::Wire’ has no member named ‘get_hdlname_attribute’; did you mean ‘get_bool_attribute’?
  117 |     for (string name : w->get_hdlname_attribute())
      |                           ^~~~~~~~~~~~~~~~~~~~~
      |                           get_bool_attribute
src/eqy_combine.cc:121:21: error: ‘ID’ has not been declared
  121 |      if (a.first == ID::hdlname)
      |                     ^~
make: *** [Makefile:26: src/eqy_combine.so] Error 1

Am I missing something or has something become outdated?

Report: Partition Overview

partition name
number of input/output/cross nets and bits
number of gold and gate cells
unused gate/gold input bits
results from strategies
pointers to CEX vcd files

Invalid JSON generated during partition stage

Using Yosys 0.33+6 (git sha1 05f0262d775, clang++ 11.1.0 -fPIC -Os)

During the partition stage, this following JSON file is generated:

test_sram_macro/partition/test_sram_macro.flattensubmodule.logic_not.test_sram_macro.v374_Y.json:

{
    "index": 45,
    "name": "test_sram_macro.flattensubmodule.logic_not.test_sram_macro.v374_Y",
    "inbits": {
      "cs": [0]
    },
    "outbits": {
      "$flatten\submodule.$logic_not$./test_sram_macro.v:37$4_Y": [0]
    },
    "crossbits": {
    }
}

Which is read by eqy and thus reports an error:

File "/nix/store/dqvlshhrc4q7519gfinxprl3rn2y1rwz-eqy/bin/eqy", line 1208, in <module>
    main()
  File "/nix/store/dqvlshhrc4q7519gfinxprl3rn2y1rwz-eqy/bin/eqy", line 1181, in main
    make_scripts(ctx.args, ctx, ctx.job, strategies)
  File "/nix/store/dqvlshhrc4q7519gfinxprl3rn2y1rwz-eqy/bin/eqy", line 1016, in make_scripts
    cfg.partitions.append(EqyPartition(line, args, cfg, job))
  File "/nix/store/dqvlshhrc4q7519gfinxprl3rn2y1rwz-eqy/bin/eqy", line 999, in __init__
    for key, value in json.load(f).items():
  File "/nix/store/65cp4izx3bllnwqn7c7dhrq9h9gmjkal-python3-3.10.9/lib/python3.10/json/__init__.py", line 293, in load
    return loads(fp.read(),
  File "/nix/store/65cp4izx3bllnwqn7c7dhrq9h9gmjkal-python3-3.10.9/lib/python3.10/json/__init__.py", line 346, in loads
    return _default_decoder.decode(s)
  File "/nix/store/65cp4izx3bllnwqn7c7dhrq9h9gmjkal-python3-3.10.9/lib/python3.10/json/decoder.py", line 337, in decode
    obj, end = self.raw_decode(s, idx=_w(s, 0).end())
  File "/nix/store/65cp4izx3bllnwqn7c7dhrq9h9gmjkal-python3-3.10.9/lib/python3.10/json/decoder.py", line 353, in raw_decode
    obj, end = self.scan_once(s, idx)
json.decoder.JSONDecodeError: Invalid \escape: line 9 column 16 (char 188)

I've attached a reproducible: Not really sure where to start here if I'd like to fix this

repro.tar.gz

Warning messages about unused partition inputs

Print a warning message if the gold or gate part of a partition contains unused inputs.

Unclear error reporting in the presence of multiple conflicting drivers

With the attached test case, when I run eqy -d run --force --jobs 40 4_eqy_test.eqy I get:

EQY 21:16:12 [run] partition: starting process "cd run; yosys -ql partition.log partition.ys"
EQY 21:16:15 [run] partition: ERROR: Multiple drivers for \_27797_.B2.
EQY 21:16:15 [run] partition: finished (returncode=1)

However I can not see more than one driver for the net attached to pin _27797_.B2. It would be helpful if the message gave the driver names (or at least two of them). It seems like a false error from what I can see but it prevents completion of the check.

bug.zip

Change satseq strategy to actually use k-induction

Widely differing behavior with different standard cell libs (but the same design)

I used the advice provided in #40 to successfully run a simple design with ASAP7 (runtime ~ 1m). But when I run the same design with skyhd130, I hit #40 for skyhd130

Test case has 2 directories (ignore the nangate45 directory)

Please let me know if there is anything else I can provide/help with to make the debug easier :).

bug.tar.gz

Support for UDP?

In asap7 the cells description in Verilog come from Liberate which uses UDP like:

primitive altos_latch (q, v, clk, d);
	output q;
	reg q;
	input v, clk, d;

	table
		* ? ? : ? : x;
		? 1 0 : ? : 0;
		? 1 1 : ? : 1;
		? x 0 : 0 : -;
		? x 1 : 1 : -;
		? 0 ? : ? : -;
	endtable
endprimitive

but I get errors when reading as soon as it sees this:

platforms/asap7/work_around_yosys/asap7sc7p5t_SEQ_RVT_TT_220101.v:37: ERROR: syntax error, unexpected TOK_ID

Are UDP supported in eqy? This is a common characterization tool so I expect this will be a common issue.

Bug in parsing partitions

Hi,

I am trying to do equivalence checking (Yosys 0.29 and EQY cc91b45) with the module attached in the zip file:

$ make
EQY 15:51:21 [script] read_gate: Warning: Replacing memory \mem with list of registers. See ibex_error.v:9281, ibex_error.v:9255
EQY 15:51:23 [script] read_gold: finished (returncode=0)
EQY 15:51:23 [script] read_gate: finished (returncode=0)
EQY 15:51:23 [script] combine: starting process "yosys -ql script/combine.log script/combine.ys"
EQY 15:51:23 [script] combine: finished (returncode=0)
EQY 15:51:24 [script] partition: starting process "cd script; yosys -ql partition.log partition.ys"
EQY 15:51:38 [script] partition: finished (returncode=0)
Traceback (most recent call last):
  File "/usr/local/bin/eqy", line 1208, in <module>
    main()
  File "/usr/local/bin/eqy", line 1181, in main
    make_scripts(ctx.args, ctx, ctx.job, strategies)
  File "/usr/local/bin/eqy", line 1016, in make_scripts
    cfg.partitions.append(EqyPartition(line, args, cfg, job))
  File "/usr/local/bin/eqy", line 999, in __init__
    for key, value in json.load(f).items():
  File "/usr/lib/python3.10/json/__init__.py", line 293, in load
    return loads(fp.read(),
  File "/usr/lib/python3.10/json/__init__.py", line 346, in loads
    return _default_decoder.decode(s)
  File "/usr/lib/python3.10/json/decoder.py", line 337, in decode
    obj, end = self.raw_decode(s, idx=_w(s, 0).end())
  File "/usr/lib/python3.10/json/decoder.py", line 353, in raw_decode
    obj, end = self.scan_once(s, idx)
json.decoder.JSONDecodeError: Invalid \escape: line 9 column 10 (char 158)
make: *** [Makefile:6: ibex_error] Error 1

The problem is that a generated partition json file contains a backslash:

"outbits": {
      "$1\mstatus_d[5:0]": [0]
    },

Which then cannot be parsed here:

eqy/src/eqy.py

Line 999 in cc91b45

for key, value in json.load(f).items():

A quick fix could be to remove all backslashes:

        with open(f"{args.workdir}/partitions/{self.name}.json", "r") as f:
            json_data = f.read()
            json_data = json_data.replace("\\","")
            for key, value in json.loads(json_data).items():

But I am not sure whether the generated json file actually should contain a backslash or not.

Thanks,
-Pascal

Move grouping commands to new [collect ...] section

The grouping commands ([no]autogroup, [no]group, [no]stop, [no]split) are interpreted out-of-order relative to the other commands in [partition ...]. I think therefore, it would be less confusing for users if we'd move them to a different section type. Maybe [collect ...] would be a good fit for a name. (Also, those commands are a bit more low-level and in most cases users will likely just want to keep the default settings for the grouping/collect step of partitioning.)

Unrelated cells sharing the same name can cause conflicting drivers in an amended partition (triggerd by the default ghdl-yosys-plugin output)

I am trying to use eqy in conjuction with ghdl-yosys-plugin. However, I get the following error:

ERROR: conflicting matches for gold bit $auto$ghdl.cc:806:import_module$28: $auto$ghdl.cc:806:import_module$100 vs $auto$ghdl.cc:806:import_module$42

There are many such auto-generated names in the netlist, so the next thing I tried was to add the following:

[match *]
nodefault
gold-match /^((?!import_module).)*$/

However, this has no effect on the error.

I am not sure if preventing those signals from being matched would fix the issue, or what the implications would be.

Therefore, I am wondering whether it is possible to use eqy with ghdl-yosys-plugin? If not, is this a limitation of eqy, or of ghdl-yosys-plugin?

Improve error message when encountering unmapped memories in a partition solved and using SBY

The SBY strategy uses xprop by default and xprop currently requires the memory to be mapped. The solution is to add memory_map -formal, but the error message that points to a memory is hidden in the SBY logfile. Since EQY knows which partitions contain memory it could produce a better error and/or just take care of mapping the memory.

Running eqy can final report error "Argument list too long"

Problem 1:

For the two provided designs the runtimes are as follows:

Design  Instance count    Runtime (simple)   Runtime (sby)
aes         32k                37m             257m
jpeg        55k               140m             900m

It is not clear if these run times are expected or is there something incorrect with the way we are using eqy.

Problem 2:

At the end of all the four runs (2 designs/2 different strategies) an error is encountered before creating the final report. The logfile for one run is available in aes/logfile.txt. Here is the last few lines of the logfile:

EQY 15:57:04 [aes] run: Running strategy 'sby' on 'aes_cipher_top.wire389.Y'..
EQY 15:57:05 [aes] run: Proved equivalence of partition 'aes_cipher_top.wire389.Y' using strategy 'sby'
EQY 15:57:05 [aes] run: make -f strategies.mk summary
EQY 15:57:05 [aes] run: make[1]: Entering directory '/home/harsh/bugs/eqy/aes'
EQY 15:57:05 [aes] run: make[1]: execvp: /bin/sh: Argument list too long
EQY 15:57:05 [aes] run: make[1]: *** [strategies.mk:825391: summary] Error 127
EQY 15:57:05 [aes] run: make[1]: Leaving directory '/home/harsh/bugs/eqy/aes'
EQY 15:57:05 [aes] run: make: *** [strategies.mk:825389: all] Error 2
EQY 15:57:05 [aes] run: make: Leaving directory '/home/harsh/bugs/eqy/aes'
EQY 15:57:05 [aes] run: finished (returncode=2)

Testcase data is public. The designs are here. And the library data is here

Recode sections are matched against the post-combine gold design but applied to the pre-combine gold design.

This makes it impossible to target signals where the module/name pair of a signal is different pre- and post-combine. As a workaround it's possible to manually flattening hierarchy levels only present on the gold side using the [gold] script, which makes the pre-combine and post-combine gold design match.

We could fix this by either a) applying the recode to the post-combine gold design or b) fixing the matching code to use the pre-combine gold ids (which it currently doesn't have access to).

EQY fails to prove a cell mapping equivalent

See the attached problem for EQY: t2.tar.gz

It is a purely combinational circuit mapped to standard cells. EQY is configured with

[gold]
read_verilog t2_gold.v

[gate]
read_liberty -ignore_miss_func t2_lib1.lib
read_verilog t2_mapping.v
hierarchy -top top

[strategy basic]
use sat
depth 10

and logs the following (redacted to the important parts)

EQY 20:11:10 [t2] Warning: Partition top.F contains 1 unused gold inputs.
EQY 20:11:10 [t2] Warning: Partition top.F contains 64 unused gate inputs.

...

EQY 20:11:10 [t2] run: Running strategy 'basic' on 'top.F'..
EQY 20:11:11 [t2] run: Could not prove equivalence of partition 'top.F' using strategy 'basic'

...

EQY 20:11:28 [t2] Warning: Failed to prove equivalence for 1/8 partitions:
EQY 20:11:28 [t2] Failed to prove equivalence of partition top.F

Meanwhile if I test with a Yosys script

read_verilog t2_gold.v
check -assert
design -stash gold

read_liberty -ignore_miss_func t2_lib1.lib
read_verilog t2_mapping.v
hierarchy -top top
flatten
check -assert

design -copy-from gold -as gold top
equiv_make gold top equiv
equiv_induct equiv
equiv_status -assert

the two netlists are proven equivalent.

The issue reproduces on the nightly OSS CAD Suite build: https://github.com/YosysHQ/oss-cad-suite-build/releases/tag/2024-04-26

ERROR: syntax error in *.eqy line 1

Hello!
I've tried to perform an equivalence checking for two Verilog modules with EQY. These modules come from TrustHub benchmark (https://trust-hub.org/#/benchmarks/chip-level-trojan) -- one of them is so called "trojan" (synt_c1355-CS1280.v), another one (c1355-CS1280.v) is trojan-free.
Here is my EQY fail.eqy script:

[gold]
read_verilog c1355-CS1280.v
prep -top c1355
memory_map

[gate]
read_verilog synt_c1355-CS1280.v
prep -top c1355
memory_map

[collect *]
group regfile*
join imm_*
join insn*

[strategy sby]
use sby
depth 10

When I try to use it with eqy -f fail.eqy, I receive the following error:

ERROR: syntax error in fail.eqy line 1

Am I missing something, or is it probably a bug?

I've attached an archive with the specified Verilog modules and *.eqy script here: c1355-CS1280.tar.gz.

Default partitioning of eqy fails to prove equivalence for circuit containing only "eq" and "neq", but succeeds if output is turned into internal wire

This is the smallest reproducer for the bug, given modules gate.v:

module comparators (
    b,
    a,
    eq,
    neq
);
    input [7:0] b;
    input [7:0] a;
    output eq;
    output neq;

    assign eq = a == b;
    assign neq = ~eq;
endmodule

and gold.v:

module comparators (
    b,
    a,
    eq,
    neq
);
    input [7:0] b;
    input [7:0] a;
    output eq;
    output neq;

    assign eq = a == b;
    assign neq = a != b;
endmodule

sby claims that the neq partitions are not equivalent. In the generated .vcd trace both eq and neq are shown with value 1 for gold.v which doesn't make sense, those 2 should always be a negation of each-other.

If I change eq to be a wire instead of an output then suddenly it is able to prove that neq is in fact equivalent.
(Note that introducing additional wires in gate.v doesn't help either).
I tried several smtbmc engines (bitwuzla, boolector) with the same result, the problem seems to be with the way the partition is created.

Reproduced the bug with oss-cad-suite-linux-x64-20230821.tgz running on Fedora 38.

I've attached the full working and failing inputs and the full logs created by eqy:
sbybug.zip

The warning about unconnected inputs here looks suspicious:

EQY 22:33:27 [equiv] read_gold: starting process "yosys -ql equiv/gold.log equiv/gold.ys"
EQY 22:33:27 [equiv] read_gold: finished (returncode=0)
EQY 22:33:27 [equiv] read_gate: starting process "yosys -ql equiv/gate.log equiv/gate.ys"
EQY 22:33:27 [equiv] read_gate: finished (returncode=0)
EQY 22:33:27 [equiv] combine: starting process "yosys -ql equiv/combine.log equiv/combine.ys"
EQY 22:33:27 [equiv] combine: finished (returncode=0)
EQY 22:33:27 [equiv] partition: starting process "cd equiv; yosys -ql partition.log partition.ys"
EQY 22:33:27 [equiv] partition: finished (returncode=0)
EQY 22:33:27 [equiv] Warning: Partition comparators.neq contains 1 unused gold inputs.
EQY 22:33:27 [equiv] Warning: Partition comparators.neq contains 2 unused gate inputs.
EQY 22:33:27 [equiv] run: starting process "make -C equiv -f strategies.mk"
EQY 22:33:27 [equiv] run: make: Entering directory '/var/home/edwin/ddca/bookhardcaml/_build/default/examples/0503/bug/fails/equiv'
EQY 22:33:27 [equiv] run: Running strategy 'sby' on 'comparators.eq'..
EQY 22:33:27 [equiv] run: Proved equivalence of partition 'comparators.eq' using strategy 'sby'
EQY 22:33:27 [equiv] run: Running strategy 'sby' on 'comparators.neq'..
EQY 22:33:27 [equiv] run: Could not prove equivalence of partition 'comparators.neq' using strategy 'sby': partitions not equivalent
EQY 22:33:27 [equiv] run: make -f strategies.mk summary
EQY 22:33:27 [equiv] run: make[1]: Entering directory '/var/home/edwin/ddca/bookhardcaml/_build/default/examples/0503/bug/fails/equiv'
EQY 22:33:27 [equiv] run: make[1]: Leaving directory '/var/home/edwin/ddca/bookhardcaml/_build/default/examples/0503/bug/fails/equiv'
EQY 22:33:27 [equiv] run: make: Leaving directory '/var/home/edwin/ddca/bookhardcaml/_build/default/examples/0503/bug/fails/equiv'
EQY 22:33:27 [equiv] run: finished (returncode=0)
EQY 22:33:27 [equiv] Successfully proved equivalence of partition comparators.eq
EQY 22:33:27 [equiv] Warning: Failed to prove equivalence for 1/2 partitions:
EQY 22:33:27 [equiv] Failed to prove equivalence of partition comparators.neq
EQY 22:33:27 [equiv] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
EQY 22:33:27 [equiv] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
EQY 22:33:27 [equiv] DONE (FAIL, rc=2)

What am I doing wrong?

make: yosys-config: No such file or directory

eqy stuck in infinite loop with gate design primitives (Xilinx gates) as blackboxes

Hi,
I guess I'm using naively the tool by comparing two netlists: initial RTL and one file after synthesis targeting Xilinx and providing Xilinx gates as blackboxes.
Still when doing so, the tool hangs in an infinite loop in the eqy execute, in particular in co_flatten_worker method.

I've attached a test case.

Versions I'm using:
Yosys 0.38+54 (git sha1 f8d4d7128, clang 15.0.0 -fPIC -Os)
eqy: latest (5791c90)

test_case.tar.gz

Thanks.
Christophe

Module patterns should actually be arbitrary hierarchical prefixes/contexts

The current design document has a strict separation of "module patterns", and "net patterns" that look up net names within that module. But what we actually want long-term is to support any hierarchical prefix in those module patterns, so that we are independent of flattening.

Thus, when we process the databases of IDs, we have to look at the original gold design hierarchy before combining and flattening, and collect all those prefixes, and then create a database with all proper module names.

Then, when we have a match for a "module pattern", we have to remove the part that matches the actual module ind the partially flattened design, and use the rest (with a dot appended at the end) as an implicit prefix for matching the net patterns within the matching module. (And for names that we assign to partitions, we also need to add that prefix to the user-supplied partition names.)