334 commits

Author	SHA1	Message	Date
Clifford Wolf	2198948398	Improved write_json help message	2016-12-29 12:13:29 +01:00
Clifford Wolf	a61c88f122	Added $anyconst support to AIGER back-end	2016-12-11 13:48:18 +01:00
Clifford Wolf	a44cc7a3d1	Added $assert/$assume support to AIGER back-end	2016-12-03 13:20:29 +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	5fa1fa1e6f	Added "write_aiger -zinit -symbols -vmap"	2016-12-01 11:04:36 +01:00
Clifford Wolf	c1f762ca56	Added "write_aiger" command	2016-11-30 21:30:24 +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	5c2c78e2dd	Added wire start_offset and upto handling BLIF back-end	2016-11-23 13:54:33 +01:00
Clifford Wolf	f257ccf22e	Added "yosys-smtbmc --append"	2016-11-22 21:21:13 +01:00
Adam Izraelevitz	f77dc3bacc	Bugfix: include assign to write-mask	2016-11-18 11:49:26 -08:00
Clifford Wolf	e01382739d	More progress in FIRRTL back-end	2016-11-18 02:41:29 +01:00
Clifford Wolf	c051115e03	Progress in FIRRTL back-end	2016-11-18 00:32:35 +01:00
Clifford Wolf	57966a619f	Added first draft of FIRRTL back-end	2016-11-17 23:36:47 +01:00
Clifford Wolf	ce132cf652	Cleanups and fixed in write_verilog regarding reg init	2016-11-16 12:00:39 +01:00
Clifford Wolf	3db2ac4e00	Added hex constant support to write_verilog	2016-11-03 12:13:23 +01:00
Clifford Wolf	caa2fc62ef	Adde "write_verilog -renameprefix -v"	2016-11-01 11:30:27 +01:00
Clifford Wolf	aa72262330	Added avail params to ilang format, check module params in 'hierarchy -check'	2016-10-22 11:05:49 +02:00
Clifford Wolf	281a977b39	Ignore L_pi nets in "yosys-smtbmc --cex"	2016-10-18 10:54:53 +02:00
Clifford Wolf	9e980a2bb0	Use init value "2" for all uninitialized FFs in BLIF back-end	2016-10-18 10:54:04 +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	53655d173b	Added $global_clock verilog syntax support for creating $ff cells	2016-10-14 12:33:56 +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
Clifford Wolf	4eb0d6fc0e	Added "yosys-smtbmc -s abc"	2016-10-01 13:54:21 +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	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	14bfd3c5c1	yosys-smtbmc meminit support	2016-09-08 11:16:12 +02: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	97b449fe55	yosys-smtbmc: flush stdout after each log msg	2016-09-06 01:40:31 +02:00
Clifford Wolf	372d672c2a	Minor bugfix in write_smt2	2016-09-04 16:32:47 +02:00
Clifford Wolf	fa5565b606	Added boolector support to yosys-smtbmc	2016-09-03 14:26:00 +02:00
Clifford Wolf	948aac9e1e	Don't re-create hex_dict for each value	2016-09-02 13:46:56 +02:00