Skip to content

Add non-deterministic loop or for-loop with fixed no. of iterations #167

@ngernest

Description

@ngernest

(This is a summary of this Slack discussion)

Consider the Brave New World bug in #158. There should be a way for us to vary the no. of cycles in which we apply back pressure.

There are two options:

  1. Non-deterministic loop operator (akin to Kleene star)

Here, we non-deterministically choose the no. of loop iterations. Example:

fn recv<DUT: AXISManager>(
    out data: u32,
    out is_last: u1,
) {
    DUT.i_aresetn := 1'b1;         // Keep out of reset

    // we are free to signal ready or not, it does not matter until valid is asserted
    DUT.i_tready := X;


    // wait for valid data
    while(DUT.i_tvalid == 1'b0) {
        step();
    }

    // now we are allowed to stall for an arbitrary number of cycles as long
    // as we keep ready low
    DUT.i_tready := 1'b0;
    while(X) {
        // valid has to remain true even if we are stalling the transfer!
        assert_eq(DUT.i_tvalid, 1'b1);
        assert_eq(DUT.i_tdata, data);
        step();
    }
    // set ready to true for the final cycle
    DUT.i_tready := 1'b1;
    assert_eq(DUT.i_tvalid, 1'b1);
    assert_eq(DUT.i_tdata, data);

    // One cycle for the transfer to complete
    step();
}

This is challenging for users of the interpreter and the monitor since they have no way to control the no. of iterations in which back pressure is applied. This motivates the second approach:

  1. For-loop with a fixed no. of iterations

Here, we have an extra input parameter which fixes the no. of loop-iterating. The user of the interpreter needs to decide ahead of time the no. of loop iterations. On the other hand, the monitor needs to infer the value for this input parameter by forking two threads at each loop iteration (one thread executes the loop body while the other thread exits the loop) and seeing which thread succeeds. This would make the monitor implementation more complex (but would be simple to implement in the interpreter).

Example:

fn foo(..., in back_pressure_cycles: u8) { 
   ...
   for back_pressure_cycles iterations {
     ...
   }
}

Another potential issue in the monitor is if two threads succeeds, one which continues the loop body and one which exits the loop. In this case, we need a way to break ties. Kevin mentioned letting the thread which continues the loop body succeed since it allows for a more compact transaction trace (e.g. a fully combinational adder which maintains its inputs/outputs for 3 cycles, as opposed to 3 separate add transactions).

Metadata

Metadata

Assignees

No one assigned

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions