Commit Graph

4467 Commits

Author SHA1 Message Date
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
Udi Finkelstein 2b9c75f8e3 This PR should be the base for discussion, do not merge it yet!
It correctly detects reg/wire mix and incorrect use on blocking,nonblocking assignments within blocks and assign statements.

What it DOES'T do:
Detect registers connected to output ports of instances.

Where it FAILS:
memorty nonblocking assignments causes spurious (I assume??) errors on yosys-generated "_ADDR", "_DATA", "EN" signals.

You can test it with tests/simple/reg_wire_error.v (look inside for the comments to enable/disable specific lines)
2018-03-11 23:09:34 +02: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