I choose here the CoFluent Studio example because this is something I know. However, I think the described process can be at least partially applied to other SystemC-based design flows. I will just talk about the usual test bench verification here, formal verification is another problem.
CoFluent Studio can be used to model test benches enabling verification at system-level for CoFluent models themselves (the abstraction level is Message Level Model / Transaction Level Model), but also for external models at different abstraction levels. The generated output SystemC model can be connected without major modification to a virtual platform model (usually TLM or slightly lower level) and even to RTL models using transactors (as done in most SystemC-based methodologies). Thus, the verification across the design process is always operated with the same test bench. Of course, transactor design is still a necessary effort, although in most cases it should not be difficult to automate transactor code generation.

One of the interesting points you mentioned is the separate of concerns between function and architecture. In CoFluent Studio, functional and platform models are separated. An architectural model can be created by mapping the different functions onto computation resources of the platform, functional relations onto memories, buses and so on. The platform model can be seen as a set of constraints applied to the functional model through mapping operation. Thus, the test bench designed for functional verification can become an architectural verification test bench through mapping operation. I think it is the only time in the design flow at which is needed to modify the test bench: I mean the step from an untimed or partially timed model to a timed "golden model" used as a specification during the design flow.

Thanks for the comment George. I would like to clarify what I meant by "TLM standards are for verification and not for synthesis." If we consider the OSCI TLM 1.0 and TLM 2.0 standards, they have been constructed specifically with verification in mind. Many of the features in these are not synthesizable by any of the tools on the market today and it is unlikely that some constructs ever will be. So a synthesizable subset has to be created before they can be freely interchanged. At the same time, these standards do not include some of the constructs necessary for synthesis, such as resets - so the standards have to be extended for use in a synthesis flow.

Brian,

With respect to abstraction, verification has definitely led synthesis. In that dimension, ESL synthesis and ESL verification are often completely different animals -- and ESL synthesis can raise the fundamental question as to whether ESL is an abstraction or just a language syntax.

Abstractions should be relevant regardless of use model. You mentioned how TLM standards are for verification, not for synthesis. But, why not use them for synthesis as well? Designs can benefit from TLM concepts as well. At Bluespec, TLM can be used for designs, models and verification -- and they are synthesizable in all of these contexts.

And, we're also synthesizing verification IP, whether it be models, transactors or test benches. We just posted a new technical white paper covering just this on our website (http://www.bluespec.com/synthesizable-test-bench.htm) entitled:

Delivering Synthesizable Verification IP for Test Benches
Case Study: SystemVerilog VMM vs. BSV for an Ethernet MAC test bench

In the case study, the synthesizable BSV-based test bench is about 40% fewer lines of code than the non-synthesizable SystemVerilog VMM-based one for comparable functionality. (BSV is used for design implementations as well, whether they be datapath, control or system interconnect -- abstraction should be delivered regardless of use model.)

When people work in FPGA/emulation environments, the verification abstractions that they use should still remain relevant. High-level concepts such as TLM and modern, high-level programming language features should be usable in the synthesis world as well.