4005 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Clifford Wolf	b6fbeb0969	Add handling of verific OPER_REDUCE_NOR ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-26 15:26:01 +01:00
Clifford Wolf	2aeb4d4e12	Add handling of verific OPER_SELECTOR and OPER_WIDE_SELECTOR ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-26 15:20:27 +01:00
Clifford Wolf	9cd9f5fc78	Add handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUX ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-26 15:02:03 +01:00
Clifford Wolf	d1cb5150aa	Add "SVA syntax cheat sheet" comment to verificsva.cc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-26 14:31:58 +01:00
Clifford Wolf	d31584c649	Add $dlatchsr support to clk2fflogic	2018-02-26 12:20:28 +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	fba499b866	Fix opt_rmdff handling of $dlatchsr ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-26 11:46:05 +01:00
Clifford Wolf	0d636964b8	Merge branch 'forall'	2018-02-23 19:37:00 +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	eb67a7532b	Add $allconst and $allseq cell types ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-23 13:14:47 +01:00
Clifford Wolf	2521ed305e	Add Verific SVA support for ranges in repetition operator	2018-02-22 12:37:30 +01:00
Clifford Wolf	6d12c83d36	Add support for SVA throughout via Verific	2018-02-21 13:09:47 +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	f2cfe73d74	Merge pull request #507 from cr1901/msys2 ... Improve msys2 flags for building abc.	2018-02-19 19:32:11 +01:00
William D. Jones	b0b08da5cb	Improve msys2 flags for building abc.	2018-02-19 12:54:34 -05:00
Clifford Wolf	5c6247dfa6	Add support for SVA sequence concatenation ranges via verific ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-18 16:35:06 +01:00
Clifford Wolf	9d963cd29c	Add support for SVA until statements via Verific ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-18 14:57:52 +01:00
Clifford Wolf	5fa2aa2741	Move Verific SVA importer to extra C++ source file ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-18 13:52:49 +01:00
Clifford Wolf	c4bf34f6ce	Merge Verific SVA preprocessor and SVA importer	2018-02-18 13:28:08 +01:00
Clifford Wolf	68a829dbcd	Merge branch 'master' of github.com:cliffordwolf/yosys	2018-02-16 14:22:11 +01:00
Clifford Wolf	2c95dfcb5b	Improve handling of "bus" pins in liberty front-end (some files use bus.pin.direction) ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-15 17:36:08 +01:00
Clifford Wolf	bc8ab3ab44	Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF	2018-02-15 15:26:37 +01:00
Clifford Wolf	c1abd3b02c	Fixed yosys-config for binary distributions with Verific ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-13 15:22:50 +01:00
Clifford Wolf	717abc93a8	Recognize stand-alone obj pattern even when it contains a slash	2018-02-13 14:55:24 +01:00
Clifford Wolf	c9672e2e2e	Fix handling of zero-length cell connections in SMT2 back-end ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-08 19:12:12 +01:00
Clifford Wolf	0659d9eac7	Merge branch 'master' of github.com:cliffordwolf/yosys	2018-02-03 15:05:08 +01:00
Clifford Wolf	82c436587c	Do not create deep backtraces unless in ENABLE_DEBUG mode ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-03 15:04:39 +01:00
Clifford Wolf	6fedcbce86	Merge pull request #488 from azonenberg/for_clifford ... coolrunner2: Move LOC attributes onto the IO cells	2018-02-03 14:45:23 +01:00
Clifford Wolf	e4f0218907	Fixed gcc 7.2 "statement will never be executed" warning	2018-02-03 14:31:47 +01:00
Clifford Wolf	6c00e064e2	Fix single-bit $stable handling in verific front-end ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-01 12:51:49 +01:00
Clifford Wolf	9af40faa0b	Add Verific attribute handling for assert/assume/cover/live/fair cells ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-01-31 19:06:51 +01:00
Clifford Wolf	e97f10b142	Fix smtio.py for large SMT2 S-expressions	2018-01-29 12:34:28 +01:00
Clifford Wolf	675f53abbb	Fix permissions on verific vdb files	2018-01-28 18:52:01 +01:00
Clifford Wolf	1d8161b432	Fixed handling of synchronous and asynchronous assertion/assumption/cover in verific bindings ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-01-23 17:42:40 +01:00
Clifford Wolf	318be8651c	Use "strip -S" instead of "strip -d" for Mac OS X compatibility ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-01-19 23:56:23 +01:00
Clifford Wolf	9337e4999d	Improve log messages in equiv_make ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-01-19 16:20:40 +01:00
Clifford Wolf	54aeca0983	Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output	2018-01-18 14:25:22 +01:00
Robert Ou	2abcd98527	coolrunner2: Move LOC attributes onto the IO cells	2018-01-17 16:17:32 -08:00
Clifford Wolf	57e02b6629	Strip debug symbols from binaries on install	2018-01-17 14:14:10 +01:00
Clifford Wolf	9ac560f5d3	Add "dffinit -highlow" and fix synth_intel ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-01-09 18:42:19 +01:00
Clifford Wolf	a96c775a73	Add support for "yosys -E" ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-01-07 16:36:13 +01:00
Clifford Wolf	446ccf1f05	Bugfix in hierarchy blackbox module port width handling	2018-01-07 16:35:22 +01:00
Clifford Wolf	b557989576	Update ABC to hg rev 6e3c24b3308a ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-01-07 13:47:59 +01:00
Clifford Wolf	26c4323d48	Merge pull request #479 from Fatsie/latch_without_data ... Some standard cell libraries include a latch with only set/reset.	2018-01-05 23:00:28 +01:00
Clifford Wolf	c80315cea4	Bugfix in hierarchy handling of blackbox module ports ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-01-05 13:28:45 +01:00
Clifford Wolf	fefb652d56	Merge pull request #480 from Fatsie/liberty_value_expression ... Value of properties can be expression.	2018-01-04 13:30:00 +01:00
Clifford Wolf	2d140a44eb	Temporarily derive blackbox modules in hierarchy to evaluate port widths ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-01-04 13:23:29 +01:00
Staf Verhaegen	92eb841f0a	Value of properties can be expression. ... Example found in the 2007.03 Liberty Reference Manual that was also found in the wild: input_voltage(CMOS) { vil : 0.3 * VDD ; vih : 0.7 * VDD ; vimin : -0.5 ; vimax : VDD + 0.5 ; } Current implementation just parses the expression but no interpretation is done.	2018-01-03 21:37:17 +00:00
Staf Verhaegen	5126c6f22b	Some standard cell libraries include a latch with only set/reset.	2018-01-03 21:36:02 +00:00
Clifford Wolf	9804ebedbf	Add "no driver for signal bit" error msg to btor back-end	2017-12-24 17:30:36 +01:00