Skip to content

[enhancement] Short-circuiting in DSLX logical expressions #3150

@mikex-oss

Description

@mikex-oss

What's hard to do? (limit 100 words)

The DSLX interpreter does not support short-circuiting, meaning you can't write if p && <expr that's only valid if p>.

Note that SystemVerilog does use short-circuit evaluation for &&, ||, ->, and ? : (see section 11.3.5 of the SystemVerilog LRM - screenshoted below) so this can be surprising to both software and hardware engineers.

Image

Silly example:

fn muladd(a: u8, b: u8, c: u8) -> u8 {
    let arr = for (i, arr) in u32:0..u32:10 {
      let val = if i > u32:0 && arr[i - u32:1] != u8:0 {
         arr[i - u32:1]
      } else {
        a * b + c
      };
      update(arr, i, val)
    }(zero!<u8[10]>());
    arr[0]
}

In if i > u32:0 && arr[i - u32:1] != u8:0, the RHS of the && is evaluated for i = 0 and the index wraps around, causing the following error:

INVALID_ARGUMENT: Index out of bounds; index: 4294967295 >= 10 elements; lhs: [u8:0, u8:0, u8:0, u8:0, u8:0, u8:0, u8:0, u8:0, u8:0, u8:0];

@ericastor argued that the real bug is in the array indexing. That's true, and I've separately reported in #3146, but I think there is still a case for the general short-circuiting behavior in DSLX.

One concern is with short-circuiting side-effecting ops, e.g. asserts. We'll need to address the activation bit to properly handle this if moving forward with this proposal.

Current best alternative workaround (limit 100 words)

Instead of relying on short-circuiting, you can equivalently write the following using an outer mux and not get any interpreter error:

fn muladd(a: u8, b: u8, c: u8) -> u8 {
    let arr = for (i, arr) in u32:0..u32:10 {
      let composite_predicate_result = if i > u32:0 {
        arr[i - u32:1] != u8:0
      } else {
        false
      };
      let val = if composite_predicate_result {
         arr[i - u32:1]
      } else {
        a * b + c
      };
      update(arr, i, val)
    }(zero!<u8[10]>());
    arr[0]
}

An alternative workaround is to factor out the dependency in a separate accumulator element so the secondary predicate is not coupled.

fn muladd(a: u8, b: u8, c: u8) -> u8 {
    let (arr, _) = for (i, (arr, prev)) in u32:0..u32:10 {
      let val = if i > u32:0 && prev != u8:0 {
         arr[i - u32:1]
      } else {
        a * b + c
      };
      (update(arr, i, val), val)
    }(zero!<(u8[10], u8)>());
    arr[0]
}

Your view of the "best case XLS enhancement" (limit 100 words)

Allow the more compact inlined composite predicate that relies on short-circuiting to evaluate without errors.

If non-short circuiting is desired by the user, you can use the bitwise & operator as in SystemVerilog and software languages like C++.

cc: @allight @grebe @hongted who participated in an offline discussion.

Metadata

Metadata

Assignees

No one assigned

    Labels

    dslxDSLX (domain specific language) implementation / front-endenhancementNew feature or request

    Projects

    Status

    No status

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions