Commit Graph

1857 Commits

Author SHA1 Message Date
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
Krystine Sherwin df95ea824b read_verilog: Add missing defaults for flags
Fix for YosysHQ/sby#103
2024-05-07 20:25:36 +02:00
George Rennie 4e6deb53b6 read_aiger: Fix incorrect read of binary Aiger without outputs
* Also makes all ascii parsing finish reading lines and adds a small
  test
2024-04-29 14:06:58 +01:00
KrystalDelusion c3ae33da33
Merge pull request #4285 from YosysHQ/typo_fixup
Typo fixing
2024-04-25 09:54:48 +12: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
N. Engelhardt 18afa36acd
Merge pull request #4273 from YosysHQ/vhdl_params
verific: Improve import VHDL constants
2024-04-09 18:01:41 +02:00
Catherine a5441bc00c fmt: `FmtPart::{STRING→LITERAL},{CHARACTER→STRING}`.
Before this commit, the `STRING` variant inserted a literal string;
the `CHARACTER` variant inserted a string. This commit renames them
to `LITERAL` and `STRING` respectively.
2024-04-02 12:13:22 +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
Krystine Sherwin 3eeefd23e3
Typo fixup(s) 2024-03-18 11:09:23 +13: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
Martin Povišer b16f4900fd ast/simplify: Interpret hdlname w/o expecting backslash 2024-02-13 21:38:41 +01:00
Catherine d8ce26a5ba read_verilog: correctly format `hdlname` attribute value.
The leading slash is not a part of the attribute as it only concerns
public values.
2024-02-13 18:41:53 +00:00
Miodrag Milanovic ae7daf99f4 Verific: Add attributes to module instantiation 2024-02-12 09:53:47 +01:00
Dag Lem f09ea16bd1 Resolve struct member multiple dimensions defined in stages with typedef 2024-02-11 11:26:52 -05:00
Dag Lem 03f35c3def Resolve multiple dimensions defined in stages with typedef 2024-02-11 11:26:52 -05:00
Dag Lem e0d3977e19 Add support for $dimensions and $unpacked_dimensions 2024-02-11 11:26:52 -05:00
Dag Lem 2125357e76 Add support for $increment 2024-02-11 11:26:52 -05:00
Dag Lem 88d9e213cb Decoding of a few more AST nodes in dumpVlog 2024-02-11 11:26:52 -05:00
Dag Lem 39fea32c6e Add support for packed multidimensional arrays
* Generalization of dimensions metadata (also simplifies $size et al.)
* Parsing and elaboration of multidimensional packed ranges
2024-02-11 11:26:52 -05:00
Catherine 1236bb65b6 read_verilog: don't include empty `opt_sva_label` in span.
Consider this SystemVerilog file:

    module top(...);
      input clk;
      input [7:0] data;
      input ack;

      always @(posedge clk)
        if (ack) begin
          assert(data != 8'h0a);
        end
    endmodule

Before this commit, the span for the assert was:

        if (ack) begin>
          assert(data != 8'h0a)<;

After this commit, the span for the assert is:

        if (ack) begin
          >assert(data != 8'h0a)<;

This helps editor integrations that only look at the beginning
of the span.
2024-02-08 14:25:35 +00:00
Miodrag Milanović 5d3e4c5c7a
Merge pull request #4182 from QuantamHD/fix_aldff
verific: Improves aldff inference in verific importer
2024-02-06 08:19:43 +01:00
N. Engelhardt 2422dd6845
Merge pull request #4153 from Coloquinte/blif_delay_constraints
Issue a warning instead of a syntax error for blif delay constraints
2024-02-05 15:14:05 +01:00
Ethan Mahintorabi ff578ecabd
fix formatting
Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>
2024-02-05 07:23:04 +00:00
Ethan Mahintorabi bc66dfd9ea
verific: Fixes incorrect aldff inference in verific importer
The following SV module at HEAD imported with verific,

```systemverilog
    module my_module(
      input logic [4:0] a,
      input logic clk,
      input logic enable,
      output logic [4:0] z
    );

    reg [4:0] pipeline_register;
    always @(posedge clk) begin
      pipeline_register <= enable ? a : pipeline_register;
    end
    assign z = pipeline_register;

    endmodule : my_module

```

results in the following output verilog

```systemverilog
/* Generated by 0.36 */

(* top =  1  *)
(* hdlname = "my_module" *)
(* src = "/tmp/temp_directory_zTwd0l/my_input.v:2.12-2.21" *)
module my_module(clk, enable, a, z);
  wire [4:0] _0_;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:3.25-3.26" *)
  input [4:0] a;
  wire [4:0] a;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:4.19-4.22" *)
  input clk;
  wire clk;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:5.19-5.25" *)
  input enable;
  wire enable;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:6.26-6.27" *)
  output [4:0] z;
  wire [4:0] z;
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:10.12-12.8" *)
  \$aldff  #(
    .ALOAD_POLARITY(32'd1),
    .CLK_POLARITY(32'd1),
    .WIDTH(32'd5)
  ) _1_ (
    .AD(5'hxx),
    .ALOAD(1'h0),
    .CLK(clk),
    .D(_0_),
    .Q(z)
  );
  (* src = "/tmp/temp_directory_zTwd0l/my_input.v:11.28-11.58" *)
  \$mux  #(
    .WIDTH(32'd5)
  ) _2_ (
    .A(z),
    .B(a),
    .S(enable),
    .Y(_0_)
  );
endmodule
```

Yosys is incorrectly infering aldffs due to an incorrect conversion
of logical 1 and 0 SigBits.

My PR unifies the conversion of Verific::Net objects into SigBits using
Yosys' internal representation of special signals like 0,1,x,z. After
my PR these signals are correctly converted into DFFs.

Signed-off-by: Ethan Mahintorabi <ethanmoon@google.com>
2024-02-05 07:10:25 +00:00
Catherine c7bf0e3b8f Add new `$check` cell to represent assertions with a message. 2024-02-01 20:10:39 +01:00
Miodrag Milanovic db1de5fe5d verific: add option to skip simplifying complex ports 2024-01-30 16:33:44 +01:00
Gabriel Gouvine c634d59c18 Issue a warning instead of a syntax error for blif delay constraints 2024-01-23 16:25:16 +00:00
Miodrag Milanovic 1764c0ee3c Fix verific clocking when no driver exist 2024-01-18 08:47:04 +01:00
Martin Povišer 149bcd88ad
Merge pull request #4026 from uis246/fix-format
Fix printf formats
2024-01-15 16:04:11 +01:00
uis 5902b2826d Fix printf formats 2024-01-15 12:07:54 +01:00
Catherine 1159e48721 write_verilog: emit `initial $display` correctly. 2024-01-11 13:13:04 +01:00
Dag Lem 3ed9030eb4 Optionally suppress output from display system tasks in read_verilog 2024-01-11 13:12:53 +01:00
Jannis Harder 510d137996 fmt: Allow non-constant $display calls in initial blocks
These are useful for formal verification with SBY where they can be used
to display solver chosen `rand const reg` signals and signals derived
from those.

The previous error message for non-constant initial $display statements
is downgraded to a log message. Constant initial $display statements
will be shown both during elaboration and become part of the RTLIL so
that the `sim` output is complete.
2024-01-11 13:01:28 +01:00
Dag Lem 23cd23efc5 Simplify and correct AST for array slice assignment
Corrects sign extension of the right hand side, and hopefully
makes the code simpler to understand.

Fixes #4064
2024-01-10 21:15:00 +01:00
Dag Lem 1a2b4759e8 Assign from rvalue via temporary register in nowrshmsk CASE
Avoid repeating complex rvalue expressions for each condition.
2024-01-10 20:40:01 +01:00
Dag Lem 2cab4ff173 Correction and optimization of nowrshmsk
This makes tests/verilog/dynamic_range_lhs.v pass, after ensuring that
nowrshmsk is actually tested.

Stride is extracted from indexing of two-dimensional packed arrays and
variable slices on the form dst[i*stride +: width] = src, and is used
to optimize the generated CASE block.

Also uses less confusing variable names for indexing of lhs wires.
2024-01-10 20:28:36 +01:00
Dag Lem 1bbea13f80 Correct hierarchical path names for structs and unions 2024-01-04 17:22:07 +01:00
Martin Povišer 320e75a3e3
Merge pull request #4065 from daglem/fix-AST_SHIFT-AST_SHIFTX
Respect the sign of the right operand of AST_SHIFT and AST_SHIFTX
2023-12-12 11:47:29 +01:00
Dag Lem 655921e851 Uncloak array expressions generated by read_verilog -dump_vlog2
Explicit conversion of AST_TO_SIGNED, AST_TO_UNSIGNED, and AST_CAST_SIZE
makes it possible to reason about simplified array expressions.
2023-12-11 19:12:35 +01:00
Dag Lem cda470d63e Respect the sign of the right operand of AST_SHIFT and AST_SHIFTX
The $shift and $shiftx cells perform a left logical shift if the second
operand is negative. This change passes the sign of the second operand
of AST_SHIFT and AST_SHIFTX into $shift and $shiftx cells, respectively.
2023-12-11 18:58:34 +01:00
Miodrag Milanovic 96fecf0716 Revert "Add attributes to module instantiation"
This reverts commit 8f207eed1b.
2023-12-04 16:37:01 +01:00
Miodrag Milanovic 8f207eed1b Add attributes to module instantiation 2023-11-23 11:01:49 +01:00
N. Engelhardt 5fb1264db5 verific: don't try to import attributes from nullptr 2023-11-14 15:05:24 +01:00
N. Engelhardt 93a426cbbf
Merge pull request #4008 from nakengelhardt/mem_libmap_data_attr
memory_libmap: look for ram_style attributes on surrounding signals
2023-11-06 16:25:38 +01:00
Miodrag Milanovic f06d56d224 Handling non-existing location in verific logs 2023-11-03 08:06:16 +01:00
Miodrag Milanovic 4eb18e1f07 change verific log callback api 2023-11-01 08:13:27 +01:00
N. Engelhardt 833b67af80 verific: import attributes on ports
Co-authored-by: Miodrag Milanović <mmicko@gmail.com>
2023-10-20 18:31:41 +02:00
Miodrag Milanovic d473a207a1 Preserve VHDL architecture name in attribute 2023-10-12 09:17:06 +02:00
Jannis Harder 4ed708836a verific: Use CellBaseName to identify top modules 2023-10-10 11:51:16 +02:00
Martin Povišer 8367f06188 ast/simplify: Remove unused in_param code 2023-10-05 22:42:36 -04:00
Miodrag Milanović a54e6f2d1f
Merge pull request #3984 from YosysHQ/module_hdlname
verific: save original module name
2023-10-05 19:41:00 +02:00
Jannis Harder 47a4b790f8 verific: Pass top modules to static elaboration when using hierarchy 2023-10-05 16:51:49 +02:00
Jannis Harder 23b9e61c47 verific: Pass list of top modules to static elaboration 2023-10-05 16:51:49 +02:00
Miodrag Milanovic 268fe92d22 verific: save original module name 2023-10-05 11:22:40 +02:00
Jannis Harder 563a56d9ff verific: Improve interaction between -L, -work and bind statements 2023-10-03 15:52:01 +02:00
Jannis Harder cc843d414f simplify: Avoid calling fixup_hierarchy_flags on nullptr
Compiling on GCC hid this bug as it optimized the nullptr call away as
undefined behavior, but running the SBY tests with a clang build hits
this error.
2023-09-29 12:28:50 +02:00
Martin Povišer 20024900d9
Merge pull request #3813 from povik/ast-simplify-work-vol2
ast/simplify: Remove in_lvalue/in_param simplify() parameters
2023-09-28 11:57:58 +02:00
Miodrag Milanovic f193ebdded Verific: add default parameters to modules 2023-09-27 16:57:18 +02:00
Martin Povišer a511976b48 ast/simplify: Retire in_lvalue/in_param arguments to simplify 2023-09-26 13:32:15 +02:00
Martin Povišer 22b99413e8 ast/simplify: Make in_lvalue/in_param into props of AST nodes
Instead of passing around in_lvalue/in_param flags to simplify, we make
the flags into properties of the AST nodes themselves. After the tree
is first parsed, we once do

  ast->fixup_hierarchy_flags(true)

to walk the full hierarchy and set the flags to their initial correct
values. Then as long as one is using ->clone(), ->cloneInto() and the
AstNode constructor (with children passed to it) to modify the tree, the
flags will be kept in sync automatically. On the other hand if we are
modifying the children list of an existing node, we may need to call

  node->fixup_hierarchy_flags()

to do a localized fixup. That fixup will update the flags on the node's
children, and will propagate the change down the tree if necessary.

clone() doesn't always retain the flags of the subtree being cloned. It
will produce a tree with a consistent setting of the flags, but the
root doesn't have in_param/in_lvalue set unless it's intrinsic to the
type of node being cloned (e.g. AST_PARAMETER). cloneInto() will make
sure the cloned subtree has the flags consistent with the new placement
in a hierarchy.

Add asserts to make sure the old and new way of determining the flags
agree.
2023-09-26 13:32:15 +02:00
Martin Povišer 10d0e69588 ast/simplify: Make tweaks in advance of big in_lvalue/in_param change
The following commit will replace the way in_lvalue/in_param is being
tracked in the simplify code. Make tweaks in advance so that it will
be easier to make the old way and the new way agree.

These changes all should be innocuous.
2023-09-26 13:31:59 +02:00
Martin Povišer 99a5773911
Merge pull request #3920 from zachjs/asgn-expr
sv: support assignments within expressions
2023-09-20 11:30:14 +02:00
Miodrag Milanovic 18855f23ce Set src attribute for verific with full info 2023-09-19 12:00:10 +02:00
Zachary Snow 28e99f2b8c fix width of post-increment/decrement expressions 2023-09-18 23:46:06 -04:00
Zachary Snow 7d07615dee allow attributes in front of ++/-- statements 2023-09-18 23:46:02 -04:00
Jannis Harder 0e8a4adb59 verific: Update YOSYSHQ_VERIFIC_API_VERSION 2023-09-13 11:32:36 +02:00
Miodrag Milanovic 27ac912709 Support import of $future_ff 2023-09-13 11:32:36 +02:00
Miodrag Milanovic 9c255c98b1 unescape string tag attribute 2023-09-13 11:32:36 +02:00
Miodrag Milanovic 54050a8c16 Basic support for tag primitives 2023-09-13 11:32:36 +02:00
Miodrag Milanovic 7b134c2a8c verific - respect order of read and write for rams 2023-09-12 11:56:15 +02:00
Zachary Snow 4edb1a1921 sv: support assignments within expressions
- Add support for assignments within expressions, e.g., `x[y++] = z;` or
  `x = (y *= 2) - 1;`. The logic is handled entirely within the parser
  by injecting statements into the current procedural block.
- Add support for pre-increment/decrement statements, which are
  behaviorally equivalent to post-increment/decrement statements.
- Fix non-standard attribute position used for post-increment/decrement
  statements.
2023-09-05 22:27:55 -04:00
Martin Povišer 2d0fc040cf ast: Substitute rvalues when parsing out print arguments
Apply the local substitutions stemming from process context when parsing
out format arguments to `$display` or other statements.
2023-09-05 21:40:39 +02:00
Charlotte f9d38253c5 ast: add `PRIORITY` to `$print` cells 2023-08-11 04:46:52 +02:00
Charlotte 992a728ec7 tests: CXX may be e.g. gcc, so use CC and link stdc++ explicitly 2023-08-11 04:46:52 +02:00
Charlotte 9f9561379b fmt: format %t consistently at initial 2023-08-11 04:46:52 +02:00
Charlotte c382d7d3ac fmt: %t/$time support 2023-08-11 04:46:52 +02:00
whitequark d5c9953c09 ast: translate $display/$write tasks in always blocks to new $print cell. 2023-08-11 04:46:52 +02:00
whitequark 9f8e039a4b ast: use new format string helpers. 2023-08-11 04:46:52 +02:00
whitequark f8e2c955fc read_verilog: set location of AST_TCALL.
Useful for error reporting of $display() arguments, etc.
2023-08-11 04:46:52 +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
Zachary Snow d5d2bf815a Fix semantic merge conflict in previous two merged PRs 2023-07-21 00:08:10 -04:00
Martin Povišer 72a4022a10 ast/simplify: Retire 'at_zero' flag
Now that all the callsites pass in 'false' for the flag (or propagate
the flag on recursion), we can retire it.
2023-07-20 23:40:19 -04:00
Martin Povišer 4fceeb3b32 ast/simplify: Use clone_at_zero() for "at_zero" evaluations
The correct way of using the 'at_zero' regime of simplify is to perform
the simplification on a cloned AST subtree, otherwise the "at_zero"
evaluation seeps into the main tree.

Move the effect of the 'at_zero' flag to the cloning itself, so that
the simplify flag can be retired. We assume we can rely on id2ast in
the new clone method.
2023-07-20 23:40:19 -04:00
Martin Povišer 77d4b5230e ast: Move to a new helper method to print input errors
It's a repeating pattern to print an error message tied to an AST
node. Start using an 'input_error' helper for that. Among other
things this is beneficial in shortening the print lines, which tend
to be long.
2023-07-20 23:40:19 -04:00
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