Conversion from specification to implementation can be done with a process known as selective 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, fully automated techniques for this fail with anything other than trivial example designs. (This last sentence is only the author's conjecture, but he will dig up some hard evidence soon, perhaps).
It seems that a better 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. An example might be the handshake logic for a bus or network protocol.
An alternative to refinement is searching over all possible designs. This is feasible for tiny designs with just a few nets and gates, but also it is feasible as a method of stitching together a few components at a higher-level of abstraction. Hence it might be feasible in general. Recently, so-called symbolic methods have matured, where instead of explicitly searching over all possible designs, the computer searches over a symbolic representation of the design's behaviour (such as its next state function). Symbolic methods exponentiate the size of design that can be handled.
Systems which can synthesise hardware from formal specifications are not in wide commercial use, but there is a good market opportunity there and, in the long run, such systems will probably generate better designs than humans.
A final goal will be to freely mix design specifications in many forms, including functional and formal specifications. The synthesis system should basically only complain under the following situations: