yosyshq / eqy Goto Github PK
View Code? Open in Web Editor NEWEquivalence checking with Yosys
Home Page: https://yosyshq.readthedocs.io/projects/eqy/en/latest/
License: Other
Equivalence checking with Yosys
Home Page: https://yosyshq.readthedocs.io/projects/eqy/en/latest/
License: Other
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
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?
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?
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
Print a warning message if the gold or gate part of a partition contains unused inputs.
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.
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 :).
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.
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:
Line 999 in cc91b45
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
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.)
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?
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.
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
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).
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
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.
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?
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)
Thanks.
Christophe
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.)
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.