How to use Shared Variable

I no longer have access to JG - it was temporary.

Protected types are VHDL 2002, not 2008. So should work with JG.

From my JG training - AUX code is a necessity. But anything that prevents separate threads being needed is what you have to do for formal. JG doesnt really support anything clever in asserts - otherwise the prove time just explodes. Aux code also increases the State space, so making it non-synthesisable probably wont really work with JG. All AUX code I have seen for JG was basically synthesisable verilog (Ive only worked with SVA).