Commit Graph

3777 Commits

Author SHA1 Message Date
Clifford Wolf dd5fab69c1 Add smtio status msgs when --progress is inactive
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 21:59:30 +02:00
Clifford Wolf a48c7e5abf Bugfix in smtio.py VCD file generator
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 12:45:31 +02:00
Clifford Wolf 665eec3d53 Removed $timescale from "sat" command VCD writer
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-29 12:38:41 +02:00
Clifford Wolf 0acea3548b Set stack size to at least 128 MB (large stack needed for parsing huge expressions)
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-27 15:04:10 +02:00
Clifford Wolf 5e49ee5c2d Fix tests/simple/specify.v
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-27 14:34:00 +02:00
Udi Finkelstein 6378e2cd46 First draft of Verilog parser support for specify blocks and parameters.
The only functionality of this code at the moment is to accept correct specify syntax and ignore it.
No part of the specify block is added to the AST
2018-03-27 14:34:00 +02:00
Clifford Wolf f3eaa0ffa5
Merge pull request #515 from edcote/patch-1
Rename rename to renames
2018-03-27 14:14:51 +02:00
Clifford Wolf ee3c12d6d9 Chenged "extensions_map" to "extensions_list" in hierarchy.cc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-27 14:12:57 +02:00
Clifford Wolf c652774ca2
Merge pull request #518 from xerpi/master
passes/hierarchy: Reduce code duplication in expand_module
2018-03-27 14:10:39 +02:00
Sergi Granell f93f8aaa11 passes/hierarchy: Reduce code duplication in expand_module
This also makes it easier to add new file extensions support.

Signed-off-by: Sergi Granell <xerpi.g.12@gmail.com>
2018-03-27 09:35:20 +02:00
Clifford Wolf 77bd645c35 Add $mem support to SMT2 clock tagging
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-27 02:11:20 +02:00
Clifford Wolf 6f681c4f82 Fix build for new ABC location on github, also update ABC to a2d59be 2018-03-27 00:39:01 +02:00
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