System factorization in codesign. A case study of the use of formal techniques to achieve hardware-software decomposition

A major element of codesign is the task of decomposing a design in order to target some of its components to hardware and some to software while maintaining the integrity of the execution model. We illustrate how a previously- developed algebraic technique which we call `system factorization´, adapts to this notion of decomposition. As an example, we describe how the mechanization of system factorization was used in the formal derivation of an implementation of Hunt´s (1992) FM9001 microprocessor description using the DDD (digital design derivation) system. This case study demonstrates the benefits to system-level design in combinational-reasoning systems, hardware synthesis tools, and a hardware development platform in an integrated prototyping environment