Commit Graph

301 Commits

Author SHA1 Message Date
Miodrag Milanovic 7b134c2a8c verific - respect order of read and write for rams 2023-09-12 11:56:15 +02:00
Miodrag Milanovic 19d5293657 when blackboxing no need to know missing modules 2023-07-31 09:18:54 +02:00
Miodrag Milanovic 372760af57 spaces to tabs 2023-07-25 09:40:30 +02:00
Miodrag Milanovic 3989181cd6 Add ability to blackbox modules/units from file while reading with verific 2023-07-25 09:40:30 +02:00
N. Engelhardt 21686f0d9d verific: import src attribute on $memrd/$memwr cells 2023-06-23 19:41:36 +02:00
Miodrag Milanovic aff0065646 Use defaultvalue for init values of input ports 2023-06-21 13:21:34 +02:00
Miodrag Milanovic 75cf79588e Add ability for user plugin to add new verific log callback 2023-06-12 10:01:01 +02:00
Miodrag Milanovic ecd289c100 Fix importing parametrized VHDL entity 2023-05-23 08:25:08 +02:00
Jannis Harder ec47bf1745 verific: Handle conditions when using sva_at_only in VerificClocking
This handles conditions on clocked concurrent assertions in unclocked
procedural contexts.
2023-04-21 16:51:42 +02:00
Jannis Harder 390d1c583a verific: Fix enum_values support and signed attribute values
This uses the same constant parsing for enum_values and for attributes
and extends it to handle signed values as those are used for enums that
implicitly use the int type.
2023-03-15 09:51:36 +01:00
Miodrag Milanovic a30894e5fa Handle more wide case selector types 2023-02-27 09:24:04 +01:00
Miodrag Milanovic 109b88c379 For case select values use Sa instead of Sx and Sz 2023-02-08 09:22:48 +01:00
Miodrag Milanovic e7e37df91b Add verific import support for OPER_WIDE_CASE_SELECT_BOX 2023-02-06 09:28:23 +01:00
Miodrag Milanovic 6574553189 Fixes for some of clang scan-build detected issues 2023-01-17 12:58:08 +01:00
Miodrag Milanovic b867dee241 respect noblackbox attribute in verific 2022-12-15 08:17:53 +01:00
Miodrag Milanović 9362fdb4c6
Merge pull request #3568 from YosysHQ/verific_msg
Set all Verific messages of certain type to other
2022-12-05 16:22:44 +01:00
Miodrag Milanovic 34a64aa322 set VERI-1063 explicitly 2022-12-02 17:11:17 +01:00
Miodrag Milanovic 2dd55d73a0 reset elaboration error after rewriter 2022-11-30 17:26:48 +01:00
Miodrag Milanovic bfd79845b6 Set all verific messages of certain type to other 2022-11-30 16:42:37 +01:00
Miodrag Milanovic f764cd1655 update documentation 2022-11-25 14:27:30 +01:00
Miodrag Milanovic b0be19c126 Support importing verilog configurations using Verific 2022-11-25 13:02:11 +01:00
Miodrag Milanovic 59b6ac47c9 Add additional help info 2022-10-31 18:04:34 +01:00
Miodrag Milanovic 6fb80bce15 Enable importing blackbox modules only 2022-10-31 10:51:28 +01:00
Miodrag Milanovic e702f2894a Support for reading liberty files using verific 2022-10-31 10:15:05 +01:00
Miodrag Milanovic 48628fbf5a Skip verific primitives and operators import by default 2022-10-14 17:41:24 +02:00
Miodrag Milanovic 922f8b614a Add option to import all cells from all libraries 2022-10-14 16:54:57 +02:00
Claire Xenia Wolf 090228a6a1 Fix handling of verific -L options, add implicit "-L work"
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2022-10-10 00:47:42 +02:00
Miodrag Milanovic 1a6f10e8ba Add support for EDIF file reading using Verific 2022-10-04 09:18:44 +02:00
Miodrag Milanovic 43267dec99 support file content redirection for verific frontened 2022-09-28 15:56:46 +02:00
Miodrag Milanovic b45517f7b7 Add comment for future self 2022-09-28 14:45:39 +02:00
Miodrag Milanovic f54ac8a6d6 Handle attributes imported from verific 2022-09-28 08:51:26 +02:00
Miodrag Milanovic 8fb498744f Import memory attributes 2022-09-21 15:48:40 +02:00
Miodrag Milanovic 3f94f9313a verific: better fix for read callback 2022-09-07 09:48:19 +02:00
Miodrag Milanovic 06a9c7499a verific: fix crash when using prep right after read 2022-09-07 09:40:14 +02:00
Miodrag Milanovic 6c65ca4e50 Encode filename unprintable chars 2022-08-08 16:13:33 +02:00
Miodrag Milanovic 2b1aeb44d9 verific - make filepath handling compatible with verilog frontend 2022-08-08 11:57:28 +02:00
Miodrag Milanovic 52a4a89265 Setting wire upto in verific import 2022-07-29 17:10:31 +02:00
Miodrag Milanovic 59b96bb1f8 Upadte documentation and changelog 2022-07-04 11:09:06 +02:00
Miodrag Milanovic b80976b543 Update to new verific extensions inteface 2022-06-30 11:19:01 +02:00
Miodrag Milanovic 1fdbb42fdd Revert "use new verific extensions library"
This reverts commit 607e957657.
2022-06-21 18:07:47 +02:00
Miodrag Milanovic 607e957657 use new verific extensions library 2022-06-17 16:04:22 +02:00
Miodrag Milanovic ddc8044655 removed deprecated features code 2022-06-13 10:50:24 +02:00
Miodrag Milanovic 6e8e4b4550 verific: Added "-vlog-libext" option to specify search extension for libraries 2022-06-09 08:57:48 +02:00
Miodrag Milanovic e35a166353 verific: proper file location for readmem commands 2022-06-04 08:39:50 +02:00
Miodrag Milanovic fdb393b6ce fix text to fit 80 columns 2022-05-23 19:57:21 +02:00
Miodrag Milanovic 4a5790d404 Update verific command file documentation 2022-05-23 19:35:14 +02:00
Miodrag Milanovic a6ec5754c6 Use analysis mode if set in file 2022-05-23 19:13:45 +02:00
Jannis Harder fada77b8cf verific: Use new value change logic also for $stable of wide signals.
I missed this in the previous PR.
2022-05-11 13:05:27 +02:00
Jannis Harder 587e09d551
Merge pull request #3305 from jix/sva_value_change_logic
verific: Improve logic generated for SVA value change expressions
2022-05-09 16:40:34 +02:00
Jannis Harder a855d62b42 verific: Improve logic generated for SVA value change expressions
The previously generated logic assumed an unconstrained past value in
the initial state and did not handle 'x values. While the current formal
verification flow uses 2-valued logic, SVA value change expressions
require a past value of 'x during the initial state to behave in the
expected way (i.e. to consider both an initial 0 and an initial 1 as
$changed and an initial 1 as $rose and an initial 0 as $fell).

This patch now generates logic that at the same time

	a) provides the expected behavior in a 2-valued logic setting, not
	   depending on any dont-care optimizations, and

	b) properly handles 'x values in yosys simulation
2022-05-09 15:04:01 +02:00