查看文章

A crucial point in hardware/software co-design is how to perform the partitioning of a system into hardware and software components. Although several algorithms to partitioning have been recently proposed, the formal verification of the partitioning procedure is an emergent research topic. In this paper we present an innovative and automatic approach to partitioning with emphasis on correctness. The formalism used is occam and the algebraic laws that define its semantics. In the proposed approach, the partitioning procedure is characterised as a program transformation task and the partitioned system is derived from the original description of the system by applying transformation rules, all of them proved from the basic laws of occam. A tool has been developed to allow the partitioning to be carried out automatically. The entire approach is illustrated here through a small case study.