328 commits

Author	SHA1	Message	Date
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
Clifford Wolf	a9c3acf5a2	Add SMT2 statebv mode (inactive for now)	2017-02-24 14:04:52 +01:00
Clifford Wolf	242c5f01de	Add "yosys-smtbmc -S <opt>"	2017-02-19 22:51:29 +01:00
Clifford Wolf	5541b42159	Add assert check in "yosys-smtbmc -c"	2017-02-04 21:22:17 +01:00
Clifford Wolf	adbecfee66	Improve yosys-smtbmc cover() support	2017-02-04 21:10:24 +01:00
Clifford Wolf	0c0784b6bf	Partially implement cover() support in yosys-smtbmc	2017-02-04 18:17:08 +01:00
Clifford Wolf	6abf79eb28	Further improve cover() support	2017-02-04 17:02:13 +01:00
Clifford Wolf	18ea65ef04	Add "yosys-smtbmc --aig <aim_filename>:<aiw_filename>" support	2017-01-30 11:38:43 +01:00
Clifford Wolf	e54c355b41	Add "yosys-smtbmc --aig-noheader" and AIGER mem init support	2017-01-28 15:15:02 +01:00
Clifford Wolf	b7cfb7dbd2	Fix $initstate handling bug in yosys-smtbmc	2017-01-11 14:14:12 +01:00
Clifford Wolf	b9ad91b93e	Implicitly set "yosys-smtbmc --noprogress" on windows	2017-01-04 15:23:48 +01:00
Clifford Wolf	ed812ea39c	Fixed "yosys-smtbmc --noprogress"	2017-01-04 12:03:04 +01:00
Clifford Wolf	81bb952e5d	Handle "always 1" like "always -1" in .smtc files	2017-01-02 20:08:03 +01:00
Clifford Wolf	37760541bd	Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aig	2016-12-03 12:37:20 +01:00
Clifford Wolf	88b9733253	Added "yosys-smtbmc --aig"	2016-12-01 13:16:57 +01:00
Clifford Wolf	52c243cf05	Added support for partially initialized regs to smt2 back-end	2016-12-01 12:00:00 +01:00
Clifford Wolf	df2e5aad6f	Bugfix in smt2 back-end for pure checker modules	2016-11-28 15:15:09 +01:00
Clifford Wolf	c17d98f55c	Removed shebang line from smtio.py, fixes #279	2016-11-27 12:11:04 +01:00
Clifford Wolf	f257ccf22e	Added "yosys-smtbmc --append"	2016-11-22 21:21:13 +01:00
Clifford Wolf	281a977b39	Ignore L_pi nets in "yosys-smtbmc --cex"	2016-10-18 10:54:53 +02:00
Clifford Wolf	0bcc617a4f	Added "yosys-smtbmc --cex <filename>"	2016-10-17 14:57:28 +02:00
Clifford Wolf	189fbd4cf8	cleanup in write_smt2 log messages (-bv and -mem are now default)	2016-10-16 23:02:51 +02:00
Clifford Wolf	bdc316db50	Added $anyseq cell type	2016-10-14 15:24:03 +02:00
Clifford Wolf	8ebba8a35f	Added $ff and $_FF_ cell types	2016-10-12 01:18:39 +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	9aec8a1672	yosys-smtbmc: added smtc [...] support for cells	2016-10-02 22:08:30 +02:00