The hardware-software codesign space exploration process is formalized
through a theoretic model based on Linear Hybrid Automata.
This formalization not only allows rigorous synthesis, but also produces
verifiable designs. Parallelism in hardware and in software are
modeled and explored. Design choices occurring in hardware-software
interfaces are investigated. Finally, a metric-based selection procedure
for codesign alternatives is also proposed.