434 commits

Author	SHA1	Message	Date
Clifford Wolf	292984896b	Simple fix BTOR memory encoding	2017-12-17 18:57:54 +01:00
Clifford Wolf	bbdcc1f9d4	Improve BTOR memory encoding	2017-12-17 18:55:17 +01:00
Clifford Wolf	30f23281ed	Add array support to btor back-end	2017-12-15 02:19:06 +01:00
Clifford Wolf	ad901671c5	Add $anyconst/$anyseq support to btor back-end	2017-12-15 00:40:24 +01:00
Clifford Wolf	162c29bd6b	Merge branch 'master' into btor-ng	2017-12-14 03:13:47 +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	a48ec49017	Merge branch 'master' into btor-ng	2017-12-14 02:17:01 +01:00
Clifford Wolf	2625da6440	Add smt2 back-end support for async write memories	2017-12-14 02:07:10 +01:00
Clifford Wolf	546de7fa4f	Add "write_btor -s" mode	2017-12-13 00:15:44 +01:00
Clifford Wolf	0881bbf2e7	Add state initval handling to btor back-end	2017-12-12 23:44:08 +01:00
Clifford Wolf	f697282246	Add btor back-end support for 'x' constants	2017-12-12 21:48:55 +01:00
Clifford Wolf	82d1fd77de	Add btor $shift/$shiftx support	2017-12-11 14:24:19 +01:00
Clifford Wolf	cc119b5232	Fix btor back-end shift handling	2017-12-10 08:40:11 +01:00
Clifford Wolf	133a0f4978	Add support for $pmux in btor back-end	2017-12-10 08:11:08 +01:00
Clifford Wolf	83cf736309	Add support for more cell types to btor back-end	2017-12-10 07:16:47 +01:00
Clifford Wolf	63343aeaaa	Fix btor concat	2017-12-09 05:58:14 +01:00
Clifford Wolf	da91b31bb2	Fixed "yosys-smtbmc -g" handling of no solution	2017-11-27 19:43:36 +01:00
Clifford Wolf	b981e5aa69	Fixed "yosys-smtbmc -g" handling of no solution	2017-11-27 17:42:32 +01:00
Clifford Wolf	e3a51b3e87	Bugfixes in new BTOR back-end	2017-11-24 18:13:41 +01:00
Clifford Wolf	60d1129506	Progress in new BTOR back-end	2017-11-23 23:44:39 +01:00
Clifford Wolf	b3d6b277ea	Progress in new BTOR back-end	2017-11-23 18:50:10 +01:00
Clifford Wolf	cc2495d48d	Progress in new BTOR back-end	2017-11-23 18:14:53 +01:00
Clifford Wolf	e41dcaa759	Progress with new BTOR backend	2017-11-23 08:28:29 +01:00
Clifford Wolf	6ee305553a	Add skeleton for new BTOR back-end	2017-11-23 06:38:57 +01:00
Clifford Wolf	eceacdb9a3	Remove old BTOR back-end	2017-11-23 04:28:51 +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	adf1754729	Add $shiftx support to verilog front-end	2017-10-07 13:40:54 +02:00
Clifford Wolf	65f91e5120	Rename "write_verilog -nobasenradix" to "write_verilog -decimal"	2017-10-03 17:31:21 +02:00
dh73	e480847753	Fixed wrong declaration in Verilog backend	2017-10-01 11:11:32 -05:00
dh73	cbaba62401	Adding Cyclone IV (E, GX), Arria 10, Cyclone V and LPM functions (ALTPLL and M9K); M9K is not finished yet. Achronix Speedster also in this commit. Both Arria10 and Speedster-i are still experimental due complexity, but you can experiment around those devices right now	2017-10-01 11:04:17 -05: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	4a8c131fa7	Fix the fixed handling of x-bits in EDIF back-end	2017-07-11 17:45:29 +02:00
Clifford Wolf	479be3cec7	Fix handling of x-bits in EDIF back-end	2017-07-11 17:38:19 +02:00
Clifford Wolf	9557fd2a36	Add attributes and parameter support to JSON front-end	2017-07-10 13:17:38 +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	5442554e6f	Fix generation of multiple outputs for same AIG node in write_aiger	2017-07-05 14:23:54 +02:00
Clifford Wolf	37af6294bd	Add write_table command	2017-07-05 12:13:53 +02:00
Clifford Wolf	3e0948e16f	Remove unneeded delays in smtbmc vlogtb	2017-07-03 15:37:17 +02:00
Clifford Wolf	287831dca3	Include output ports with constant driver in AIGER output	2017-07-03 14:53: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