Specify, Compile, Run: Hardware from PSL

We 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 we extend these recent methods to generate compact circuits and we show their practicality by synthesizing a generalized buffer and an arbiter for ARM’s AMBA AHB bus from specifications given in PSL. These are the first industrial examples that have been synthesized automatically from their specifications. Key words: temporal logic, synthesis, games, binary decision diagrams

• Type: Journal
• Year: 2007
• Where: ENTCS
• Authors: Roderick Bloem, Stefan Galler, Barbara Jobstmann, Nir Piterman, Amir Pnueli, Martin Weiglhofer
• Keywords: ARM’s AMBA AHB, Automatic Synthesis, ENTCS 2007, Formal Specification Language