The authors propose to use a formal specification language as a high-level hardware description language. Formal languages allow for compact, unambiguous representations and yield designs that are correct by construction. The idea of automatic synthesis from specifications is old, but used to be completely impractical. Recently, great strides towards efficient synthesis from specifications have been made. In this paper, they extend these recent methods to generate compact circuits and they show their practicality by synthesizing an arbiter for ARM's AMBA AHB bus and a generalized buffer from specifications given in PSL.