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 |
Clifford Wolf
|
b6fbeb0969
|
Add handling of verific OPER_REDUCE_NOR
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-26 15:26:01 +01:00 |
Clifford Wolf
|
2aeb4d4e12
|
Add handling of verific OPER_SELECTOR and OPER_WIDE_SELECTOR
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-26 15:20:27 +01:00 |
Clifford Wolf
|
9cd9f5fc78
|
Add handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUX
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-26 15:02:03 +01:00 |
Clifford Wolf
|
d1cb5150aa
|
Add "SVA syntax cheat sheet" comment to verificsva.cc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-26 14:31:58 +01:00 |
Clifford Wolf
|
d31584c649
|
Add $dlatchsr support to clk2fflogic
|
2018-02-26 12:20:28 +01:00 |
Clifford Wolf
|
675dd5347a
|
Small fixes and improvements in $allconst/$allseq handling
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-26 11:58:44 +01:00 |
Clifford Wolf
|
fba499b866
|
Fix opt_rmdff handling of $dlatchsr
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-26 11:46:05 +01:00 |
Clifford Wolf
|
0d636964b8
|
Merge branch 'forall'
|
2018-02-23 19:37:00 +01:00 |
Clifford Wolf
|
b13e6bd375
|
Add smtbmc support for exist-forall problems
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-23 19:33:30 +01:00 |
Clifford Wolf
|
eb67a7532b
|
Add $allconst and $allseq cell types
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-23 13:14:47 +01:00 |
Clifford Wolf
|
2521ed305e
|
Add Verific SVA support for ranges in repetition operator
|
2018-02-22 12:37:30 +01:00 |
Clifford Wolf
|
6d12c83d36
|
Add support for SVA throughout via Verific
|
2018-02-21 13:09:47 +01:00 |
Clifford Wolf
|
17583b6a21
|
Add support for mockup clock signals in yosys-smtbmc vcd output
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-20 17:45:22 +01:00 |
Clifford Wolf
|
f2cfe73d74
|
Merge pull request #507 from cr1901/msys2
Improve msys2 flags for building abc.
|
2018-02-19 19:32:11 +01:00 |
William D. Jones
|
b0b08da5cb
|
Improve msys2 flags for building abc.
|
2018-02-19 12:54:34 -05:00 |
Clifford Wolf
|
5c6247dfa6
|
Add support for SVA sequence concatenation ranges via verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-18 16:35:06 +01:00 |
Clifford Wolf
|
9d963cd29c
|
Add support for SVA until statements via Verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-18 14:57:52 +01:00 |
Clifford Wolf
|
5fa2aa2741
|
Move Verific SVA importer to extra C++ source file
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-18 13:52:49 +01:00 |
Clifford Wolf
|
c4bf34f6ce
|
Merge Verific SVA preprocessor and SVA importer
|
2018-02-18 13:28:08 +01:00 |
Clifford Wolf
|
68a829dbcd
|
Merge branch 'master' of github.com:cliffordwolf/yosys
|
2018-02-16 14:22:11 +01:00 |
Clifford Wolf
|
2c95dfcb5b
|
Improve handling of "bus" pins in liberty front-end (some files use bus.pin.direction)
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-15 17:36:08 +01:00 |
Clifford Wolf
|
bc8ab3ab44
|
Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF
|
2018-02-15 15:26:37 +01:00 |
Clifford Wolf
|
c1abd3b02c
|
Fixed yosys-config for binary distributions with Verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-13 15:22:50 +01:00 |
Clifford Wolf
|
717abc93a8
|
Recognize stand-alone obj pattern even when it contains a slash
|
2018-02-13 14:55:24 +01:00 |
Clifford Wolf
|
c9672e2e2e
|
Fix handling of zero-length cell connections in SMT2 back-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-08 19:12:12 +01:00 |
Clifford Wolf
|
0659d9eac7
|
Merge branch 'master' of github.com:cliffordwolf/yosys
|
2018-02-03 15:05:08 +01:00 |
Clifford Wolf
|
82c436587c
|
Do not create deep backtraces unless in ENABLE_DEBUG mode
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-03 15:04:39 +01:00 |
Clifford Wolf
|
6fedcbce86
|
Merge pull request #488 from azonenberg/for_clifford
coolrunner2: Move LOC attributes onto the IO cells
|
2018-02-03 14:45:23 +01:00 |
Clifford Wolf
|
e4f0218907
|
Fixed gcc 7.2 "statement will never be executed" warning
|
2018-02-03 14:31:47 +01:00 |
Clifford Wolf
|
6c00e064e2
|
Fix single-bit $stable handling in verific front-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-01 12:51:49 +01:00 |
Clifford Wolf
|
9af40faa0b
|
Add Verific attribute handling for assert/assume/cover/live/fair cells
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-01-31 19:06:51 +01:00 |
Clifford Wolf
|
e97f10b142
|
Fix smtio.py for large SMT2 S-expressions
|
2018-01-29 12:34:28 +01:00 |
Clifford Wolf
|
675f53abbb
|
Fix permissions on verific vdb files
|
2018-01-28 18:52:01 +01:00 |
Clifford Wolf
|
1d8161b432
|
Fixed handling of synchronous and asynchronous assertion/assumption/cover in verific bindings
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-01-23 17:42:40 +01:00 |
Clifford Wolf
|
318be8651c
|
Use "strip -S" instead of "strip -d" for Mac OS X compatibility
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-01-19 23:56:23 +01:00 |
Clifford Wolf
|
9337e4999d
|
Improve log messages in equiv_make
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-01-19 16:20:40 +01:00 |
Clifford Wolf
|
54aeca0983
|
Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output
|
2018-01-18 14:25:22 +01:00 |
Robert Ou
|
2abcd98527
|
coolrunner2: Move LOC attributes onto the IO cells
|
2018-01-17 16:17:32 -08:00 |
Clifford Wolf
|
57e02b6629
|
Strip debug symbols from binaries on install
|
2018-01-17 14:14:10 +01:00 |
Clifford Wolf
|
9ac560f5d3
|
Add "dffinit -highlow" and fix synth_intel
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-01-09 18:42:19 +01:00 |