Sequential-system factorization
Kamlesh Rath · 1995
The success of high-level synthesis methods in reducing design time and formal verification methods in reducing design errors in digital VLSI circuits have opened the way to system-level synthesis and verification. Derivation is a form of formal verification that deals with correct-by-construction reasoning. A set of equivalence preserving transformations are used to derive an implementation from a specification. A key step in derivation is to impose an architectural structure on a behavioral specification by factoring functional behavior into abstract components [40]. These system factorization transformations impose a naive model for synchronization and data communication between components in a system. The thesis of this work is that system factorization must be generalized to support arbitrary interaction protocols between components in a system for derivational methodology to be useful in system-level design. This dissertation develops a general transformation to decompose a seque...