1503 commits

Author	SHA1	Message	Date
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
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	c365e33fd7	Fix AIGER back-end for multiple symbols per input/latch/output/property	2017-05-30 19:09:11 +02:00
Clifford Wolf	9ed4c9d710	Improve write_aiger handling of unconnected nets and constants	2017-05-28 11:31:35 +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	2122ae69b3	Add workaround for CBMC bug to SimpleC back-end	2017-05-17 21:07:54 +02:00
Clifford Wolf	05cdd58c8d	Add $_ANDNOT_ and $_ORNOT_ gates	2017-05-17 09:08:29 +02:00
Clifford Wolf	9f4fbc5e74	Add <modname>_init() function generator to simpleC back-end	2017-05-16 19:34:07 +02:00
Clifford Wolf	35be567605	Improve simplec back-end	2017-05-16 08:50:23 +02:00
Clifford Wolf	8d3c706459	Improve simplec back-end	2017-05-15 13:21:59 +02:00
Clifford Wolf	9c397ea78b	Improve simplec back-end	2017-05-14 13:14:49 +02:00
Clifford Wolf	628daab277	Improve simplec back-end	2017-05-13 18:47:31 +02:00
Clifford Wolf	ef7594ce3d	Improve simplec back-end	2017-05-12 22:39:16 +02:00
Clifford Wolf	7931e1ebb4	Added support for more gate types to simplec back-end	2017-05-12 17:42:31 +02:00
Clifford Wolf	bd4ed19887	Add first draft of simple C back-end	2017-05-12 14:13:33 +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	0ac72e759d	Add generation of logic cells to EDIF back-end runtest.py	2017-03-19 14:57:40 +01:00
Clifford Wolf	850f8299a9	Fix EDIF: portRef member 0 is always the MSB bit	2017-03-19 14:53:28 +01:00
Clifford Wolf	1390e9a0a7	Add simple EDIF test case generator and checker	2017-03-18 15:00:03 +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	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