Design transformations for system level models

The complexity of current digital designs is increasing the pressure on designers to move from RTL to higher levels of abstraction. This pressure is only compounded by the shrinking time allotted to development cycle as well as the demands of hardware/software codesign and design space exploration that are more and more becoming common place in the typical design flow. While formal verification tools, either combinational or sequential, have contributed to significant advances in the block level verification of designs they do not yet scale well to the system level. As such simulation-based verification is still a cornerstone of design verification.;This thesis will present our research into identifying design transformations that can help expose the parallelism often present in system level software models of hardware designs with the goal of improving the simulation performance of their respective software models. Initial experiments, where designs were manually transformed, have shown that such a goal is achievable if the models are restructured in a way that often times goes against the structure imposed by the modeling language. For such transformations to have practical applicability we needed algorithms to analyze, and transform such designs automatically. Since the transformations often result in significant changes to this description we also needed a formal proof of correctness for these transformations for designers to feel comfortable with the results obtained. Towards this goal that end we have investigated several formal models and devised an approach based on Petri nets. A set of transformations was initially developed for a restricted class of Petri nets that performed the desired structural changes on the designs with formal proofs also developed for each of the transformations. With this better understanding of the structural properties of the Petri nets obtained during the proof process, we relax most of the restrictions on the initial class of Petri nets thus ensuring their applicability to a much wider class of designs. The same structural knowledge has also allowed us to significantly improve the complexity of the transformation algorithms.;We demonstrate the efficiency and impact of these transformations on simulation performance on a suite of testcases written in SystemC.