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
3cbca5064c
verific: Handle non-seq properties with VerificClocking conditions
2023-04-21 17:19:42 +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 Milanović
d19f9d0b66
Update README
2022-07-28 12:32:19 +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
Jannis Harder
96f64f4788
verific: Fix conditions of SVAs with explicit clocks within procedures
...
For SVAs that have an explicit clock and are contained in a procedure
which conditionally executes the assertion, verific expresses this using
a mux with one input connected to constant 1 and the other output
connected to an SVA_AT. The existing code only handled the case where
the first input is connected to 1. This patch also handles the other
case.
2022-05-03 14:13:08 +02:00
Miodrag Milanovic
422db937d4
Ignore merging past ffs that we are not properly merging
2022-04-29 14:35:02 +02:00
Miodrag Milanovic
1cc281ca6f
verific: allow memories to be inferred in loops (vhdl)
2022-04-18 09:10:28 +02:00
N. Engelhardt
57bc29c64a
verific: allow memories to be inferred in loops
2022-04-15 15:10:48 +02:00
Miodrag Milanovic
1a1f529099
Preserve internal wires for external nets
2022-04-01 12:07:15 +02:00
Miodrag Milanovic
bbf65702a1
Fix valgrind tests when using verific
2022-03-30 17:25:53 +02:00
Miodrag Milanovic
703769e494
Properly mark modules imported
2022-03-26 09:43:51 +01:00
Miodrag Milanovic
245ecb0529
Import verific netlist in consistent order
2022-03-25 13:44:16 +01:00
Miodrag Milanovic
29293a57bb
Remove quotes if any from attribute
2022-02-16 19:10:13 +01:00
Miodrag Milanovic
2cef48bf2c
Add ability to override verilog mode for verific -f command
2022-02-09 09:19:25 +01:00
Miodrag Milanovic
0b633b6c2e
Use bmux for NTO1MUX
2022-02-02 16:16:08 +01:00
Claire Xenia Wolf
313340aed5
Add YOSYS to the implicitly defined verilog macros in verific
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-12-13 18:20:08 +01:00
Miodrag Milanović
2412497c26
Merge pull request #3102 from YosysHQ/claire/enumxz
...
Fix verific import of enum values with x and/or z
2021-12-10 19:36:37 +01:00
Claire Xenia Wolf
2da214d721
Fix verific import of enum values with x and/or z
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-12-10 14:52:27 +01:00
Claire Xen
19773d093f
Update verific.cc
...
Ad-hoc fixes/improvements
2021-12-10 14:27:18 +01:00
Miodrag Milanovic
b06f547993
If direction NONE use that from first bit
2021-12-08 11:50:10 +01:00
Miodrag Milanovic
3ebfa3fb84
Make sure cell names are unique for wide operators
2021-12-03 09:49:05 +01:00
Miodrag Milanovic
15a35f5584
No need to alocate more memory than used
2021-11-10 10:50:44 +01:00
Claire Xenia Wolf
2ea757da51
Add "verific -cfg" command
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-11-01 10:41:51 +01:00
Claire Xenia Wolf
83118bfb9e
Fix verific gclk handling for async-load FFs
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-31 17:12:29 +01:00
Miodrag Milanovic
f7cc388bb5
Enable async load dff emit by default in Verific
2021-10-27 15:56:56 +02:00
Miodrag Milanovic
32673edfea
Revert "Compile option for enabling async load verific support"
...
This reverts commit b8624ad2ae
.
2021-10-27 15:55:43 +02:00
Miodrag Milanovic
b8624ad2ae
Compile option for enabling async load verific support
2021-10-25 09:04:43 +02:00
Claire Xenia Wolf
90b440f870
Fix verific.cc PRIM_DLATCH handling
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-21 12:13:35 +02:00
Claire Xenia Wolf
16a177560f
Initial Verific impoter support for {PRIM,WIDE_OPER}_DLATCH{,RS}
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-21 05:42:47 +02:00
Miodrag Milanovic
17269ae59b
Option to disable verific VHDL support
2021-10-20 10:02:58 +02:00
Miodrag Milanovic
1aa6896966
Support PRIM_BUFIF1 primitive
2021-10-14 13:04:32 +02:00
Claire Xen
2d3c79458d
Merge pull request #3039 from YosysHQ/claire/verific_aldff
...
Add support for $aldff flip-flops to verific importer
2021-10-11 10:01:56 +02:00
Claire Xenia Wolf
c8074769b0
Add Verific adffe/dffsre/aldffe FIXMEs
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-11 10:00:20 +02:00
Miodrag Milanovic
93fbc9fba4
Import module attributes from Verific
2021-10-10 10:01:45 +02:00
Claire Xenia Wolf
34f1df8435
Fixes and add comments for open FIXME items
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-08 17:24:45 +02:00
Claire Xenia Wolf
1602a03864
Add support for $aldff flip-flops to verific importer
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-10-08 16:21:25 +02:00
Miodrag Milanovic
abc5700628
verific set db_infer_set_reset_registers
2021-10-04 16:48:33 +02:00
Miodrag Milanovic
c3d4bb4cc9
update required verific version
2021-09-02 14:59:16 +02:00
Miodrag Milanovic
b59c427348
Make Verific extensions optional
2021-08-20 10:19:04 +02:00
Miodrag Milanovic
be04d8834e
Require latest verific
2021-08-02 10:29:58 +02:00
Miodrag Milanovic
987fca5297
Update to latest verific
2021-07-21 09:46:53 +02:00
Miodrag Milanovic
7a5ac90985
Update to latest Verific with extensions for initial assertions
2021-07-09 09:02:27 +02:00
Miodrag Milanovic
0dbb05a75e
Add additional help
2021-07-05 09:16:54 +02:00
Miodrag Milanovic
c0d8da20d5
Support command files in Verific
2021-06-16 11:21:44 +02:00
Claire Xenia Wolf
72787f52fc
Fixing old e-mail addresses and deadnames
...
s/((Claire|Xen|Xenia|Clifford)\s+)+(Wolf|Xen)\s+<(claire|clifford)@(symbioticeda.com|clifford.at|yosyshq.com)>/Claire Xenia Wolf <claire@yosyshq.com>/gi;
s/((Nina|Nak|N\.)\s+)+Engelhardt\s+<nak@(symbioticeda.com|yosyshq.com)>/N. Engelhardt <nak@yosyshq.com>/gi;
s/((David)\s+)+Shah\s+<(dave|david)@(symbioticeda.com|yosyshq.com|ds0.me)>/David Shah <dave@ds0.me>/gi;
s/((Miodrag)\s+)+Milanovic\s+<(miodrag|micko)@(symbioticeda.com|yosyshq.com)>/Miodrag Milanovic <micko@yosyshq.com>/gi;
s,https?://www.clifford.at/yosys/,http://yosyshq.net/yosys/,g ;
2021-06-08 00:39:36 +02:00
Claire Xen
6c56c083f8
Update README
2021-03-04 16:43:30 +01:00
Claire Xen
27d7741540
Merge pull request #2574 from dh73/master
...
Accept disable case for SVA liveness properties.
2021-02-15 17:49:11 +01:00
Miodrag Milanovic
13c2fd7137
Ganulate Verific support
2021-02-12 10:08:43 +01:00
Diego H
c96eb2fbd7
Accept disable case for SVA liveness properties.
2021-02-04 15:35:35 -06:00
Miodrag Milanovic
d99c032c27
Require latest Verific build
2021-01-30 09:23:46 +01:00
Claire Xenia Wolf
acad7a6e40
Switch verific bindings from Symbiotic EDA flavored Verific to YosysHQ flavored Verific
...
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
2021-01-20 20:48:10 +01:00
Miodrag Milanovic
1c4a18f66f
Bump required Verific version
2020-12-02 15:18:04 +01:00