Advertisement

Suraq — A Controller Synthesis Tool Using Uninterpreted Functions

  • Georg Hofferek
  • Ashutosh Gupta
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8855)

Abstract

Boolean controllers for systems with complex datapaths are often very difficult to implement correctly, in particular when concurrency is involved. Yet, in many instances it is easy to formally specify correctness. For example, the specification for the controller of a pipelined processor only has to state that the pipelined processor gives the same results as a non-pipelined reference design. This makes such controllers a good target for automated synthesis. However, an efficient abstraction for the complex datapath elements is needed, as a bit-precise description is often infeasible. We present Suraq, the first controller synthesis tool which uses uninterpreted functions for the abstraction. Quantified first-order formulas (with specific quantifier structure) serve as the specification language from which Suraq synthesizes Boolean controllers. Suraq transforms the specification into an unsatisfiable SMT formula, and uses Craig interpolation to compute its results. Using Suraq, we were able to synthesize a controller (consisting of two Boolean signals) for a five-stage pipelined DLX processor in roughly one hour and 15 minutes.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Suraq — Synthesizer using Uninterpreted functions, aRrays and eQuality (2014), http://www.iaik.tugraz.at/content/research/design_verification/suraq/
  2. 2.
    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard: Version 2.0. In: Proc. of the 8th Int. Workshop on Satisfiability Modulo Theories (2010)Google Scholar
  3. 3.
    Bouton, T., de Oliveira, D.C.B., Déharbe, D., Fontaine, P.: veriT: An open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 151–156. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  4. 4.
    Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  5. 5.
    Burch, J.R., Dill, D.L.: Automatic verification of pipelined microprocessor control. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 68–80. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  6. 6.
    Craig, W.: Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory. The Journal of Symbolic Logic 22(3), 269–285 (1957)CrossRefMATHMathSciNetGoogle Scholar
  7. 7.
    Filiot, E., Jin, N., Raskin, J.-F.: An antichain algorithm for LTL realizability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 263–277. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  8. 8.
    Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) VMCAI 2012. LNCS, vol. 7148, pp. 219–234. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  9. 9.
    Fuchs, A., Goel, A., Grundy, J., Krstic, S., Tinelli, C.: Ground interpolation for the theory of equality. Logical Methods in Computer Science 8(1) (2012)Google Scholar
  10. 10.
    Hennessy, J.L., Patterson, D.A.: Computer Architecture: A Quantitative Approach, 2nd edn. Morgan Kaufmann (1996)Google Scholar
  11. 11.
    Hofferek, G.: Controller Synthesis with Uninterpreted Functions. Ph.D. thesis, Graz University of Technology (July 2014)Google Scholar
  12. 12.
    Hofferek, G., Bloem, R.: Controller synthesis for pipelined circuits using uninterpreted functions. In: MEMOCODE (2011)Google Scholar
  13. 13.
    Hofferek, G., Gupta, A., Könighofer, B., Jiang, J., Bloem, R.: Synthesizing multiple boolean functions using interpolation on a single proof. In: FMCAD (2013)Google Scholar
  14. 14.
    Jobstmann, B., Galler, S., Weiglhofer, M., Bloem, R.: Anzu: A tool for property synthesis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 258–262. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Kuncak, V., Mayer, M., Piskac, R., Suter, P.: Functional synthesis for linear arithmetic and sets. STTT 15(5-6) (2013)Google Scholar
  16. 16.
    Morgenstern, A., Schneider, K.: Exploiting the temporal logic hierarchy and the non-confluence property for efficient LTL synthesis. GANDALF (2010)Google Scholar
  17. 17.
    Schewe, S., Finkbeiner, B.: Bounded synthesis. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 474–488. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  18. 18.
    Sohail, S., Somenzi, F.: Safety first: a two-stage algorithm for the synthesis of reactive systems. STTT 15(5-6) (2013)Google Scholar
  19. 19.
    Solar-Lezama, A.: Program sketching. STTT 15(5-6) (2013)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Georg Hofferek
    • 1
  • Ashutosh Gupta
    • 2
  1. 1.Graz University of TechnologyAustria
  2. 2.ISTAustria

Personalised recommendations