HOME       UP       PREV       NEXT (Synthesis from Rules (SAT-based idea).)  

Refinement from a specification to implementation.

Conversion from specification to implementation can be done with a process known as selective stepwise refinement. This chips away at bits of the specification until, finally, it has all be converted to logic. Some example rules for the conversion are given earlier

There are a vast number of refinement rules available for application at each refinement step and the quality of the outcome is sensitive to early decisions. Therefore, it is hard to make this fully automated.

Perhaps a good approach is for much of the design to be specified algorithmically by the designer (as in the above work) but for the designer to leave gaps where he is confident that a refinement-based tool will fill them. These gaps are often left by designers in their first pass at a design anyway; or else they are filled with some approximate code that will allow the whole design to compile and which is heavily marked with comments to say that it is probably wrong. These critical bits of code are often the hardest to write and easiest to get wrong and are the bits that are most relevant to meeting the design specification. Practical examples are the handshake and glue logic for bus or network protocols.

Systems that can synthesise hardware from formal specifications are not in wide commercial use, but there is a good opportunity there and, in the long run, such systems will probably generate better designs than humans.

The synthesis system should allow a free mix of design specifications in many forms, including behavioural fragments and functional specifications. and only complain or fail when:


57: (C) 2012-18, DJ Greaves, University of Cambridge, Computer Laboratory.