This paper presents methodology and tools developed for the EGOS project. The main contributions of this project in hardware/software codesign include formal specifications of a system and hardware/software partitioning. By refinement, an acyclic graph is deduced from the formal specifications of the system, and this graph is the entry point of partitioning algorithms. The EGOS framework provides two partitioning algorithms selected according to the complexity of the system. The first one is exhaustive and is adapted to small systems. The second one lets the designer specify the trade-off between the heuristic execution time and the solution quality. Moreover, the partitioning methodology takes into account the impact of communication and includes communication constraints. Graphical tools are briefly described that facilitate the codesign process.