3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-07-12 15:36:40 +00:00
Commit graph

428 commits

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