Commit Graph

9065 Commits

Author SHA1 Message Date
Alberto Gonzalez 0fda8308bc Add support for optimizing exists-forall problems.
Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate.
Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al.
Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
2020-03-13 17:10:29 +00:00
Miodrag Milanovic 395daf6ced exclude clang from checking 2020-03-13 17:23:27 +01:00
Miodrag Milanovic 8f221118d2 Add YS_ prefix to macros, add explanation and apply to older version as well 2020-03-13 17:19:54 +01:00
Claire Wolf c0a009139b
Merge pull request #1764 from Xiretza/fix-abcrev-check
Improve ABC repository management in Makefile
2020-03-13 16:54:19 +01:00
Eddie Hung 432a09af80 kernel: SigSpec use more const& + overloads to prevent implicit SigSpec 2020-03-13 08:17:39 -07:00
Miodrag Milanovic 5b73e7c63a Added back tests for logger 2020-03-13 15:00:18 +01:00
Miodrag Milanovic 7c54e61979 Use boost xpressive for gcc 4.8 2020-03-13 14:58:35 +01:00
Miodrag Milanovic 746629f18d remove include where not used 2020-03-13 14:55:53 +01:00
Claire Wolf 29e2b2dc05 Add info-file and cover features to write_btor
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-13 13:46:32 +01:00
Eddie Hung b567f03c26 kernel: optimise Module::remove(const pool<RTLIL::Wire*>() 2020-03-12 16:00:34 -07:00
Eddie Hung a076052fe4 kernel: SigPool to use const& + overloads to prevent implicit SigSpec 2020-03-12 16:00:34 -07:00
Xiretza 9dedac50e2
Improve ABC repository management in Makefile
`rev-parse --short` output may have a different abbreviated hash length than
ABCREV, so a simple string comparison always fails, even if the correct
commit is checked out. Pass both commits through rev-parse and then
compare the full hashes instead.

Add an `echo-abc-rev` target so that packaging scripts can set ABCPULL=0 and
handle all the git nastiness themselves.
2020-03-12 19:26:21 +01:00
Miodrag Milanovic a0cc795e85 Added filter-out for libyosys.so 2020-03-12 18:28:20 +01:00
Miodrag Milanovic f37f558f72 Revert "Clean up 'install' Makefile target"
This reverts commit 2a746234fe.
2020-03-12 18:26:19 +01:00
Miodrag Milanovic 178a8e3bff Revert "Improve ABC repository management in Makefile"
This reverts commit 90404e1969.
2020-03-12 18:26:07 +01:00
Miodrag Milanović af84e5acf1
Merge pull request #1666 from Xiretza/improve-makefile
Makefile improvements for packaging scripts
2020-03-12 16:14:48 +02:00
N. Engelhardt 6986371bac
Merge pull request #1751 from boqwxp/add_assert
Extend `add` command to allow adding $assert cells.
2020-03-12 11:18:35 +01:00
Miodrag Milanovic 82ad422b4e Add mandatory wasm file to zip file as well 2020-03-12 11:17:15 +01:00
Miodrag Milanović d38098e5fa
Merge pull request #1757 from jiegec/fix-emcc
Fix compilation for emcc
2020-03-12 12:16:28 +02:00
Marcus Comstedt 5e94bf0291 refixed parsing of constant with comment between size and value
The three parts of a based constant (size, base, digits) are now three
separate tokens, allowing the linear whitespace (including comments)
between them to be treated as normal inter-token whitespace.
2020-03-11 18:21:44 +01:00
jiegec 26137d8bb7 Add EXTRA_EXPORTED_RUNTIME_METHODS env for yosysjs 2020-03-11 23:01:04 +08:00
jiegec 7b679eecb3 Fix compilation for emcc 2020-03-11 22:09:24 +08:00
Eddie Hung 3ada82639f verilog: add test 2020-03-11 06:51:03 -07:00
Eddie Hung dd8ebf7873
Merge pull request #1743 from YosysHQ/eddie/abc9_keep
abc9: improve (* keep *) handling
2020-03-11 06:32:15 -07:00
Eddie Hung d624a11dd1
Merge pull request #1744 from YosysHQ/eddie/fix1675
Bump ABCREV to receive fix for #1675
2020-03-11 06:31:06 -07:00
Alberto Gonzalez 005dd601ab
Extend `add` command to allow adding cells for verification like $assert, $assume, etc. 2020-03-10 21:49:22 +00:00
Eddie Hung 2d63bf5877 verilog: also set location for simple_behavioral_stmt 2020-03-10 10:29:24 -07:00
David Shah f2550d45ff
Merge pull request #1753 from YosysHQ/dave/abc9-speedup
Add ScriptPass::run_nocheck and use for abc9
2020-03-10 13:51:59 +00:00
David Shah ddcd87b577
Merge pull request #1721 from YosysHQ/dave/tribuf-unused
deminout: Don't demote inouts with unused bits
2020-03-10 13:51:40 +00:00
N. Engelhardt f91705cf8a
Merge pull request #1755 from boqwxp/add_cmd_cleanup
Clean up `passes/cmds/add.cc` code style.
2020-03-10 13:10:50 +01:00
Alberto Gonzalez 47537f2e42
Clean up passes/cmds/add.cc code style. 2020-03-10 10:37:10 +00:00
Alberto Gonzalez da8270aa01
Set AST source locations in more parser rules. 2020-03-10 01:50:39 +00:00
Eddie Hung d23acf8c61
Merge pull request #1747 from YosysHQ/claire/partselfix
Fix partsel expr bit width handling and add test case
2020-03-09 11:51:57 -07:00
David Shah b8abf14376 Add ScriptPass::run_nocheck and use for abc9
Signed-off-by: David Shah <dave@ds0.me>
2020-03-09 14:34:22 +00:00
N. Engelhardt 282d331e7e
Merge pull request #1716 from zeldin/ecp5_fix
ecp5: remove unused parameter from \$__ECP5_PDPW16KD
2020-03-09 11:04:08 +01:00
Claire Wolf a7cc4673c3 Fix partsel expr bit width handling and add test case
Signed-off-by: Claire Wolf <claire@symbioticeda.com>
2020-03-08 16:12:12 +01:00
Eddie Hung 3be7784d0e xaiger: remove some unnecessary operations ...
... since they can not be triggered by (* keep *) anymore
(but could still be triggered by (* abc9_scc *) !?!)
2020-03-06 10:51:47 -08:00
Eddie Hung 7a89ed1fa2 Bump ABCREV to receive fix for #1675 2020-03-06 10:32:48 -08:00
Eddie Hung 80dcc8a0d1 abc9: for sccs, create a new wire instead of using entirety of existing 2020-03-06 10:30:07 -08:00
Eddie Hung 91a7a74ac4 abc9: (* keep *) wires to be PO only, not PI as well; fix scc handling 2020-03-06 10:20:30 -08:00
Eddie Hung 2335c59e5b abc: add abc.debug scratchpad option 2020-03-06 10:09:01 -08:00
N. Engelhardt 8a39a580e1 remove unused parameters 2020-03-06 16:45:36 +01:00
Miodrag Milanović bfeba9ad11
Merge pull request #1742 from nakengelhardt/rpc-test-again
More rpc test fixes
2020-03-06 16:06:54 +01:00
N. Engelhardt 88494e81f5 rpc test: make frontend listen before launching yosys & introduce safeguard if yosys errors 2020-03-06 15:29:01 +01:00
Eddie Hung 8b074cc473
Merge pull request #1739 from YosysHQ/eddie/issue1738
ice40: fix specify for -device {lp,u}
2020-03-05 09:41:54 -08:00
Eddie Hung 69f1555058 ice40: fix specify for ICE40_{LP,U} 2020-03-05 08:11:49 -08:00
Eddie Hung 3c2e910bb3 tests: extend tests/arch/run-tests.sh for defines 2020-03-05 08:08:32 -08:00
Eddie Hung 0930c00f03 ice40: fix implicit signal in specify, also clamp negative times to 0 2020-03-04 15:28:17 -08:00
Eddie Hung 6eb528277e
Merge pull request #1735 from YosysHQ/eddie/abc9_dsp48e1
xilinx: cleanup DSP48E1 handling for abc9
2020-03-04 13:37:09 -08:00
Eddie Hung 7b543fdb0c xilinx: consider DSP48E1.ADREG 2020-03-04 12:04:02 -08:00