Clifford Wolf
6af0d03fae
Add Verific SVA support for "always" properties
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-22 15:52:21 +01:00
Clifford Wolf
55bda2b2c6
Correctly treat empty modules as blackboxes in Verific
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-20 12:56:31 +01:00
Clifford Wolf
f6ff311a1d
Do not rename VHDL entities to "entity(impl)" when they are top modules
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-11-20 12:54:10 +01:00
Eddie Hung
e2819ce31c
Oops
2019-11-19 13:25:38 -08:00
Eddie Hung
84711f0e8c
Print help message for verific pass
2019-11-19 13:24:48 -08:00
Clifford Wolf
84982b3083
Improve naming scheme for (VHDL) modules imported from Verific
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-24 12:13:50 +02:00
Clifford Wolf
d49c6b2cba
Add "verific -L"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-24 09:14:03 +02:00
Clifford Wolf
4033ff8c2e
Fix handling of "restrict" in Verific front-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-10-21 12:39:28 +02:00
Clifford Wolf
27d59dc055
Fix erroneous ifndef-NDEBUG in verific.cc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-08-17 14:49:55 +02:00
Clifford Wolf
0c5db07cd6
Fix various NDEBUG compiler warnings, closes #1255
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-08-13 13:29:03 +02:00
Clifford Wolf
f54bf1631f
Merge pull request #1258 from YosysHQ/eddie/cleanup
...
Cleanup a few barnacles across codebase
2019-08-10 09:52:14 +02:00
Eddie Hung
6d77236f38
substr() -> compare()
2019-08-07 12:20:08 -07:00
Eddie Hung
48d0f99406
stoi -> atoi
2019-08-07 11:09:17 -07:00
Clifford Wolf
9260e97aa2
Automatically prune init attributes in verific front-end, fixes #1237
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-08-07 15:31:49 +02:00
Eddie Hung
c11ad24fd7
Use std::stoi instead of atoi(<str>.c_str())
2019-08-06 16:45:48 -07:00
Eddie Hung
046e1a5214
Use State::S{0,1}
2019-08-06 16:22:47 -07:00
Clifford Wolf
fc462c8243
Call "read_verilog" with -defer from "read"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-07-29 10:29:36 +02:00
Clifford Wolf
36120fcc30
Only support Symbiotic EDA flavored Verific
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-06-02 10:14:50 +02:00
Clifford Wolf
2faa1d0e80
Enable Verific flag veri_elaborate_top_level_modules_having_interface_ports, fixes #1055
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-05-30 10:04:26 +02:00
Eddie Hung
c7d7d8ad1b
For hier_tree::Elaborate() also include SV root modules (bind)
2019-05-03 20:53:25 +02:00
Eddie Hung
3ea54ec400
Fix verific_parameters construction, use attribute to mark top netlists
2019-05-03 20:53:25 +02:00
Eddie Hung
a27b42e975
WIP -chparam support for hierarchy when verific
2019-05-03 20:53:25 +02:00
Eddie Hung
0f1a4cc03c
verific_import() changes to avoid ElaborateAll()
2019-05-03 20:53:25 +02:00
Clifford Wolf
7682629b79
Add "read -verific" and "read -noverific"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-27 14:03:35 +01:00
Clifford Wolf
c863796e9f
Fix "verific -extnets" for more complex situations
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-26 14:17:46 +01:00
Clifford Wolf
cebd21aa96
Merge pull request #858 from YosysHQ/clifford/svalabels
...
Add support for using SVA labels in yosys-smtbmc console output
2019-03-09 11:14:57 -08:00
Eddie Hung
ee013fba54
Update help message for -chparam
2019-03-09 01:56:16 +00:00
Eddie Hung
2aa3903757
Add -chparam option to verific command
2019-03-09 01:54:01 +00:00
Eddie Hung
1dc060f32e
Fix spelling
2019-03-09 00:43:50 +00:00
Clifford Wolf
cda37830b0
Add hack for handling SVA labels via Verific
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-03-07 10:52:44 -08:00
Clifford Wolf
60e3c38054
Improve "read" error msg
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-28 20:34:42 -08:00
Clifford Wolf
a516b4fb5a
Check if Verific was built with DB_PRESERVE_INITIAL_VALUE
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-02-24 19:51:30 +01:00
Clifford Wolf
6d1e7e9403
Remove -m32 Verific eval lib build instructions
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-04 15:03:49 +01:00
Clifford Wolf
1eb101a38a
Improve VerificImporter support for writes to asymmetric memories
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-02 15:33:43 +01:00
Clifford Wolf
50b09de033
Fix VerificImporter asymmetric memories error message
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2019-01-02 15:05:23 +01:00
whitequark
efa278e232
Fix typographical and grammatical errors and inconsistencies.
...
The initial list of hits was generated with the codespell command
below, and each hit was evaluated and fixed manually while taking
context into consideration.
DIRS="kernel/ frontends/ backends/ passes/ techlibs/"
DIRS="${DIRS} libs/ezsat/ libs/subcircuit"
codespell $DIRS -S *.o -L upto,iff,thru,synopsys,uint
More hits were found by looking through comments and strings manually.
2019-01-02 13:12:17 +00:00
Clifford Wolf
3d671630e2
Improve src tagging (using names and attrs) of cells and wires in verific front-end
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-18 16:01:22 +01:00
Clifford Wolf
910d94b212
Verific updates
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-12-06 07:21:50 +01:00
Clifford Wolf
5387ccb041
Set Verific flag vhdl_support_variable_slice=1
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-11-09 21:03:23 +01:00
Clifford Wolf
9850de405a
Improve Verific importer blackbox handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-10-07 19:48:55 +02:00
Clifford Wolf
4b0448fc2c
Fix compiler warning in verific.cc
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-10-05 09:26:10 +02:00
Clifford Wolf
5d9d22f66d
Add "verific -L <int>" option
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-09-04 20:06:10 +02:00
Clifford Wolf
408077769f
Add "verific -work" help message
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-08-22 17:22:24 +02:00
Clifford Wolf
4b02ee9162
Add Verific -work parameter
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-08-22 13:30:22 +02:00
Clifford Wolf
e343f3e6d4
Add "verific -set-<severity> <msg_id>.."
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-08-16 11:49:17 +02:00
Clifford Wolf
0899a53bee
Verific workaround for VIPER ticket 13851
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-08-16 11:31:19 +02:00
Clifford Wolf
67b1026297
Merge pull request #591 from hzeller/virtual-override
...
Consistent use of 'override' for virtual methods in derived classes.
2018-08-15 14:05:38 +02:00
Clifford Wolf
e275692e84
Verific: Produce errors for instantiating unknown module
...
Because if the unknown module is connected to any constants, Verific will
actually break all constants in the same module, even if they have nothing
to do structurally with that instance of an unknown module.
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-07-22 18:44:05 +02:00
Henner Zeller
3aa4484a3c
Consistent use of 'override' for virtual methods in derived classes.
...
o Not all derived methods were marked 'override', but it is a great
feature of C++11 that we should make use of.
o While at it: touched header files got a -*- c++ -*- for emacs to
provide support for that language.
o use YS_OVERRIDE for all override keywords (though we should probably
use the plain keyword going forward now that C++11 is established)
2018-07-20 23:51:06 -07:00
Clifford Wolf
65234d4b24
Fix handling of eventually properties in verific importer
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-07-17 12:43:30 +02:00
Clifford Wolf
5041ed2f7d
Fix verific -vlog-incdir and -vlog-libdir handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-07-16 18:47:42 +02:00
Clifford Wolf
f897af626d
Fix "read -incdir"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-07-16 16:48:09 +02:00
Clifford Wolf
f39b897545
Add "read -incdir"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-07-16 15:32:26 +02:00
Clifford Wolf
8b92ddb9d2
Fix verific eventually handling
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-29 19:24:58 +02:00
Clifford Wolf
0404cf61d5
Add verific support for eventually properties
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-29 19:21:04 +02:00
Clifford Wolf
ebf0f003d3
Add "verific -formal" and "read -formal"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-29 10:02:27 +02:00
Clifford Wolf
afedb2d03e
Add "read -sv -D" support
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-28 23:58:15 +02:00
Clifford Wolf
07e616900c
Add "read -undef"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-28 23:43:38 +02:00
Clifford Wolf
848c3c5c88
Add YOSYS_NOVERIFIC env variable for temporarily disabling verific
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-22 20:40:22 +02:00
Clifford Wolf
d412b17259
Add simplified "read" command, enable extnets in implicit Verific import
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-21 16:56:55 +02:00
Clifford Wolf
5f2bc1ce76
Add automatic verific import in hierarchy command
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-20 23:45:01 +02:00
Clifford Wolf
4372cf690d
Add (* gclk *) attribute support
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-06-01 13:25:42 +02:00
Clifford Wolf
9a946c207f
Add comment to VIPER #13453 work-around
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-28 13:36:35 +02:00
Clifford Wolf
001c9f1d45
Fix Verific handling of single-bit anyseq/anyconst wires
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-25 15:41:45 +02:00
Clifford Wolf
251562a491
Fix VerificClocking for cases where Verific generates chains of PRIM_SVA_POSEDGE
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-24 18:13:38 +02:00
Clifford Wolf
4d645f0fce
Fix verific handling of anyconst/anyseq attributes
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-24 17:07:06 +02:00
Clifford Wolf
a7281930c5
Fix handling of anyconst/anyseq attrs in VHDL code via Verific
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-15 19:27:00 +02:00
Clifford Wolf
24e6401617
Further improve handling of zero-length SVA consecutive repetition
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-05 14:32:04 +02:00
Clifford Wolf
3e67497ec2
Fix handling of zero-length SVA consecutive repetition
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-05-05 13:58:01 +02:00
Clifford Wolf
617c60cea6
Add PRIM_HDL_ASSERTION support to Verific importer
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-07 18:38:42 +02:00
Clifford Wolf
0ac768f9df
Fix handling of $global_clocking in Verific
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-06 21:23:47 +02:00
Clifford Wolf
278685b084
Add Verific anyseq/anyconst/allseq/allconst attribute support
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-06 14:19:55 +02:00
Clifford Wolf
ab8db2c168
Add "verific -autocover"
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-04-06 14:10:57 +02:00
makaimann
0c404b1f63
Set RAM runtime flags for Verific frontend
2018-04-05 17:38:08 -07:00
Clifford Wolf
93985d91b1
Remove left-over log_ping debug commands.. oops.
...
Signed-off-by: Clifford Wolf <clifford@clifford.at>
2018-03-31 14:23:57 +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
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
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
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
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
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
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
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
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
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
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
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
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
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
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
bc8ab3ab44
Fix verific PRIM_SVA_AT handling in properties with PRIM_SVA_DISABLE_IFF
2018-02-15 15:26:37 +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
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
ba90e08398
Add support for Verific PRIM_SVA_NOT properties
2017-12-10 01:10:03 +01:00
Clifford Wolf
e4a4c0e10c
Add Verific OPER_SVA_STABLE support
2017-12-10 00:59:44 +01:00
Clifford Wolf
27916105a9
Refactoring Verific SVA rewriter
2017-12-10 00:26:26 +01:00
Clifford Wolf
0a31a0b3ae
Remove all PSL support code from verific.cc
2017-10-20 13:14:04 +02:00
Clifford Wolf
1954c78ea7
Add "verific -vlog-libdir"
2017-10-13 20:23:19 +02:00
Clifford Wolf
e7a3c47cc7
Add "verific -vlog-incdir" and "verific -vlog-define"
2017-10-13 20:12:51 +02:00
Clifford Wolf
05068af880
Update Verific README
2017-10-13 17:11:53 +02:00
Clifford Wolf
bc5cc4e103
Add Verific fairness/liveness support
2017-10-12 12:00:09 +02:00
Clifford Wolf
c10e96c9ec
Start work on pre-processor for Verific SVA properties
2017-10-10 15:16:39 +02:00
Clifford Wolf
fc3378916d
Improve handling of Verific errors
2017-10-05 14:38:32 +02:00
Clifford Wolf
ee56a887b6
Improve Verific error handling, check VHDL static asserts
2017-10-04 18:56:28 +02:00
Clifford Wolf
b92ff2706e
Fix nasty bug in Verific bindings
2017-10-04 17:23:42 +02:00
Clifford Wolf
15073790bf
Add merging of "past FFs" to verific importer
2017-07-29 00:10:38 +02:00
Clifford Wolf
d4b9602cbd
Add minimal support for PSL in VHDL via Verific
2017-07-28 17:39:49 +02:00
Clifford Wolf
5a828fff34
Improve Verific HDL language options
2017-07-28 15:32:54 +02:00
Clifford Wolf
acd6cfaf67
Fix handling of non-user-declared Verific netbus
2017-07-28 11:31:27 +02:00
Clifford Wolf
c1cfca8f54
Improve Verific SVA importer
2017-07-27 14:05:09 +02:00
Clifford Wolf
2336d5508b
Add log_warning_noprefix() API, Use for Verific warnings and errors
2017-07-27 12:17:04 +02:00
Clifford Wolf
d9641621d9
Add "verific -import -n" and "verific -import -nosva"
2017-07-27 11:54:45 +02:00
Clifford Wolf
90d8329f64
Improve Verific SVA import: negedge and $past
2017-07-27 11:40:07 +02:00
Clifford Wolf
147ff96ba3
Improve Verific SVA importer
2017-07-27 10:39:39 +02:00
Clifford Wolf
530040ba6f
Improve Verific bindings (mostly related to SVA)
2017-07-26 18:00:01 +02:00
Clifford Wolf
abd3b4e8e7
Improve "help verific" message
2017-07-25 15:13:22 +02:00
Clifford Wolf
6dbe1d4c92
Add "verific -extnets"
2017-07-25 14:53:11 +02:00
Clifford Wolf
c97c92e4ec
Improve "verific -all" handling
2017-07-25 13:33:25 +02:00
Clifford Wolf
41be530c4e
Add "verific -import -d <dump_file"
2017-07-24 13:57:16 +02:00
Clifford Wolf
92d3aad670
Add "verific -import -flatten" and "verific -import -v"
2017-07-24 11:29:06 +02:00
Clifford Wolf
5be535517c
Add "verific -import -k"
2017-07-22 16:16:44 +02:00
Clifford Wolf
2785aaffeb
Improve docs for verific bindings, add simply sby example
2017-07-22 11:58:51 +02:00
Clifford Wolf
28039c3063
Add Verific Release information to log
2017-07-04 20:01:30 +02:00
Clifford Wolf
cdb6ceb8c6
Add support for verific mem initialization
2017-02-11 15:57:36 +01:00
Clifford Wolf
c449f4b86f
Fix another stupid bug in the same line
2017-02-11 11:47:51 +01:00
Clifford Wolf
fa4a7efe15
Add verific support for initialized variables
2017-02-11 11:40:18 +01:00
Clifford Wolf
0b7aac645c
Improve handling of Verific warnings and error messages
2017-02-11 11:39:50 +01:00
Clifford Wolf
eb7b18e897
Fix extremely stupid typo
2017-02-11 11:09:07 +01:00
Clifford Wolf
2ca8d483dd
Add "rand" and "rand const" verific support
2017-02-09 12:53:46 +01:00
Clifford Wolf
1d1f56a361
Add PSL parser mode to verific front-end
2017-02-08 10:40:33 +01:00
Clifford Wolf
3928482a3c
Add $cover cell type and SVA cover() support
2017-02-04 14:14:26 +01:00
Clifford Wolf
911c44d164
Add assert/assume support to verific front-end
2017-02-04 13:36:00 +01:00
Clifford Wolf
0bc95f1e04
Added "yosys -D" feature
2016-04-21 23:28:37 +02:00
Clifford Wolf
7bd329afa0
Support for more Verific primitives (patch I got per email)
2016-02-13 08:19:30 +01:00
Clifford Wolf
6a27cbe5b1
Bugfix in Verific front-end
2016-02-03 08:59:57 +01:00
Clifford Wolf
4a3e1ded1e
Updated verific build instructions
2016-02-02 19:50:17 +01:00
Clifford Wolf
ba407da187
Added addBufGate module method
2016-02-02 11:26:07 +01:00
Clifford Wolf
ab2d8e5c8c
Added PRIM_DLATCHRS support to verific front-end
2015-11-24 12:16:19 +01:00
Clifford Wolf
415e0a1b90
Fixed performance bug in Verific importer
2015-11-16 12:38:56 +01:00
Clifford Wolf
b18f3a2974
Changes for Verific 3.16_484_32_151112
2015-11-12 19:28:14 +01:00
Clifford Wolf
207736b4ee
Import more std:: stuff into Yosys namespace
2015-10-25 19:30:49 +01:00
Clifford Wolf
924d9d6e86
Added read-enable to memory model
2015-09-25 12:23:11 +02:00
Clifford Wolf
84bf862f7c
Spell check (by Larry Doolittle)
2015-08-14 10:56:05 +02:00
Clifford Wolf
6c84341f22
Fixed trailing whitespaces
2015-07-02 11:14:30 +02:00
Clifford Wolf
61512b6f41
Verific build fixes
2015-05-17 08:19:52 +02:00
Clifford Wolf
fe829bdbdc
Added log_warning() API
2014-11-09 10:44:23 +01:00
Clifford Wolf
acf010d30d
Added "ENABLE_PLUGINS := 0" to verific amd64 build instructions
2014-11-08 11:38:44 +01:00
William Speirs
31267a1ae8
Header changes so it will compile on VS
2014-10-17 11:41:36 +02:00
Clifford Wolf
4569a747f8
Renamed SIZE() to GetSize() because of name collision on Win32
2014-10-10 17:07:24 +02:00
Ruben Undheim
79cbf9067c
Corrected spelling mistakes found by lintian
2014-09-06 08:47:06 +02:00
Clifford Wolf
7f734ecc09
Added module->uniquify()
2014-08-16 23:50:36 +02:00
Clifford Wolf
f092b50148
Renamed $_INV_ cell type to $_NOT_
2014-08-15 14:11:40 +02:00
Clifford Wolf
593264e9ed
Fixed building verific bindings
2014-08-12 15:21:06 +02:00
Clifford Wolf
c6fd82c70b
Fixed build of verific bindings
2014-07-31 16:45:23 +02:00
Clifford Wolf
e6d33513a5
Added module->design and cell->module, wire->module pointers
2014-07-31 14:11:39 +02:00
Clifford Wolf
1cb25c05b3
Moved some stuff to kernel/yosys.{h,cc}, using Yosys:: namespace
2014-07-31 13:19:47 +02:00
Clifford Wolf
7bd2d1064f
Using log_assert() instead of assert()
2014-07-28 11:27:48 +02:00
Clifford Wolf
7661ded8dd
Fixed verific bindings for new RTLIL api
2014-07-27 12:00:28 +02:00
Clifford Wolf
1488bc0c4f
Updated verific build/test instructions
2014-07-25 12:16:03 +02:00
Clifford Wolf
375aa71dfe
Various fixes in Verific frontend for new RTLIL API
2014-07-23 21:35:01 +02:00
Clifford Wolf
a3b9692a68
Fixed mapping of Verific WIDE_DFFRS operator
2014-03-20 13:40:01 +01:00
Clifford Wolf
470c2455e4
Fixed mapping of Verific FADD primitive with unconnected outputs
2014-03-20 13:26:52 +01:00
Clifford Wolf
cdf1257565
Progress in Verific bindings
2014-03-17 14:43:16 +01:00
Clifford Wolf
0b0dcfda7d
Progress in Verific bindings
2014-03-17 02:43:53 +01:00
Clifford Wolf
a67cd2d4a2
Progress in Verific bindings
2014-03-17 01:56:00 +01:00
Clifford Wolf
acda74c12c
Added support for memories to verific bindings
2014-03-16 17:05:05 +01:00
Clifford Wolf
7545510edc
Use Verific Net::{IsGnd,IsPwr} API in Verific bindings
2014-03-16 16:06:03 +01:00
Clifford Wolf
0ebee4c8e7
Progress in Verific bindings
2014-03-15 22:51:12 +01:00
Clifford Wolf
fc2c821407
Progress in Verific bindings
2014-03-15 15:31:54 +01:00
Clifford Wolf
1d00ad9d4d
Progress in Verific bindings
2014-03-15 14:36:11 +01:00
Clifford Wolf
e37d672ae7
Progress in Verific bindings
2014-03-14 16:40:25 +01:00
Clifford Wolf
0ac915a757
Progress in Verific bindings
2014-03-14 11:46:13 +01:00
Clifford Wolf
9a1accf692
Progress in Verific bindings
2014-03-13 18:21:00 +01:00
Clifford Wolf
6a53bc7b27
Copy Verific vdbs files to Yosys "share" data directory
2014-03-13 17:34:31 +01:00
Clifford Wolf
7a1ac11203
Added test_navre.ys for verific frontend
2014-03-13 13:12:06 +01:00
Clifford Wolf
5a15539c9b
Improved verific command (added support for some operators)
2014-03-10 12:06:57 +01:00
Clifford Wolf
c71791a1ff
Improvements in verific command
2014-03-10 03:03:08 +01:00
Clifford Wolf
8d06f9f2fe
Added "verific" command
2014-03-09 20:40:04 +01:00