From Boolean Functional Equations to Control Software
Mari
Federico
author
Melatti
Igor
author
Salvo
Ivano
author
Tronci
Enrico
author
2011
CoRR, Technical Report
Many software as well digital hardware automatic synthesis methods define the set of implementations meeting the given system specifications with a boolean relation K. In such a context a fundamental step in the software (hardware) synthesis process is finding effective solutions to the functional equation defined by K. This entails finding a (set of) boolean function(s) F (typically represented using OBDDs, Ordered Binary Decision Diagrams) such that: 1) for all x for which K is satisfiable, K(x, F(x)) = 1 holds; 2) the implementation of F is efficient with respect to given implementation parameters such as code size or execution time. While this problem has been widely studied in digital hardware synthesis, little has been done in a software synthesis context. Unfortunately the approaches developed for hardware synthesis cannot be directly used in a software context. This motivates investigation of effective methods to solve the above problem when F has to be implemented with software. In this paper we present an algorithm that, from an OBDD representation for K, generates a C code implementation for F that has the same size as the OBDD for F and a WCET (Worst Case Execution Time) at most O(nr), being n = |x| the number of arguments of functions in F and r the number of functions in F.
exported from refbase (http://mclab.di.uniroma1.it/publications/show.php?record=105), last updated on Sat, 01 Dec 2012 14:49:29 +0100
text
http://arxiv.org/abs/1106.0468
http://arxiv.org/abs/1106.0468
Mari_etal2011
technical report
report