207 commits

Author	SHA1	Message	Date
Clifford Wolf	77bd645c35	Add $mem support to SMT2 clock tagging ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-27 02:11:20 +02:00
Clifford Wolf	3f00702475	Improve yosys-smtbmc log output and error handling ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-17 18:06:17 +01:00
Clifford Wolf	4d4e3a8ca6	Improve handling of invalid check-sat result in smtio.py ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-17 12:17:53 +01:00
Clifford Wolf	3545c0fffb	Remove debug prints from yosys-smtbmc VCD writer ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-08 16:24:35 +01:00
Clifford Wolf	8b604004da	Check results of (check-sat) in yosys-smtbmc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-07 22:54:19 +01:00
Clifford Wolf	cedbc35f4b	Imporove yosys-smtbmc error handling, Improve VCD output ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-05 12:17:22 +01:00
Clifford Wolf	8b7602e660	Improve SMT2 encoding of $reduce_{and,or,bool} ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 21:22:20 +01:00
Clifford Wolf	45a6fce92c	Fix a hangup in yosys-smtbmc error handling ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 21:13:30 +01:00
Clifford Wolf	ae4e204c76	Improved error handling in yosys-smtbmc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-03 20:00:07 +01:00
Clifford Wolf	a44e1edaa3	Terminate running SMT solver when smtbmc is terminated ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-03 14:50:40 +01:00
Clifford Wolf	3ced2cca6e	Fix smtbmc smtc/aiw parser for wire names containing [] ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-03 14:15:49 +01:00
Clifford Wolf	90ae426078	Mangle names with square brackets in VCD files to work around issues in gtkwave ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-01 14:15:27 +01:00
Clifford Wolf	675dd5347a	Small fixes and improvements in $allconst/$allseq handling ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-26 11:58:44 +01:00
Clifford Wolf	b13e6bd375	Add smtbmc support for exist-forall problems ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-23 19:33:30 +01:00
Clifford Wolf	17583b6a21	Add support for mockup clock signals in yosys-smtbmc vcd output ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-20 17:45:22 +01:00
Clifford Wolf	c9672e2e2e	Fix handling of zero-length cell connections in SMT2 back-end ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-08 19:12:12 +01:00
Clifford Wolf	e97f10b142	Fix smtio.py for large SMT2 S-expressions	2018-01-29 12:34:28 +01:00
Clifford Wolf	54aeca0983	Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output	2018-01-18 14:25:22 +01:00
Clifford Wolf	9419de3e37	Add yosys-smtbmc VCD writer support for memories with async writes	2017-12-14 03:06:00 +01:00
Clifford Wolf	2625da6440	Add smt2 back-end support for async write memories	2017-12-14 02:07:10 +01:00
Clifford Wolf	da91b31bb2	Fixed "yosys-smtbmc -g" handling of no solution	2017-11-27 19:43:36 +01:00
Clifford Wolf	455c1c9d97	Fix SMT2 handling of initstate in sub-modules	2017-10-29 13:21:20 +01:00
Clifford Wolf	1170508264	Improve smtio performance by using reader thread, not writer thread	2017-10-26 01:01:55 +02:00
Clifford Wolf	f513494f5f	Use separate writer thread for talking to SMT solver to avoid read/write deadlock	2017-10-25 19:59:56 +02:00
Clifford Wolf	76326c163a	Improve p_* functions in smtio.py	2017-10-25 15:45:32 +02:00
Clifford Wolf	c672c321e3	Capsulate smt-solver read/write in separate functions	2017-10-25 13:37:11 +02:00
Clifford Wolf	dd46d76394	Fix a bug in yosys-smtbmc in ROM handling	2017-10-25 13:05:14 +02:00
Clifford Wolf	c2d737457a	Fix bug in write_smt2 (export logic driving hierarchical cells before exporting regs)	2017-08-25 11:44:48 +02:00
Clifford Wolf	48b2b376d0	Add "yosys-smtbmc --smtc-init --smtc-top --noinit"	2017-08-04 17:09:08 +02:00
Clifford Wolf	3a8f6f0f51	Add verilator support to testbenches generated by yosys-smtbmc	2017-07-21 14:33:29 +02:00
Clifford Wolf	10c7709e68	Generate FSM-style testbenches in smtbmc	2017-07-12 15:57:04 +02:00
Clifford Wolf	3c693b6561	Change s/asserts/assertions/ in yosys-smtbmc log messages	2017-07-07 11:52:25 +02:00
Clifford Wolf	8f7404f82c	Add "yosys-smtbmc --presat"	2017-07-07 02:47:30 +02:00
Clifford Wolf	3e0948e16f	Remove unneeded delays in smtbmc vlogtb	2017-07-03 15:37:17 +02:00
Clifford Wolf	ea805af6f5	Add "yosys-smtbmc --vlogtb-top"	2017-07-01 18:19:23 +02:00
Clifford Wolf	7d2fb6e2fc	Fix smtbmc vlogtb bug in $anyseq handling	2017-07-01 02:13:32 +02:00
Clifford Wolf	8f8baccfde	Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand const reg"	2017-06-07 12:30:24 +02:00
Clifford Wolf	d9201b85f3	Change default smt2 solver to yices (Yices 2 has switched its license to GPL)	2017-05-27 11:56:01 +02:00
Clifford Wolf	05cdd58c8d	Add $_ANDNOT_ and $_ORNOT_ gates	2017-05-17 09:08:29 +02:00
Clifford Wolf	1a4b7c6bfa	Fix boolector support in yosys-smtbmc	2017-05-08 14:33:22 +02:00
Clifford Wolf	106e44f406	Add "write_smt2 -stdt" mode	2017-03-20 12:00:35 +01:00
Clifford Wolf	c855353986	Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg	2017-03-04 23:41:54 +01:00
Clifford Wolf	fbd52ec6dd	Use hex addresses in smtbmc vcd mem traces	2017-02-28 13:54:50 +01:00
Clifford Wolf	2203562268	Add smtbmc support for memory vcd dumping	2017-02-26 21:26:32 +01:00
Clifford Wolf	80ecd7a26f	Fix extra newline bug in write_smt2	2017-02-26 14:41:27 +01:00
Clifford Wolf	6e152f7aa1	Fix bug in smtio unroll code	2017-02-26 14:39:07 +01:00
Clifford Wolf	66a1617b69	Fix assert checking in "yosys-smtbmc -c --append"	2017-02-26 11:06:26 +01:00
Clifford Wolf	fd1cc0c73d	Improve (and fix for stbv mode) SMT2 memory API	2017-02-26 10:58:34 +01:00
Clifford Wolf	38bf458037	Add support for "yosys-smtbmc -c --append"	2017-02-25 23:41:40 +01:00
Clifford Wolf	7af9727f78	Add "write_smt2 -stbv"	2017-02-24 18:24:53 +01:00