3991 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Clifford Wolf	59508c99b4	define PATH_MAX if not defined by limits.h	2016-10-11 12:12:09 +02:00
Clifford Wolf	11130d581d	Merge branch 'master' of github.com:cliffordwolf/yosys	2016-10-11 03:58:27 +02:00
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