3815 commits

This branch

This branch

All branches

Author	SHA1	Message	Date
Clifford Wolf	491c352da7	Add .sv support to "hierarchy -libdir"	2018-03-26 21:19:00 +02:00
Clifford Wolf	315d5e32bf	Fix handling of unclocked immediate assertions in Verific front-end ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-26 13:04:10 +02:00
Edmond Cote	64ea55056a	Rename rename to renames ... Create TCL alias for rename command. Using renames. Following the same convention as proc -> procs.	2018-03-20 15:50:50 -07:00
Clifford Wolf	3f00702475	Improve yosys-smtbmc log output and error handling ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-17 18:06:17 +01:00
Clifford Wolf	4d4e3a8ca6	Improve handling of invalid check-sat result in smtio.py ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-17 12:17:53 +01:00
Clifford Wolf	e7862d4f64	Update todo for more features to verificsva.cc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-16 15:48:48 +01:00
Clifford Wolf	38596ce68f	Update todo for more features to verificsva.cc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-16 12:16:52 +01:00
Clifford Wolf	462e9f7bd4	Add todo for more features to verificsva.cc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-16 12:15:36 +01:00
Clifford Wolf	7cf9d88028	Improve import of memories via Verific ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-15 18:20:37 +01:00
Clifford Wolf	bf402a806a	Fix handling of SV compilation units in Verific front-end ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-14 20:22:11 +01:00
Clifford Wolf	08225f49a4	Add "expose -input" ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-12 13:52:52 +01:00
Clifford Wolf	83ffb23739	Add "setundef -undef" ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-12 13:52:35 +01:00
Larry Doolittle	efaef82f75	Squelch trailing whitespace, including meta-whitespace	2018-03-11 16:03:41 +01:00
Larry Doolittle	82fecc98c0	Harmonize uses of _WIN32 macro	2018-03-11 16:01:30 +01:00
Clifford Wolf	307c16a309	Fix SVA handling of NON_CONSECUTIVE_REPEAT and GOTO_REPEAT ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-10 16:24:01 +01:00
Clifford Wolf	ce37b6d730	Fix variable name typo in verificsva.cc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-10 14:33:42 +01:00
Clifford Wolf	da216937b1	Add support for trivial SVA sequences and properties ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-10 14:32:01 +01:00
Clifford Wolf	a74f805ba0	Fix handling of src attributes in flatten ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-10 13:55:30 +01:00
Clifford Wolf	3545c0fffb	Remove debug prints from yosys-smtbmc VCD writer ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-08 16:24:35 +01:00
Clifford Wolf	a15208f301	Use Verific hier_tree component for elaboration ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-08 13:26:33 +01:00
Clifford Wolf	8b604004da	Check results of (check-sat) in yosys-smtbmc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-07 22:54:19 +01:00
Clifford Wolf	a4bbfd2d15	Fix Verific handling of "assert property (..);" in always block ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-07 20:06:02 +01:00
Clifford Wolf	92d5f4db6f	Add "verific -import -V" ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-07 19:40:34 +01:00
Clifford Wolf	252627fc54	Set Verific db_preserve_user_nets flag ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-07 18:08:03 +01:00
Clifford Wolf	6991c132b5	Add Xilinx RAM64X1D and RAM128X1D simulation models	2018-03-07 17:31:48 +01:00
Clifford Wolf	73c01dca65	Add "memory_nordff" pass ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-06 23:31:51 +01:00
Clifford Wolf	dcc4a18d5a	Update comment about supported SVA in verificsva.cc ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-06 15:47:33 +01:00
Clifford Wolf	03b49654b1	Add SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT support ... Signed-off-by: Clifford Wolf <clifford@clifford.at>	2018-03-06 15:39:46 +01:00
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