Commit Graph

1766 Commits

Author SHA1 Message Date
Martin Povišer 1ac1b2eed5 ast/simplify: Factor out helper to determine range width 2023-07-20 23:40:19 -04:00
Dag Lem cff53d6d87 Corrected handling of nested typedefs of struct/union
This also corrects shadowing of constants in struct/union types.
2023-07-20 23:39:44 -04: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
Kamil Rakoczy 6b3e6d96a3 Fix missing brackets around else
Signed-off-by: Kamil Rakoczy <krakoczy@antmicro.com>
2023-05-10 08:09:11 +02:00
N. Engelhardt 0aeb6105eb
Merge pull request #3736 from jix/conc_assertion_in_unclocked_proc_ctx 2023-05-08 16:15:13 +02:00
Dag Lem ad437c178d Handling of attributes for struct / union variables
(* nowrshmsk *) on a struct / union variable now affects dynamic
bit slice assignments to members of the struct / union.

(* nowrshmsk *) can in some cases yield significant resource savings; the
combination of pipeline shifting and indexed writes is an example of this.

Constructs similar to the one below can benefit from (* nowrshmsk *), and
in addition it is no longer necessary to split out the shift assignments
on separate lines in order to avoid the error message "ERROR: incompatible
mix of lookahead and non-lookahead IDs in LHS expression."

    always_ff @(posedge clk) begin
        if (rotate) begin
            { v5, v4, v3, v2, v1, v0 } <= { v4, v3, v2, v1, v0, v5 };

            if (res) begin
                v0.bytes <= '0;
            end else if (w) begin
                v0.bytes[addr] <= data;
            end
        end
    end
2023-05-03 18:44:07 +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 985f4926b7 verilog: Fix const eval of unbased unsized constants
When the verilog frontend perfomed constant evaluation of unbased
unsized constants in a context-determined expression it did not properly
extend them by repeating the bit value. This only affected constant
evaluation and not constants that made it through unchanged to RTLIL.
The latter case was already covered by tests and working before.

This fixes the const-eval issue by checking the `is_unsized` flag in
bitsAsConst and extending the value accordingly.

