riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
12,093 Commits 81 Branches 48 Tags 64 MiB
Commit Graph

12093 Commits

Author SHA1 Message Date
Jannis Harder 1d40f5e8fa smtbmc: Avoid unnecessary string copies when parsing solver output 2022-09-02 22:37:08 +02:00
github-actions[bot] 6e907acf86 Bump version 2022-09-01 00:18:29 +00:00
Miodrag Milanović d8a383b555
Merge pull request #3087 from tgingold-cern/sf2 
complete support for microsemi smartfusion2 and igloo2bar
 2022-08-31 09:30:09 +02:00
N. Engelhardt d829d7fe00
Merge pull request #3458 from QuantamHD/abc_faster 2022-08-31 08:58:42 +02:00
Tristan Gingold 1e0e3bd48e sf2: add NOTES about using yosys for smartfusion2 and igloo2 2022-08-31 08:40:44 +02:00
Tristan Gingold 0f6cf8b8e4 sf2: add a test for $alu gate 2022-08-31 08:40:44 +02:00
Tristan Gingold c25f3ff3df sf2: suport $alu gate and ARI1 implementation 2022-08-31 08:40:44 +02:00
Tristan Gingold 13ccdd032d synth_sf2: purge on last clean 
LiberoSoc don't like unused nets.
 2022-08-31 08:40:44 +02:00
Tristan Gingold 39993a92d7 sf2/cells_sim.v: add XTLOSC, SYSRESET cells 2022-08-31 08:40:44 +02:00
Tristan Gingold 1c0119aa90 sf2/cells_sim.v: add IOSTD parameter to I/O cells 
This parameter is set by LiberoSoc IPs, so it is needed to avoid
errors when using those IPs.
 2022-08-31 08:40:43 +02:00
Tristan Gingold 4543751a77 synth_sf2: add -discard-ffinit option to discard ff initial value 
sf2 ff have no initial values, but some IP cores use initial values.
In order to use those cores on sf2, it is required to discard the
initial value (to be carefully used).
 2022-08-31 08:40:43 +02:00
github-actions[bot] 7117817dbe Bump version 2022-08-30 00:21:44 +00:00
Miodrag Milanović a8506c1c76
Merge pull request #3463 from YosysHQ/micko/hierarchy_fix 
Makes sure to set initial_top when top change, fixes #3462
 2022-08-29 10:12:34 +02:00
