While I agree that having assertions directly in the design is nice, using `include seems like a good option because it pretty much covers all the benefits of the bindfiles, without the following drawbacks:
- Maintenance burden on bind statements in all testbenches. Risk of missing assertion files.
- Maintenance burden of parameter associations in all testbenches. Risk of mismatch between bindfile parameters and RTL parameters.
- Inability to add assertions in SV interfaces. (?)
- Extra coding overhead with parameter/port list in bindfiles and bind statements in testbenches
You could also make a custom macro that has an ifdef SIMULATION and/or synth_off pragmas around the include statement.
Timestamp of design
If you use `include, the assertion files will not be part of the synthesis makefiles, so adding an assertion will not affect the build system.
Need of pragmas
The bindfiles can import/refer to packages and their subroutines. For risks with synth_off, the solution with the custom assertion file include macro seems safe to me.
Verification of assertions
This is no problem with include. You can simply make a testbench that has all the signals used by the assertions, then include the assertion file in your testbench.
Code review complexity
If you use `include, the assertion code in the RTL will only be a single line of code. I don’t see this as a burden for reviews.