**Abstract:** 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 worst case execution time

linear in nr, being n = |x| the number of

input arguments for functions in F and r the

number of functions in F. Moreover, a formal

proof of the proposed algorithm correctness is

also shown. Finally, we present experimental

results showing effectiveness of the proposed

algorithm.

**Keywords:** Control Software Synthesis; Embedded Systems; Model Checking