Udi Finkelstein
80d9d15f1c
reg_wire_error test needs the -sv flag so it is run via a script so it had to be moved out of the tests/simple dir that only runs Verilog files
2018-06-05 18:00:06 +03: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
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