The newly added test also tests the already working non-const-eval case
to highlight that both cases should behave the same.
2023-04-20 12:12:50 +02:00
Jannis Harder fb1c2be76b verilog: Support void functions
The difference between void functions and tasks is that always_comb's
implicit sensitivity list behaves as if functions were inlined, but
ignores signals read only in tasks. This only matters for event based
simulation, and for synthesis we can treat a void function like a task.
2023-03-20 12:52:46 +01: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
Jannis Harder c50f641812
Merge pull request #3682 from daglem/struct-member-out-of-bounds
Out of bounds checking for struct/union members
2023-03-10 16:14:56 +01:00
Dag Lem 0d3423ddea Index struct/union members within corresponding wire chunks
This guards against access to bits outside of struct/union
members via dynamic indexing.
2023-03-05 14:54:17 +01:00
Miodrag Milanovic a30894e5fa Handle more wide case selector types 2023-02-27 09:24:04 +01:00
Dag Lem 79043cb849 Out of bounds checking for struct/union members
Currently, only constant indices are checked.
2023-02-19 23:25:08 +01:00
Dag Lem c1e12877f0 Support for data and array queries on struct/union item expressions
For now, $bits, $left, $right, $low, $high, and $size are supported.
2023-02-15 11:44:24 +01:00
Jannis Harder 53bda9de54
Merge pull request #3661 from daglem/struct-array-range-offset
Handle range offsets in packed arrays within packed structs
2023-02-15 11:21:56 +01:00
Dag Lem 615adc4253
Resolve package types in interfaces (#3658)
* Resolve package types in interfaces
* Added test for resolving of package types in interfaces
2023-02-12 18:25:39 -05: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
Dag Lem 777c589e85 Handle range offsets in packed arrays within packed structs
This brings the metadata for packed arrays in packed structs
in line with the metadata for unpacked arrays, and correctly
handles the case when both lsb and msb in an address range are
non-zero.
2023-02-05 17:09:51 +01:00
Dag Lem 26db5a11d3 Resolve struct member package types 2023-01-29 13:51:44 -05:00
Dag Lem db13c6df2b
Handle struct members of union type (#3641) 2023-01-29 13:45:45 -05:00
Miodrag Milanovic 6574553189 Fixes for some of clang scan-build detected issues 2023-01-17 12:58:08 +01:00
N. Engelhardt 692a0fa33b print filename in liberty log_header 2023-01-11 21:31:46 +01:00
Jannis Harder 3ebc50dee4
Merge pull request #3467 from jix/fix_cellarray_simplify
simplify: Do not recursively simplify AST_CELL within AST_CELLARRAY
2022-12-19 16:05:13 +01:00
Miodrag Milanovic b867dee241 respect noblackbox attribute in verific 2022-12-15 08:17:53 +01:00
Jannis Harder 7ad7b550cb
Merge pull request #3573 from daglem/struct-array-multidimensional
Support for packed multidimensional arrays within packed structs
2022-12-07 19:24:12 +01:00
Jannis Harder dd8b412833 simplify: Do not recursively simplify AST_CELL within AST_CELLARRAY
Otherwise the AST_CELL simplification uses the wrong celltype before the
AST_CELLARRAY simplification has a chance to unroll it and change it to
the $array celltype.
2022-12-07 18:21:36 +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 Milanović 26aaf7683f
Merge pull request #3569 from YosysHQ/ver_no_rewriters
verific: Ignore errors produced by extension
2022-12-05 16:21:12 +01:00
Dag Lem 22090011ab Made make_struct_member_range side-effect-free again 2022-12-04 06:54:22 +01:00
Dag Lem f94eec952f Support for packed multidimensional arrays within packed structs 2022-12-03 19:54:47 +01:00
Miodrag Milanovic 34a64aa322 set VERI-1063 explicitly 2022-12-02 17:11:17 +01:00
Jannis Harder 4a2b7287ca
Merge pull request #3551 from daglem/struct-array-swapped-range
Support for arrays with swapped ranges within structs
2022-12-01 00:58:32 +01:00
Dag Lem 64f88eb7f1 Added asserts for current limitation of array dimensions in packed structs 2022-11-30 23:32:41 +01:00
Dag Lem 15c8e74329 Check for all cases of currently unsupported array dimensions in packed structs 2022-11-30 20:04:45 +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
Dag Lem ddb12148e7 Support for swapped ranges in second array dimension 2022-11-23 16:31:08 +01:00
Jannis Harder fc2f622a27
Merge pull request #3552 from daglem/fix-sv-c-array-dimensions
Correct interpretation of SystemVerilog C-style array dimensions
2022-11-23 15:12:17 +01:00
Jannis Harder 239ecf9185 Merge branch 'zachjs-master' 2022-11-21 17:47:43 +01:00
Dag Lem a862642fac Correct interpretation of SystemVerilog C-style array dimensions
IEEE Std 1800™-2017 7.4.2 specifies that [size] is the same as [0:size-1].
2022-11-13 07:41:25 +01:00
Dag Lem bab88630c2 Support for arrays with swapped ranges within structs
This also corrects the implementation of C type arrays within structs.

Fixes #3550
2022-11-12 08:48:25 +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
Zachary Snow 71e7e09092 verilog: Support module-scoped task/function calls
This is primarily intended to enable the standard-permitted use of
module-scoped identifiers to refer to tasks and non-constant functions.
As a side-effect, this also adds support for the non-standard use of
module-scoped identifiers referring to constant functions, a feature
that is supported in some other tools, including Iverilog.
2022-10-29 15:14:11 -04: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
Miodrag Milanovic 03df1ac72b fix whitespace 2022-10-10 16:31:29 +02:00
Miodrag Milanović e8ce9442a6
Merge pull request #3452 from ALGCDG/master
Add BLIF names command input plane size check
2022-10-10 16:29:27 +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
Archie d29606532a Changing error reason string to be based on lut input plane limit constant. 2022-10-02 22:05:51 +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
KrystalDelusion 9465b2af95 Fitting help messages to 80 character width
Uses the regex below to search (using vscode):
	^\t\tlog\("(.{10,}(?<!\\n)|.{81,}\\n)"\);

Finds any log messages double indented (which help messages are)
and checks if *either* there are is no newline character at the end,
*or* the number of characters before the newline is more than 80.
2022-08-24 10:40:57 +12:00
Archie 15a0697c70 Adding check for BLIF names command input plane size. 2022-08-21 23:18:20 -05:00
Miodrag Milanovic b76c72056b set default_nettype to wire for resetall 2022-08-10 13:28:19 +02:00
Miodrag Milanovic 545a3417c8 resetall does not affect text defines, but undefineall does 2022-08-10 11:38:50 +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 Milanović 15393442d6
Merge pull request #3089 from YosysHQ/gatecat/liberty_wb
Add read_liberty -wb
2022-08-01 17:08:04 +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
Archie 7eeb656e2a Add check for BLIF with no model name 2022-06-22 00:34:49 +01: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
Zachary Snow a650d9079f verilog: fix width/sign detection for functions 2022-05-30 16:45:39 -04:00
Jannis Harder 4bfaaea0d5 verilog: fix size and signedness of array querying functions
genrtlil.cc and simplify.cc had inconsistent and slightly broken
handling of signedness for array querying functions. These functions are
defined to return a signed result. Simplify always produced an unsigned
and genrtlil always a signed 32-bit result ignoring the context.

Includes tests for the the relvant edge cases for context dependent
conversions.
2022-05-30 09:11:31 -04:00
Jannis Harder b75fa62e9b verilog: fix $past's signedness 2022-05-25 16:32:08 -04:00
Jannis Harder cffec1f95f verilog: fix signedness when removing unreachable cases 2022-05-24 23:03:31 -04: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
Zachary Snow bf15dbd0f7 sv: fix always_comb auto nosync for nested and function blocks 2022-04-05 14:43:48 -06: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