N. Engelhardt
642756a9c6
Merge pull request #5178 from jix/sva_cover_only_followed_by
2025-07-07 10:07:06 +02:00
Miodrag Milanovic
eed3bc243f
verific: enable replacing const exprs in static elaboration by default
2025-07-02 11:54:19 +02:00
Jannis Harder
f019e44e74
verificsva: Support the followed-by operator in cover mode
...
The implementation for the implication operator in cover mode actually
implements the followed-by operator, so we can re-use it unchanged.
It is not always the correct behavior for the implication operator in
cover mode, but a) it will only cause false positives not miss anything
so if the behavior is unexpected it will be visible in the produced
traces, b) it is unlikely to make a difference for most properties one
would practically use in cover mode, c) at least one other widely used
SVA implementations behaves the same way and d) it's not clear whether
we can fix this without rewriting most of verificsva.cc
2025-06-13 21:27:31 +02:00
N. Engelhardt
f22248f056
downgrade verific warnings about common coding styles
2025-06-06 16:30:50 +02:00
Emil J. Tywoniak
e5171d6aa1
verific: support single_bit_vector
2025-05-12 13:23:29 +02:00
Miodrag Milanovic
22e6ce4282
verific: bit blast RAM if using mem2reg attribute
2025-04-14 15:24:11 +02:00
Miodrag Milanovic
72f2185a94
verific: fix restoring msg state after blackbox import
2025-04-01 17:35:59 +02:00
Emil J. Tywoniak
4f3fdc8457
io: refactor string and file work into new unit
2025-03-19 13:43:42 +01:00
Jason Xu
a5f34d04f8
Address comments
2025-03-11 18:50:44 -04:00
Jason Xu
98eefc5d1a
Add file list support to read pass
2025-03-07 20:44:21 -05:00
N. Engelhardt
d640157ec4
fix some cases of hdlname being added to objects with private names
2025-01-15 15:56:42 +01:00
Emil J. Tywoniak
d071489ab1
hashlib: redo interface for flexibility
2024-12-18 14:49:25 +01:00
N. Engelhardt
378864d33b
bound attributes: handle vhdl null ranges
2024-12-12 11:42:39 +01:00
N. Engelhardt
03033ab6d4
add more tests for bounds attributes, fix attributes appearing in verilog
2024-12-11 16:11:02 +01:00
Miodrag Milanovic
7d4aff618f
verific: Disable module existence check during static elaboration
2024-12-06 15:59:09 +01:00
Miodrag Milanovic
912b38eedb
verific: Handle crash when using empty box option
2024-12-02 15:45:12 +01:00
Miodrag Milanović
29e8812bab
Merge pull request #4724 from YosysHQ/micko/blackbox_verific
...
verific: fix blackbox regression and add test case
2024-11-25 15:06:54 +01:00
Miodrag Milanovic
d6bd521487
verific : VHDL assert DFF initial value set on Verific library patch side
2024-11-21 13:43:26 +01:00
Mike Inouye
06e3ac4415
Fix bug when setting Verific runtime string flags.
...
Signed-off-by: Mike Inouye <mikeinouye@google.com>
2024-11-12 18:46:26 +00:00
Miodrag Milanovic
df391f5816
verific: fix blackbox regression and add test case
2024-11-08 14:57:04 +01:00
Emil J
caf56ca3e8
Merge pull request #4516 from YosysHQ/emil/src-attribute-std-string-wip
...
Represent string constants as strings
2024-10-14 06:42:54 -07:00
Emil J. Tywoniak
785bd44da7
rtlil: represent Const strings as std::string
2024-10-14 06:28:12 +02:00
Miodrag Milanovic
8d2b63bb8a
Set VHDL assert condition initial state if fed by FF
2024-10-11 16:32:21 +02:00
Roland Coeurjoly
bdc43c6592
Add left and right bound properties to wire. Add test. Fix printing
...
for signed attributes
Co-authored-by: N. Engelhardt <nak@yosyshq.com>
Co-authored-by: Roland Coeurjoly <rolandcoeurjoly@gmail.com>
2024-09-10 12:52:42 +02:00
Miodrag Milanović
3e14e67374
Merge pull request #4500 from YosysHQ/micko/vhdl_mixcase
...
VHDL is case insensitive, make sure netlist name is proper
2024-07-29 16:44:13 +02:00
Miodrag Milanovic
405897a971
Update top value that is returned back to hierarchy pass
2024-07-29 15:50:38 +02:00
Miodrag Milanovic
9566709426
Initialize extensions when verific pass is registered
2024-07-25 11:25:17 +02:00
Miodrag Milanovic
c94aa719d9
VHDL is case insensitive, make sure netlist name is proper
2024-07-18 16:56:52 +02:00
Miodrag Milanovic
dfde792288
Refactored import code
2024-06-17 14:49:58 +02:00
Miodrag Milanovic
19da7f7d59
Update makefile to make options uniform
2024-06-17 13:29:11 +02:00
Miodrag Milanovic
0f3f731254
Handle -work for vhdl, and clean messages
2024-06-17 13:29:11 +02:00
Miodrag Milanovic
0a81c8e161
Import all modules from all libraries when when needed
2024-06-17 13:29:11 +02:00
Miodrag Milanovic
7c3094633d
Compile with hier_tree separate SV and VHDL as well
2024-06-17 13:29:11 +02:00
Miodrag Milanovic
e2e189647f
Cleanup
2024-06-17 13:29:11 +02:00
Miodrag Milanovic
7bec332b68
SV + VHDL with RTL support
2024-06-17 13:29:11 +02:00
Miodrag Milanovic
25d50bb2af
VHDL only build support
2024-06-17 13:29:11 +02:00
Miodrag Milanovic
54bf9ccf06
Add initial support for Verific without additional YosysHQ patch
2024-06-17 13:29:11 +02:00
Mike Inouye
b0ab1cf8c3
Fix memory leak in verific file parsing.
...
Signed-off-by: Mike Inouye <mikeinouye@google.com>
2024-06-07 22:51:28 +00:00
Ethan Mahintorabi
82a4a87c97
Fixes error with vector indicies of the form [2:7] [-12:7]
...
Make sure that we correctly adjust the value to align it to a zero
indexed list with lsb = 0
Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>
2024-05-08 20:29:47 +00:00
Ethan Mahintorabi
c039da2ec1
renames variables for more code clairty
...
Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>
2024-05-08 01:09:52 +00:00
Ethan Mahintorabi
a2c1b268d9
frontend: Fixes verific import around range order
...
Test Case
```
module packed_dimensions_range_ordering (
input wire [0:4-1] in,
output wire [4-1:0] out
);
assign out = in;
endmodule : packed_dimensions_range_ordering
module instanciates_packed_dimensions_range_ordering (
input wire [4-1:0] in,
output wire [4-1:0] out
);
packed_dimensions_range_ordering U0 (
.in (in),
.out(out)
);
endmodule : instanciates_packed_dimensions_range_ordering
```
```
// with verific, does not pass formal
module instanciates_packed_dimensions_range_ordering(in, out);
input [3:0] in;
wire [3:0] in;
output [3:0] out;
wire [3:0] out;
assign out = { in[0], in[1], in[2], in[3] };
endmodule
// with surelog, passes formal
module instanciates_packed_dimensions_range_ordering(in, out);
input [3:0] in;
wire [3:0] in;
output [3:0] out;
wire [3:0] out;
assign out = in;
endmodule
```
Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>
2024-05-08 01:00:06 +00:00
Miodrag Milanovic
af94123730
verific: expose library name as module attribute
2024-04-15 17:01:07 +02:00
N. Engelhardt
3d5e23e585
Merge pull request #4302 from YosysHQ/vhdl_2019
...
Verific support for VHDL 2019
2024-04-09 18:25:05 +02:00
Miodrag Milanovic
f536de0e0e
Verific support for VHDL 2019
2024-03-28 13:21:55 +01:00
Miodrag Milanovic
4367e176fb
code split and cleanup
2024-03-19 09:15:04 +01:00
Miodrag Milanovic
9eebc80170
handle standard types
2024-03-18 10:35:01 +01:00
Miodrag Milanovic
7c09fa572e
real number handling and default to string
2024-03-14 10:37:56 +01:00
Miodrag Milanovic
4279cea33a
improve handling VHDL constants
2024-03-14 10:37:56 +01:00
Miodrag Milanovic
858eae5572
verific_const: convert VHDL values to RTLIL consts
2024-03-14 10:37:56 +01:00
Miodrag Milanovic
ae7daf99f4
Verific: Add attributes to module instantiation
2024-02-12 09:53:47 +01:00