Commit Graph

190 Commits

Author SHA1 Message Date
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