NEXT (Synthesis from Formal Specification)
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.
- 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).