Abstract: Hardware and software co-design is a designtechnique which delivers computer systems comprising hardware andsoftware components. A critical phase of the co-design process is todecompose a program into hardware and software. This paperproposes an algebraic partitioning algorithm whose correctness isverified in program algebra. The authors introduce a program analysisphase before program partitioning and develop a collection ofsyntax-based splitting rules. The former provides theinformation for moving operations from software to hardware andreducing the interaction between components, and the lattersupports a compositional approach to program partitioning.