Controller Synthesis and Verification

This chapter focuses on synthesis and verification of control units. One of the key issues in synthesis is the ability to explore the design space. One step toward design space exploration is the results presented here in control architecture synthesis that enables exploration of a range of control architectures. Another step is the use of a compiled cell approach to the technology mapping problem in control unit logic synthesis. The verification of the synthesized control unit is also an important issue. A new approach is presented that, using a combination of propositional temporal logic verifier and sequential logic extraction, has made it possible to verify formally the layout of a control unit against the specification.