article published yes Yashdeep Godhal author 5B547124-EB61-11E9-8887-89D9C04DBDF5 Krishnendu Chatterjee author 2E5DCA20-F248-11E8-B48F-1D18A9856A870000-0002-4561-241X Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000−0002−2985−7724 KrCh department ToHe department Rigorous Systems Engineering project Microsoft Research Faculty Fellowship project The standard hardware design flow involves: (a) design of an integrated circuit using a hardware description language, (b) extensive functional and formal verification, and (c) logical synthesis. However, the above-mentioned processes consume significant effort and time. An alternative approach is to use a formal specification language as a high-level hardware description language and synthesize hardware from formal specifications. Our work is a case study of the synthesis of the widely and industrially used AMBA AHB protocol from formal specifications. Bloem et al. presented the first formal specifications for the AMBA AHB Arbiter and synthesized the AHB Arbiter circuit. However, in the first formal specification some important assumptions were missing. Our contributions are as follows: (a) We present detailed formal specifications for the AHB Arbiter incorporating the missing details, and obtain significant improvements in the synthesis results (both with respect to the number of gates in the synthesized circuit and with respect to the time taken to synthesize the circuit), and (b) we present formal specifications to generate compact circuits for the remaining two main components of AMBA AHB, namely, AHB Master and AHB Slave. Thus with systematic description we are able to automatically and completely synthesize an important and widely used industrial protocol. https://research-explorer.ista.ac.at/download/2299/4910/IST-2012-87-v1+1_Synthesis_of_AMBA_AHB_from_formal_specifications-_A_case_study.pdf application/pdfno Springer2013 eng 10.1007/s10009-011-0207-9 155-6585 - 601 Godhal Y, Chatterjee K, Henzinger TA. Synthesis of AMBA AHB from formal specification: A case study. <i>International Journal on Software Tools for Technology Transfer</i>. 2013;15(5-6):585-601. doi:<a href="https://doi.org/10.1007/s10009-011-0207-9">10.1007/s10009-011-0207-9</a> Y. Godhal, K. Chatterjee, and T. A. Henzinger, “Synthesis of AMBA AHB from formal specification: A case study,” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 15, no. 5–6. Springer, pp. 585–601, 2013. Godhal, Yashdeep, et al. “Synthesis of AMBA AHB from Formal Specification: A Case Study.” <i>International Journal on Software Tools for Technology Transfer</i>, vol. 15, no. 5–6, Springer, 2013, pp. 585–601, doi:<a href="https://doi.org/10.1007/s10009-011-0207-9">10.1007/s10009-011-0207-9</a>. Y. Godhal, K. Chatterjee, T.A. Henzinger, International Journal on Software Tools for Technology Transfer 15 (2013) 585–601. Godhal Y, Chatterjee K, Henzinger TA. 2013. Synthesis of AMBA AHB from formal specification: A case study. International Journal on Software Tools for Technology Transfer. 15(5–6), 585–601. Godhal, Y., Chatterjee, K., &#38; Henzinger, T. A. (2013). Synthesis of AMBA AHB from formal specification: A case study. <i>International Journal on Software Tools for Technology Transfer</i>. Springer. <a href="https://doi.org/10.1007/s10009-011-0207-9">https://doi.org/10.1007/s10009-011-0207-9</a> Godhal, Yashdeep, Krishnendu Chatterjee, and Thomas A Henzinger. “Synthesis of AMBA AHB from Formal Specification: A Case Study.” <i>International Journal on Software Tools for Technology Transfer</i>. Springer, 2013. <a href="https://doi.org/10.1007/s10009-011-0207-9">https://doi.org/10.1007/s10009-011-0207-9</a>. 22992018-12-11T11:56:51Z2024-10-09T20:55:16Z