MicroTESK

For attached code six (6) code paths are produced:
1: L1.Event=MISS, L2.Event=MISS, pmem.condition=0, pmem.dependent!=1, pmem.STOP
2: L1.Event=MISS, L2.Event=MISS, pmem.condition=0, pmem.dependent=1, pmem.STOP
3: L1.Event=MISS, L2.Event=MISS, pmem.condition!=0, pmem.dependent!=1, pmem.STOP
4: L1.Event=MISS, L2.Event=MISS, pmem.condition!=0, pmem.dependent=1, pmem.STOP
5: L1.Event=MISS, L2.Event=HIT, pmem.STOP
6: L1.Event=HIT, pmem.STOP

None of them being pruned with isFeasible() check while paths 2 and 3 are infeasible.

  read = {
    l1Tag = va.vaddress<47..12>;
    l2Tag = va.vaddress<47..17>;

    if L1(va).hit then
      l1Entry = L1(va);
      line = l1Entry.DATA;
    else
      if L2(va).hit then
        l2Entry = L2(va);
        line = l2Entry.DATA;

        // Fill L1.
        l1Entry.TAG = l1Tag;
        l1Entry.DATA = line;
        L1(va) = l1Entry;
      else
        pa.addrdesc.paddress.physicaladdress<1..0> = 0b00;
        tempValue = MEM(pa);
        line<(64 * 0 + 63)..(64 * 0)> = tempValue;
        pa.addrdesc.paddress.physicaladdress<1..0> = 0b01;
        tempValue = MEM(pa);
        line<(64 * 1 + 63)..(64 * 1)> = tempValue;
        pa.addrdesc.paddress.physicaladdress<1..0> = 0b10;
        tempValue = MEM(pa);
        line<(64 * 2 + 63)..(64 * 2)> = tempValue;
        pa.addrdesc.paddress.physicaladdress<1..0> = 0b11;
        tempValue = MEM(pa);
        line<(64 * 3 + 63)..(64 * 3)> = tempValue;

        // Fill L2.
        l2Entry.TAG = l2Tag;
        l2Entry.DATA = line;
        L2(va) = l2Entry;

        // Fill L1.
        l1Entry.TAG = l1Tag;
        l1Entry.DATA = line;
        L1(va) = l1Entry;

        if condition != 0 then
          dependent = 1;
        else
          dependent = 0;
        endif;

        if dependent == 1 then
          temp.value = 0;
        endif;
      endif;
    endif;

    data = line<(64 * va.vaddress<4..3> + 63)..(64 * va.vaddress<4..3>)>;
  }