1164 commits

Author	SHA1	Message	Date
Clifford Wolf	a6ca28276e	Add write_aiger $anyseq support	2017-03-02 16:39:48 +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	c7d1286728	Improve "write_edif" help message	2017-02-25 16:35:53 +01:00
Clifford Wolf	dfddf391f9	Move EdifNames out of double-private namespace	2017-02-25 16:29:27 +01:00
Clifford Wolf	8c61ecdd6e	Clean up edif code, swap bit indexing of "upto" ports	2017-02-25 16:28:34 +01:00
Clifford Wolf	b76c89a5dd	Merge branch 'master' of https://github.com/klammerj/yosys into klammerj-master	2017-02-25 15:59:02 +01:00
Clifford Wolf	dac0842d61	Add $live and $fair support to AIGER back-end.	2017-02-25 13:07:15 +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
Johann Klammer	6d7a77dbf6	Did as you requested, /but/... ... Now the nets are wired in reverse again because the netlister still uses zero-based indices.	2017-02-24 13:18:49 +01:00
Johann Klammer	06df86aae3	add options for edif flavors ... *to force renames on wide ports *to choose array delimiters *to choose up or downwards indices	2017-02-23 19:42:37 +01:00
Clifford Wolf	242c5f01de	Add "yosys-smtbmc -S <opt>"	2017-02-19 22:51:29 +01:00
Clifford Wolf	4e80ce97a8	Add warning about x/z bits left unconnected in EDIF output	2017-02-14 12:49:35 +01:00
Adam Izraelevitz	794cec0016	More progress on Firrtl backend. ... Chisel -> Firrtl -> Verilog -> Firrtl -> Verilog is successful for a simple rocket-chip design.	2017-02-13 11:17:53 -08: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	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