-
-
Notifications
You must be signed in to change notification settings - Fork 76
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Support finite-state-machine coverage #763
Comments
thanks for hints :) Basically everything you said is correct. I was thinking about implementing this when I was doing first coverage implementation. I did some "research" about FSM extraction, and I ended up leaving the idea since it was quite complex.
This one should be pretty easy to implement. Simply by tracking if all possible enum values of "signal" / "variable" were visited.
It could even work with reversed logic. Consider all enums as FSMs unless there is a meta-comment that marks the signal as "not an FSM". Or some option like As for the coverage type, I would split it from expression coverage to separate FSM coverage (or FSM state coverage). Implementation-wise, there might be a limit on number of states that can be supported. I am not sure whether it is not the case now with enum itself.
This is more tricky. You can google so many articles on the FSM extraction topic. AFAIK, simulator/synthesizer tool vendors do have it, but it never works 100 % (or close to it) for different FSM coding styles. To do it correctly, one needs to synthesize the FSM as you have shown. I also think the Aldec approach here is tricky. The meta-code in the comment that defines the valid transitions is quite complex, there is whole "grammar" involved with it. Once the FSM changes, you need to update the code I have seen a company, where design and test-bench repository were split, and designer did not have write access to TB repository and vice-versa for the verification guy. This was some sort of process to guarantee that "the code is tested by someone else than by its designer". Altough it may be crazy, I would not want to be a verification engineer who can't write
Yup agreed, I think we can start dealing with this once we have the first two types working well. This is basically a cyclomatic coverage that tracks how is FSM "traversed" from "IDLE" state to its final state.
This is also quite tricky. I know some designers implement VHDL FSMs via |
One way could be to extend the exclude file format to something like
although maybe there should be a version of the above which acts on the enum type itself, in the case where the enum is never a state variable.
I think the easiest way for this is to only include signals assigned in clocked processes by default. Although this gets close to detecting state machines. However, I think we could get pretty far with just a simple heuristic like looking for
Yes, I agree.
I think the limit right now is 2**32. But a lower heuristic cutoff like 256 might be more appropriate.
This is why I think it might be better to just support PSL for this area, as PSL already has a grammar which can express these relationships. I believe something like -- Aldec enum fsm_enc CURRENT = state
-- Aldec enum fsm_enc STATES = A, B
-- Aldec enum fsm_enc TRANS = A -> B, B -> A could be expressed in PSL as cover { state = A; state = B };
cover { state = B; state = A }; and of course you could also do state coverage manually with something like cover { state = A };
cover { state = B };
Yes, I am not really a fan of this, since most other forms of coverage are "automatic." But it's unavoidable if you view coverage as a test for the testbench and the module. If you don't care about that, then branch coverage is good enough.
Well, as I understand it, things like
IMO the encoding used is really up to your synthesis tool. Most synthesis tools support recoding state machines (so your type state_t is (Uninitialized, ...);
-- ...
case state is
-- ...
when Uninitialized =>
my_output <= (others => 'X');
end case; but this is of course a bit error prone, and will probably mess with your synthesizer. (One other feature I would love to see would be better (non-standard) X propagation options, but that's a wish for another issue). Back to the point, I think initially we just shouldn't support On the other hand, adding assertions against invalid state transitions would probably be much more verbose than if they were calculated automatically. |
OK, to illustrate the PSL point a bit further, type state_t is (
IDLE,
START,
DATA,
STOP,
ERR
);
signal state: state_t;
type trans_t is array (state_t, state_t) of boolean;
function gen_transitions return trans_t is
variable valid: trans_t;
begin
for s in state_t loop
valid(s, s) := true;
end loop;
valid(IDLE, START) := true;
valid(START, IDLE) := true;
valid(START, DATA) := true;
valid(DATA, STOP) := true;
valid(STOP, IDLE) := true;
valid(STOP, ERR) := true;
valid(ERR, IDLE) := true;
return valid;
end;
constant valid: trans_t := gen_transitions;
-- ...
for_from: for state_from in state_t generate begin
for_to: for state_to in state_t generate begin
check: if valid(state_from, state_to) generate
cover { state = state_from; state = state_to };
else generate
assert never { state = state_from; state = state_to };
end generate;
end generate;
end generate; And now you have cover/asserts for all the valid/invalid transitions. This technique can be used with GHDL using It's more verbose than the Aldec DSL, but I think the generate loops can be abstracted away to be reused when necessary. |
Yup, thanks, understood. I like the idea of emulating FSM transition tracking by PSL sequences. One thing that would need to be taken care of, is then filtering of the dummy added PSL assertions so that they don't show up in the functional coverage reports. Also, the PSL support is very early state and I don't know what are @nickg plans in this regard. If you follow the discussion in the PSL issue, I think it is not a priority now. As for the FSM state tracking, I think a PSL cover point would not even be needed. I think it would suffice to emit code for an additional "process" during lower phase. There would be a run-time data (similar to coverage counters), whose each bit would keep track of a state visited (lets.call it RT_STATE_VECT). The emited code would correspond to something like:
The slightly tricky part might be in long enums that have more states than number of bits in the I think the addressing logic (selecting the word and also the bit) may even not need a case in the emited code. Since enum values are numbered from 0 in the generated code, pseudo-code will look something like this (assuming
I dare to say that this should be doable with the current API of VCODE and its simpler than emmiting additional PSL cover point. @nickg what do you think? |
It supports some basic FL operators but not much else. Recently I've been focussing on adding VHDL-2019 support but that is mostly(?) done now.
I think you could do that with the existing coverage counters which are just an array of 32-bit integers that you treat as a bit mask. |
Thinking about this again, I think emitting extra process as described above is too complex. Simpler way to achieve the same is to use callback on the FSM state signal. Then the implementation will be very similar to toggle coverage that is already implemented. |
I'am trying to give a shot at implementing this. To handle enums with arbitrary number of literals, I need to either emit multiple cover tags to track single FSM, or rework the |
I would rather keep it as a flat array. I think you can just allocate N/32 sequential tags and then refer to them by the index of the first one. |
If we want to solve the #564, we need to be able to insert a tag into the middle of array once a tag that does not exist in first The current way of accessing an element of tag array is either accessing last element, or accessing i-th element when iterating all elements. Both of these as well as inserting new element can be done effectively with singly linked list. Drawback is heap allocations for each tag, current array always allocates in "batch".
Yup, that is what I tried to do in: Blebowski@3cce18d. Wouldn't it be better to put The size of the allocated array in the run-time code would differ from number of tags, so "tag-index" in the array would no longer be offset into the run-time data, but I don't think that would mind too much... |
OK, I see now that you changed the tag array not to be flat accross the whole design, but only across the current cover scope in: Was the intention to solve the problem of above? WIth this new implementation, I think it could be sufficient to simply append the "new" tag to the most common scope. |
I did that because code gets generated on-demand now rather than all at once when you call The name |
OK, I see. Anyway, it helps also with the merging/inserting. If the tag from second
OK. I would choose
|
@sean-anderson-seco I have implemented the basic FSM coverage, @nickg just merged it. It only tracks FSM state coverage, and NVC considers signals of all user defined enums as FSMs. As for other types of FSM coverage, it requires much more elaborate implementation of FSM detection
@nickg , what do you think about it? For me, it seems a lot of complexity, and I don't really dare to try to do that now. I do think the feature |
Looks good :) |
Hello @sean-anderson-seco , do you think it is OK to close this issue, or would you like to keep it open as a TODO for the transition coverage? |
I am working on a project with coverage requirements, and one of those requirements is for "FSM coverage." This is rather nebulously defined, but from what I can tell it refers to the following set of features:
when STATE7 downto STATE0
can be covered with only two transitions). Second, the transitions can be specified "out-of-band" by some other method (such as a DSL in comments or PSL). In the latter case, this is a sort of specialized toggle coverage.std_logic_vector
instead of an enum), and invalid state transitions. This is not really coverage, but is often considered part of FSM coverage, since it can be easily implemented once valid states and transitions are known.There are several approaches for implementing this feature:
default
cases. However I think exclude files can be used to ignore such cases. This would not handle non-enum state variables, but it could be possible to add some kind of annotation/comment to cover them. It could also be possible to automatically detect state variables and extract the states, such as what is done in synthesis (ex1, ex2), but that is probably unnecessary for an initial attempt.cover
andcovergroup
directives in PSL, which can be used to implement FSM coverage (ex1, ex2). This depends on PSL support #455, but is a much more flexible approach to adding new coverage types, since arbitrary expressions can covered.I'm not going to need this feature for a while, and I don't plan on working on it in the near future. So this should be considered more of a wishlist idea. However, I've been pretty happy with the existing coverage, and I would love to avoid buying a commercial simulator just to get one specific type of coverage.
[1] Behind a login, but you can see some examples here and here.
The text was updated successfully, but these errors were encountered: