A problem I see with bind is if you have a larger test framework with a big hierarchy of modules. You then need to maintain a list of all the SVA modules to bind to in the various testbenches, and it seems easy to miss something. For example, let’s say you add a submodule to the counter module with its own SVA bindfile. You then need to update all the testbenches that use counter somewhere in the hierarchy with a new bind directive. With `include, you guarantee that you don’t miss any assertions.
Furthermore, you have another layer of maintenance whenever you add/remove ports or parameters to the module you bind to. With ports this can be done automatically with the .* notation, but this is not available for parameters, so if you add a WIDTH parameter to counter, you need to update the binds in all testbenches with #(.WIDTH(WIDTH)). With `include, added parameters will automatically be available in the assertions file, and it is guaranteed that there are no mismatches between the parameter in the module and the bind file.
If you surround include* with something like *ifdef SIMULATION, it seems to me that you cover all the items in your list of benefits for using bind. Any comments on this?