SVA, counter with features and formal verification

In reply to cool_cake20:

Thanks for the interesting suggestion. It’s basically a mux inside sequence? Anyway, it does not seem to compute :(

illegal inc/dec operator in sva; only allowed in sequence match items

Also on problem seems to be that EN has be ‘1’ all the time. Otherwise in the design the counters will obviously be reset. I’ve been trying to use “EN throughout ((FOO, count++)[=100)” type of a solution but the tools do not seem to like clk tick “unbounded” sequences with local variables…I then tried “EN[*200] intersect ((FOO, count++)[=100)” but again this seems to be illegal use of local variables.