Clifford Wolf
|
5f6a838823
|
Added smtc support for top-level state with [], [N:] syntax
|
2016-10-08 12:25:34 +02:00 |
Clifford Wolf
|
5f7c5e685b
|
Bugfix in yosys-smtbmc --noincr
|
2016-10-04 00:54:44 +02:00 |
Clifford Wolf
|
1114ce9210
|
yosys-smtbmc: ABC is a QF_BV solver
|
2016-10-03 20:43:38 +02:00 |
Clifford Wolf
|
99b2093bc4
|
Added "yosys-smtbmc --noincr"
|
2016-10-03 20:30:38 +02:00 |
Clifford Wolf
|
e586e5e15a
|
Update ABV to hg rev eb6eca6807cc
|
2016-10-02 22:08:53 +02:00 |
Clifford Wolf
|
9aec8a1672
|
yosys-smtbmc: added smtc [...] support for cells
|
2016-10-02 22:08:30 +02:00 |
Clifford Wolf
|
4eb0d6fc0e
|
Added "yosys-smtbmc -s abc"
|
2016-10-01 13:54:21 +02:00 |
Clifford Wolf
|
23594597bc
|
Updated ABV to hg rev 6b74de13c57f
|
2016-10-01 12:23:24 +02:00 |
Clifford Wolf
|
76352c99c9
|
Added "prep -nokeepdc"
|
2016-09-30 17:02:52 +02:00 |
Clifford Wolf
|
ed519f578e
|
Added "opt_rmdff -keepdc"
|
2016-09-30 17:02:38 +02:00 |
Clifford Wolf
|
ca5462523e
|
Updated ABV to hg rev 2bc57cc30593
|
2016-09-30 10:56:36 +02:00 |
Clifford Wolf
|
34e2fb594d
|
Minor improvements in yosys-smtbmc
|
2016-09-24 20:40:22 +02:00 |
Clifford Wolf
|
8f5bf6de32
|
Added liberty parser support for types within cell decls
|
2016-09-23 13:53:23 +02:00 |
Clifford Wolf
|
6300c0b3c2
|
Merge branch 'master' of https://github.com/brouhaha/yosys
|
2016-09-23 13:42:08 +02:00 |
Eric Smith
|
f4240cc8a4
|
Add optional SEED=n command line option to Makefile, and -S n command line option to test scripts, for deterministic regression tests.
|
2016-09-22 11:49:29 -06:00 |
Clifford Wolf
|
0c697b9eac
|
Added autotest.sh -I
|
2016-09-20 09:29:56 +02:00 |
Clifford Wolf
|
e788ad4885
|
Cosmetic fix in test_autotb.cc
|
2016-09-19 20:43:43 +02:00 |
Clifford Wolf
|
2e244c2d8e
|
Added yosys-smtbmc --noinfo and --dummy
|
2016-09-19 20:43:28 +02:00 |
Clifford Wolf
|
5e155aa121
|
Avoid creating very long strings in test_autotb
|
2016-09-19 10:20:20 +02:00 |
Clifford Wolf
|
aaa99c35bd
|
Added $past, $stable, $rose, $fell SVA functions
|
2016-09-19 01:30:07 +02:00 |
Clifford Wolf
|
d009cdd6ee
|
Improved handling of SMT2 logics in yosys-smtbmc
|
2016-09-18 20:48:09 +02:00 |
Clifford Wolf
|
13a03b84d4
|
Added support for bus interfaces to "read_liberty -lib"
|
2016-09-18 18:48:59 +02:00 |
Clifford Wolf
|
0ead5a9e44
|
Merge branch 'master' of github.com:cliffordwolf/yosys
|
2016-09-18 00:50:02 +02:00 |
Clifford Wolf
|
7bc88e8101
|
yosys-smtbmc: added -i support smtc files
|
2016-09-18 00:48:36 +02:00 |
Clifford Wolf
|
d8ad889594
|
Bugfix in techmap parameter handling
|
2016-09-14 20:46:54 +02:00 |
Clifford Wolf
|
d39db41df8
|
Work-around for boolector bug
|
2016-09-13 13:23:06 +02:00 |
Clifford Wolf
|
d01e34136e
|
Merge pull request #228 from Kmanfi/test
Fix for modules with big interfaces.
|
2016-09-13 12:34:19 +02:00 |
Kaj Tuomi
|
2c031cd24f
|
Fix for modules with big interfaces.
|
2016-09-13 13:13:27 +03:00 |
Clifford Wolf
|
6f416c1953
|
Added missing :produce-models setting to smtio.py
|
2016-09-11 18:17:22 +02:00 |
Clifford Wolf
|
5199aafca0
|
Minor improvements to smtio.py vcd writer
|
2016-09-10 16:24:08 +02:00 |
Clifford Wolf
|
b582f11074
|
fixed write_smt2 for (non-combinatorial) loops through hierarchical cells
|
2016-09-10 15:14:41 +02:00 |
Clifford Wolf
|
3ceba145d5
|
smt2 mem init bugfix
|
2016-09-08 18:08:15 +02:00 |
Clifford Wolf
|
2c0d818296
|
Merge branch 'master' of github.com:cliffordwolf/yosys
|
2016-09-08 11:17:05 +02:00 |
Clifford Wolf
|
14bfd3c5c1
|
yosys-smtbmc meminit support
|
2016-09-08 11:16:12 +02:00 |
Clifford Wolf
|
9e72046906
|
Merge pull request #225 from Kmanfi/test
Typo fix.
|
2016-09-08 10:06:40 +02:00 |
Kaj Tuomi
|
df4ab169a7
|
Typo fix.
|
2016-09-08 10:57:16 +03:00 |
Clifford Wolf
|
209a3d9ffc
|
Bugfix in "yosys-smtbmc --unroll"
|
2016-09-07 21:01:51 +02:00 |
Clifford Wolf
|
6770d6e0f8
|
Added "yosys-smtbmc --unroll"
|
2016-09-07 20:57:56 +02:00 |
Clifford Wolf
|
ceff7ecd91
|
Install celledges.h
|
2016-09-07 13:43:57 +02:00 |
Clifford Wolf
|
cb7dbf4070
|
Improvements in assertpmux
|
2016-09-07 12:42:16 +02:00 |
Clifford Wolf
|
e2570ffb87
|
Updated ABC to hg 8e08604f8ad3
|
2016-09-07 11:08:54 +02:00 |
Clifford Wolf
|
ab18e9df7c
|
Added assertpmux
|
2016-09-07 00:28:01 +02:00 |
Clifford Wolf
|
f3f5a02045
|
Added "tee +INT -INT"
|
2016-09-06 17:43:24 +02:00 |
Clifford Wolf
|
fc5281b3f7
|
Run log_flush() before solving in sat command
|
2016-09-06 17:35:25 +02:00 |
Clifford Wolf
|
d55a93b39f
|
Bugfix in parsing of BLIF latch init values
|
2016-09-06 17:35:06 +02:00 |
Clifford Wolf
|
97583ab729
|
Avoid creation of bogus initial blocks for assert/assume in always @*
|
2016-09-06 17:34:42 +02:00 |
Larry Doolittle
|
dcb5a6ea8a
|
Fix spelling and grammar in README
|
2016-09-06 11:25:33 +02:00 |
Clifford Wolf
|
97b449fe55
|
yosys-smtbmc: flush stdout after each log msg
|
2016-09-06 01:40:31 +02:00 |
Clifford Wolf
|
372d672c2a
|
Minor bugfix in write_smt2
|
2016-09-04 16:32:47 +02:00 |
Clifford Wolf
|
19a3b3732c
|
Minor README updates
|
2016-09-03 18:49:53 +02:00 |