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
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