An approach to hardware/software co-design and verification is presented. Hardware and software are modeled with the Specification PEARL language, which has its origins in standard Multiprocessor PEARL. Its usefulness has been enhanced for hierarchical and asymmetrical multiprocessor system modeling, and by additional parameters for schedulability analysis. It is meant to be a super-layer for programs, based on the PEARL program model. For detailed program modeling Timed State Transition Diagrams are used. The model of a co-designed system is checked for feasibility with co-simulation. The resulting information should be used for changes in the current design. After that the program model can be enhanced to its full functionality for schedulability analysis to provide the designer with more precise timing information, which may be used for fine-tuning the system design. By utilising this methodology the possibility of implementing a temporally infeasible system should be minimised.