Formal verification of logical descriptions with functional uncertainty based on logarithmic encoding of conditions

We consider the implementability testing problem for a description with functional uncertainty represented with a system of partial Boolean functions (PBF) given by a combinatorial circuit. Implementability testing is based on a formal approach in which we construct a conjunctive normal form (CNF) based on encoding multi-output intervals from the domain of this system. We propose a method for CNF construction related to a system of PBFs which is based on logarithmic encoding of multi-output intervals from the domain of this system and lets one reduce the number of auxiliary variables introduced in the resulting CNF.