Make the bhv wrapper formal-friendly

Created by: silabs-robin

1. In order to reach some PMA-related preconditions, it is necessary to have control over the PMA parameters to the core, and hence these were added to the wrapper so they can propagate from tb top level.

2. The interfaces used to pass payloads between pipeline stages, they have modports specifying i/o direction and cannot be implicitly connected (.*) to modports of incompatible type, and hence the assertion bindings were instead connected to the interface instances themselves (instead of to the portlist of a submodule).

I have tested this in formal and it both elaborates and runs without problem. I also tested it in core-v-verif and it works there too (as far as the self-checking can go without step-and-compare).