Abstract
We present the tool ANZU. ANZU takes a formal specification of a design and generates a functionally correct system if one exists. The specification is given as a set of linear temporal logic (LTL) formulas belonging to the class of generalized reactivity of rank 1. Such formulas cover the majority of the formulas used in practice. ANZU is an implementation of the symbolic reactive(l) approach to synthesis by Piterman, Pnueli, and Sa'ar. If the specification is realizable ANZU provides the user with a Verilog module that represents a correct finite-state system. © Springer-Verlag Berlin Heidelberg 2007.
Cite
CITATION STYLE
Jobstmann, B., Galler, S., Weiglhofer, M., & Bloem, R. (2007). Anzu: A tool for property synthesis. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4590 LNCS, pp. 258–262). Springer Verlag. https://doi.org/10.1007/978-3-540-73368-3_29
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