Miodrag Milanovic 5b5fe76966 Add test for bug 3462 2022-08-29 10:10:09 +02:00
Miodrag Milanovic 883831bd24 Fix mingw build 2022-08-29 10:04:12 +02:00
Miodrag Milanovic 4bc1e1d1f1 Makes sure to set initial_top when change, fixes #3462 2022-08-26 17:12:56 +02:00
github-actions[bot] 060cbd3e9e Bump version 2022-08-26 00:19:20 +00:00
N. Engelhardt 0d8ee63d03
Merge pull request #3461 from YosysHQ/aki/hashlib_assert 2022-08-25 17:09:41 +02:00
Aki Van Ness 6717e02023
kernel: hashlib: cleaned up message about table size in cases where `sizeof(int) == 4`, (closes #3440) 2022-08-25 11:08:51 -04:00
N. Engelhardt 7d35003c16
Merge pull request #3449 from YosysHQ/aki/show_pathrw 2022-08-25 17:06:29 +02:00
N. Engelhardt e3eb114e75 use inttypes format specifiers 2022-08-25 13:36:51 +02:00
N. Engelhardt 7e92e80741 dump runtime information for passes to json 2022-08-25 13:36:51 +02:00
N. Engelhardt 8e640663d6
Merge pull request #3457 from KrystalDelusion/docs_width 2022-08-25 11:41:12 +02:00
Ethan Mahintorabi 114253cd54 Improves ABC command runtime by 10-100x 
After speaking with the author of ABC he let me know that ifraig is a very old command, and that &get; &fraig -x; &put is over 100x faster than ifraig with improved PPA results.

After making the change I confirmed that this is in fact a major speed up. On our internal designs in O(millions) of standard cells we saw multi hour reductions in runtime.

Also included is an improvement to the dress command. Using AIG based transformations removes the spec it SATs against. Proving the input blif will make sure that no matter what commands are run the dress command can still do its job. I noticed a regression against some LUT mapping jobs that prompted me to fix this.
 2022-08-24 00:35:02 +00:00
KrystalDelusion 9465b2af95 Fitting help messages to 80 character width 
Uses the regex below to search (using vscode):
	^\t\tlog\("(.{10,}(?<!\\n)|.{81,}\\n)"\);

Finds any log messages double indented (which help messages are)
and checks if *either* there are is no newline character at the end,
*or* the number of characters before the newline is more than 80.
 2022-08-24 10:40:57 +12:00
Aki Van Ness 1433a63165
yosys: passes: cmds: show: added filename re-writing to `show -lib` 2022-08-22 06:04:54 -04:00
Archie 15a0697c70 Adding check for BLIF names command input plane size. 2022-08-21 23:18:20 -05:00
Archie db73f3c26b Merge branch 'master' of https://github.com/ALGCDG/yosys 2022-08-21 17:18:20 -05:00
github-actions[bot] 029c2785e8 Bump version 2022-08-19 00:19:27 +00:00
Jannis Harder f1c9399b66
Merge pull request #3450 from jix/write_aiger_nonff 
write_aiger: Fix non-$_FF_ FFs
 2022-08-18 16:50:56 +02:00
Jannis Harder 5142fb3b5c write_aiger: Fix non-$_FF_ FFs 
This broke while switching sby's formal flows to always use $_FF_'s.
 2022-08-18 13:56:22 +02:00
github-actions[bot] 1c36f4cc2c Bump version 2022-08-17 00:18:21 +00:00
Jannis Harder 556d008ed3
Merge pull request #3434 from jix/witness_flow 
Updated formal flow with new witness format
 2022-08-16 14:18:35 +02:00
Jannis Harder f7023d06a2 sim: -hdlname option to preserve flattened hierarchy in sim output 2022-08-16 13:37:30 +02:00
Jannis Harder 66f761a8c5 smtbmc: Set step range for --yw and dont skip steps for --check-witness 2022-08-16 13:37:30 +02:00
Jannis Harder 927af914f1 Update CEX minimization patches for abc 2022-08-16 13:37:30 +02:00
Jannis Harder 4ad13c647e clk2fflogic: Generate less unused logic when using verific 
Verific generates a lot of FFs with an unused async load and we cannot
always optimize that away before running clk2fflogic, so check for that
special case here.
 2022-08-16 13:37:30 +02:00
Jannis Harder 65145db7e7 rename: Add -witness mode 2022-08-16 13:37:30 +02:00
Jannis Harder b156fe903f yosys-witness: Add stats command 2022-08-16 13:37:30 +02:00
Jannis Harder 475267ac25 smtbmc: Add --check-witness mode 
This verifies that the given constraints force an assertion failure.
This is useful to debug witness trace conversion (and minimization).
 2022-08-16 13:37:30 +02:00
Jannis Harder efd5b86eb9 aiger: Add yosys-witness support 
Adds a new json based aiger map file and yosys-witness converters to us
this to convert between native and AIGER witness files.
 2022-08-16 13:37:30 +02:00
Jannis Harder f041e36c6e smtbmc: Add native json based witness format + smt2 backend support 
This adds a native json based witness trace format. By having a common
format that includes everything we support, and providing a conversion
utility (yosys-witness) we no longer need to implement every format for
every tool that deals with witness traces, avoiding a quadratic
opportunity to introduce subtle bugs.

Included:

  * smt2: New yosys-smt2-witness info lines containing full hierarchical
    paths without lossy escaping.
  * yosys-smtbmc --dump-yw trace.yw: Dump results in the new format.
  * yosys-smtbmc --yw trace.yw: Read new format as constraints.
  * yosys-witness: New tool to convert witness formats.
    Currently this can only display traces in a human-readable-only
    format and do a passthrough read/write of the new format.
  * ywio.py: Small python lib for reading and writing the new format.
    Used by yosys-smtbmc and yosys-witness to avoid duplication.
 2022-08-16 13:37:30 +02:00
Jannis Harder 96a1173598 btor: Support $anyinit cells 2022-08-16 13:37:30 +02:00
Jannis Harder 5893cae647 aiger: Support $anyinit cells 2022-08-16 13:37:30 +02:00
Jannis Harder 021c3c8da5 smt2: Support $anyinit cells 2022-08-16 13:37:30 +02:00
Jannis Harder a2f9ebe43a memory_map: Add -formal option 
This maps memories for a global clock based formal verification flow.
This implies -keepdc, uses $ff cells for ROMs and sets hdlname
attributes.
 2022-08-16 13:37:30 +02:00
Jannis Harder 0cdb14df41 setundef: Do not add anyseq / anyconst to unused memory port clocks 
Instead set those unused clocks to zero.
 2022-08-16 13:37:30 +02:00
Jannis Harder 428ad5b9fd wreduce: Keep more x-bits with -keepdc 2022-08-16 13:37:30 +02:00
Jannis Harder 95db5a9d38 formalff: New -setundef option 
Find FFs with undefined initialization values for which changing the
initialization does not change the observable behavior and initialize
them. For -ff2anyinit, this reduces the number of generated $anyinit
cells that drive wires with private names.
 2022-08-16 13:37:30 +02:00
Jannis Harder a5e1d3b997 formalff: Set new replaced_by_gclk attribute on removed dff's clks 
This attribute can be used by formal backends to indicate which clocks
were mapped to the global clock. Update the btor and smt2 backend which
already handle clock inputs to understand this attribute.
 2022-08-16 13:37:30 +02:00