5937 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Clifford Wolf	7bb83ae9f2	Add SVA first_match() support ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-06 15:06:35 +01:00
Clifford Wolf	78f2cca2d9	Add SVA within support ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-06 14:41:27 +01:00
Clifford Wolf	5555292ce2	Add support for SVA sequence intersect ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-06 14:26:57 +01:00
Clifford Wolf	d86e875f0f	Add get_fsm_accept_reject for parsing SVA properties ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-06 11:50:38 +01:00
Clifford Wolf	588ce0e34a	Simplified SVA "until" handling ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-06 01:51:42 +01:00
Clifford Wolf	cedbc35f4b	Imporove yosys-smtbmc error handling, Improve VCD output ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-05 12:17:22 +01:00
Clifford Wolf	61a9e2eeb3	Fix connwrappers help message ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 22:54:34 +01:00
Clifford Wolf	e5534a080e	Improve handling of warning messages ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 22:35:59 +01:00
Clifford Wolf	2935e8ea41	Update copyright header ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 21:31:10 +01:00
Clifford Wolf	8b7602e660	Improve SMT2 encoding of $reduce_{and,or,bool} ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 21:22:20 +01:00
Clifford Wolf	45a6fce92c	Fix a hangup in yosys-smtbmc error handling ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 21:13:30 +01:00
Clifford Wolf	480e8e676a	Add proper SVA seq.triggered support ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 19:29:26 +01:00
Clifford Wolf	27dd500d31	Add "synth -noshare" ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 17:13:45 +01:00
Clifford Wolf	8dcf3d0c76	Add Verific SVA support for "seq and seq" expressions ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 15:08:21 +01:00
Clifford Wolf	9ab2498c55	Refactor Verific SVA importer property parser ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 14:29:48 +01:00
Clifford Wolf	261cf706f4	Add VerificClocking class and refactor Verific DFF handling ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-04 13:48:53 +01:00
Clifford Wolf	ae4e204c76	Improved error handling in yosys-smtbmc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-03 20:00:07 +01:00
Clifford Wolf	707ddb77bc	Add SVA support for sequence OR ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-03 16:34:28 +01:00
Clifford Wolf	a44e1edaa3	Terminate running SMT solver when smtbmc is terminated ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-03 14:50:40 +01:00
Clifford Wolf	3ced2cca6e	Fix smtbmc smtc/aiw parser for wire names containing [] ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-03 14:15:49 +01:00
Clifford Wolf	cabc3c59e0	Fix handling of SVA "until seq.triggered" properties ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-02 18:17:10 +01:00
Clifford Wolf	ab791e61b3	Update SVA cheat sheet in verificsva.cc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-02 16:05:56 +01:00
Clifford Wolf	4e5f1f59d6	Fix in Verific SVA importer handling of until_with ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-01 19:37:36 +01:00
Clifford Wolf	90ae426078	Mangle names with square brackets in VCD files to work around issues in gtkwave ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-01 14:15:27 +01:00
Clifford Wolf	9a2a8cd97b	Fixes and improvements in Verific SVA importer ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-01 11:40:43 +01:00
Clifford Wolf	3c49e3c5b3	Add $rose/$fell support to Verific bindings ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-01 10:12:15 +01:00
Clifford Wolf	3df0d04a7b	Merge branch 'verificsva-ng'	2018-02-28 15:32:53 +01:00
Clifford Wolf	5ac3ee858a	Add support for PRIM_SVA_UNTIL to new SVA importer ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-28 15:32:17 +01:00
Clifford Wolf	8a1d6ccf0c	Add DFSM generator to verific SVA importer ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-28 15:05:33 +01:00
Clifford Wolf	15902d495f	Continue refactoring of Verific SVA importer code ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-28 11:45:04 +01:00
Clifford Wolf	25e33d7ab8	Major redesign of Verific SVA importer ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-27 20:33:15 +01:00
Clifford Wolf	6f26695d9b	Add -lz for verific builds ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-02-27 12:15:42 +01:00
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