nickg / nvc

VHDL compiler and simulator
https://www.nickg.me.uk/nvc/
GNU General Public License v3.0
636 stars 80 forks source link

PSL SERE repetition #1053

Closed Blebowski closed 2 weeks ago

Blebowski commented 3 weeks ago

Hi,

this is a WIP of sequence repetition, not yet ready to be merged.

I would like to discuss how to proceed with the FSM generation. Consider the example below:

-- psl cov_1 : cover {a;b}[*2 to 3] report "COVER HIT!";

The current code leads to FSM like so: image

State 1 serves as skip condition when minimal required number of repetitions were already met. In state 8, I would need to:

Both of these are un-guarded. I create 8 -> 9 edge during "repeat" part, so it is not guarded since checking of "third" repetition is by guard on epsilon 9 -> 10.

The psl_lower_state fires an assert, since I have two "default" edges, one EDGE_NEXT and one EDGE_EPSILON.

I need to activate both 1 and 9 from 8, so "branch" the FSM traverse. AFAICT, the psl_lower_state generates code in if-elsif-else manner, making sure only one transition is activated.

I think the behavior could be:

I think the branching behavior will be needed also for some of the other SERE logic (within or &&).

Maybe some of the PSL syntax will require also multiple activated EDGE_EPSILON. But since this is done with emit_jump, it would require more complex logic (some sort of call). Anyway, this is now not needed, only the points above.

Let me know what do you think. Btw. thanks for all the effort in the recent weeks.

nickg commented 3 weeks ago

I think the behavior could be:

* All `EDGE_NEXT` edges that have guard are activated if the guard is 1 (instead of the first one matching)

* If `EDGE_NEXT` has no guard, it is always activated.

* `EDGE_EPSILON` will behave as till now (activated in `if-else-if` manner, there can be only one default `EDGE_EPSILON`).

Yeah I think something like this will work. I was planning to add FL and soon which also needs this.

Blebowski commented 3 weeks ago

I have implemented this change. The tracking of "vanishing FSM state" is now done in run-time code since code path with psl_enter_state does not call emit_return anymore. Thus psl_enter_state falls-through to the assertion checking that sequence is not met.

Implements full consecutive repetition of PSL sequences. An open-ended repetition with inf is supported by FSM looping to "last but one" repetition of the sequence.

The MR is now ready for review.