aboutsummaryrefslogtreecommitdiffstats
Commit message (Collapse)AuthorAgeFilesLines
* Removed $timescale from "sat" command VCD writerClifford Wolf2018-03-291-1/+0
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Set stack size to at least 128 MB (large stack needed for parsing huge ↵Clifford Wolf2018-03-271-0/+13
| | | | | | expressions) Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix tests/simple/specify.vClifford Wolf2018-03-271-2/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* First draft of Verilog parser support for specify blocks and parameters.Udi Finkelstein2018-03-273-2/+201
| | | | | 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
* Merge pull request #515 from edcote/patch-1Clifford Wolf2018-03-271-3/+5
|\ | | | | Rename rename to renames
| * Rename rename to renamesEdmond Cote2018-03-201-3/+5
| | | | | | Create TCL alias for rename command. Using renames. Following the same convention as proc -> procs.
* | Chenged "extensions_map" to "extensions_list" in hierarchy.ccClifford Wolf2018-03-271-2/+2
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Merge pull request #518 from xerpi/masterClifford Wolf2018-03-271-15/+13
|\ \ | | | | | | passes/hierarchy: Reduce code duplication in expand_module
| * | passes/hierarchy: Reduce code duplication in expand_moduleSergi Granell2018-03-271-15/+13
|/ / | | | | | | | | | | This also makes it easier to add new file extensions support. Signed-off-by: Sergi Granell <xerpi.g.12@gmail.com>
* | Add $mem support to SMT2 clock taggingClifford Wolf2018-03-271-0/+18
| | | | | | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* | Fix build for new ABC location on github, also update ABC to a2d59beClifford Wolf2018-03-271-6/+6
| |
* | Add .sv support to "hierarchy -libdir"Clifford Wolf2018-03-261-0/+6
| |
* | Fix handling of unclocked immediate assertions in Verific front-endClifford Wolf2018-03-263-17/+42
|/ | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve yosys-smtbmc log output and error handlingClifford Wolf2018-03-171-5/+14
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve handling of invalid check-sat result in smtio.pyClifford Wolf2018-03-171-1/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Update todo for more features to verificsva.ccClifford Wolf2018-03-161-3/+3
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Update todo for more features to verificsva.ccClifford Wolf2018-03-161-0/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add todo for more features to verificsva.ccClifford Wolf2018-03-161-8/+45
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve import of memories via VerificClifford Wolf2018-03-151-16/+23
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix handling of SV compilation units in Verific front-endClifford Wolf2018-03-141-28/+25
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "expose -input"Clifford Wolf2018-03-121-8/+43
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "setundef -undef"Clifford Wolf2018-03-121-0/+11
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Squelch trailing whitespace, including meta-whitespaceLarry Doolittle2018-03-114-16/+16
|
* Harmonize uses of _WIN32 macroLarry Doolittle2018-03-111-1/+1
|
* Fix SVA handling of NON_CONSECUTIVE_REPEAT and GOTO_REPEATClifford Wolf2018-03-101-15/+72
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix variable name typo in verificsva.ccClifford Wolf2018-03-101-2/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for trivial SVA sequences and propertiesClifford Wolf2018-03-101-12/+102
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix handling of src attributes in flattenClifford Wolf2018-03-101-7/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Remove debug prints from yosys-smtbmc VCD writerClifford Wolf2018-03-081-2/+0
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Use Verific hier_tree component for elaborationClifford Wolf2018-03-082-1/+55
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Check results of (check-sat) in yosys-smtbmcClifford Wolf2018-03-071-0/+2
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix Verific handling of "assert property (..);" in always blockClifford Wolf2018-03-073-14/+60
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add "verific -import -V"Clifford Wolf2018-03-072-6/+18
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Set Verific db_preserve_user_nets flagClifford Wolf2018-03-071-0/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add Xilinx RAM64X1D and RAM128X1D simulation modelsClifford Wolf2018-03-074-23/+30
|
* Add "memory_nordff" passClifford Wolf2018-03-062-0/+112
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Update comment about supported SVA in verificsva.ccClifford Wolf2018-03-061-51/+8
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT supportClifford Wolf2018-03-061-20/+41
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add SVA first_match() supportClifford Wolf2018-03-061-0/+16
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add SVA within supportClifford Wolf2018-03-061-2/+18
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add support for SVA sequence intersectClifford Wolf2018-03-061-36/+251
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add get_fsm_accept_reject for parsing SVA propertiesClifford Wolf2018-03-061-73/+86
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Simplified SVA "until" handlingClifford Wolf2018-03-061-25/+16
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Imporove yosys-smtbmc error handling, Improve VCD outputClifford Wolf2018-03-052-23/+49
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix connwrappers help messageClifford Wolf2018-03-041-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve handling of warning messagesClifford Wolf2018-03-043-12/+42
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Update copyright headerClifford Wolf2018-03-041-1/+1
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Improve SMT2 encoding of $reduce_{and,or,bool}Clifford Wolf2018-03-041-1/+9
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Fix a hangup in yosys-smtbmc error handlingClifford Wolf2018-03-041-3/+5
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>
* Add proper SVA seq.triggered supportClifford Wolf2018-03-043-37/+102
| | | | Signed-off-by: Clifford Wolf <clifford@clifford.at>