83 commits

Author	SHA1	Message	Date
Clifford Wolf	2ed2e9c3e8	Change smtbmc "Warmup failed" status to "PREUNSAT" ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2019-10-03 14:59:07 +02:00
Clifford Wolf	bacca57537	Fix smtbmc.py handling of zero appended steps ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2019-03-14 22:04:42 +01:00
whitequark	efa278e232	Fix typographical and grammatical errors and inconsistencies. ... The initial list of hits was generated with the codespell command below, and each hit was evaluated and fixed manually while taking context into consideration. DIRS="kernel/ frontends/ backends/ passes/ techlibs/" DIRS="${DIRS} libs/ezsat/ libs/subcircuit" codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint More hits were found by looking through comments and strings manually.	2019-01-02 13:12:17 +00:00
Clifford Wolf	0b9bb852c6	Add yosys-smtbmc support for btor witness ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-12-10 03:43:07 +01:00
Clifford Wolf	47a5dfdaa4	Add "yosys-smtbmc --btorwit" skeleton ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-12-08 06:59:27 +01:00
Clifford Wolf	d0acea4f2e	Add proper error message for when smtbmc "append" fails ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-11-04 14:41:28 +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	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	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	9419de3e37	Add yosys-smtbmc VCD writer support for memories with async writes	2017-12-14 03:06:00 +01:00
Clifford Wolf	da91b31bb2	Fixed "yosys-smtbmc -g" handling of no solution	2017-11-27 19:43:36 +01:00
Clifford Wolf	dd46d76394	Fix a bug in yosys-smtbmc in ROM handling	2017-10-25 13:05:14 +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	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	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	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	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	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	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	5f6a838823	Added smtc support for top-level state with [], [N:] syntax	2016-10-08 12:25:34 +02:00
Clifford Wolf	34e2fb594d	Minor improvements in yosys-smtbmc	2016-09-24 20:40:22 +02:00
Clifford Wolf	2e244c2d8e	Added yosys-smtbmc --noinfo and --dummy	2016-09-19 20:43:28 +02:00
Clifford Wolf	d009cdd6ee	Improved handling of SMT2 logics in yosys-smtbmc	2016-09-18 20:48:09 +02:00
Clifford Wolf	7bc88e8101	yosys-smtbmc: added -i support smtc files	2016-09-18 00:48:36 +02:00
Clifford Wolf	d39db41df8	Work-around for boolector bug	2016-09-13 13:23:06 +02:00
Clifford Wolf	97b449fe55	yosys-smtbmc: flush stdout after each log msg	2016-09-06 01:40:31 +02:00
Clifford Wolf	fa5565b606	Added boolector support to yosys-smtbmc	2016-09-03 14:26:00 +02:00
Kaj Tuomi	d88cd0ae7f	More PEP 8 fixes.	2016-09-02 13:09:09 +03:00