Synthesis from Declarative Specifications

Rather than specify the algorithm (behaviour) we specify the required outcome.

Rather like constraint-based linear programming, the design is a piece of hardware that satisifes a number of simultaneous assertions.

Examples covered:

• Refinement Synthesis from Formal Specs,
• Rule-based hardware generation (BlueSpec),
• SAT-based logic Synthesis,
• Automatic Synthesis of Transactors and Bus Monitors (in additional materials),
• Automatic Synthesis of Glue and Interface Automata (in additional materials).