The debate about efficient methods for hardware-software co-design has taken interesting turns over the years. In this paper, we argue that the essential problems to solve are prior to the decision on how to partition the system in hardware-software. We present a formal platform-based design method we have proposed over the years and a design environment, Metropolis, supporting the methodology, which starts by capturing the design specifications at the highest level of abstraction and then proceed toward an efficient implementation by subsequent refinement steps. We present the modeling strategy used in Metropolis based on formal semantics that is general enough to support the models of computation proposed so far and that facilitates the creation of new ones. Nonfunctional and declarative constraints can also be captured using a logic language.