Complementary synthesis automatically generates an encoder's decoder with the assumption that the encoder's all input variables can always be uniquely determined by its output symbol sequence. However, to prevent the faster encoder from overwhelming the slower decoder, many encoders employ flow control mechanism that fails this assumption. Such encoders, when their output symbol sequences are too fast to be processed by the decoders, will stop transmitting data symbols, but instead transmitting idle symbols that can only uniquely determine a subset of the encoder's input variables. And the decoder should recognize and discard these idle symbols. This mechanism fails the assumption of all complementary synthesis algorithms, because some input variables can't be uniquely determined by the idle symbol. A novel algorithm is proposed to handle such encoders. First, it identifies all input variables that can be uniquely determined, and takes them as flow control variables. Second, it infers a predicate over these flow control variables that enables all other input variables to be uniquely determined. Third, it characterizes the decoder's Boolean function with Craig interpolant. Experimental results on several complex encoders indicate that this algorithm can always correctly identify the flow control variables, infer the predicates and generate the decoder's Boolean functions.

In this paper, we study the problem of solving hard propositional satisfiability problem in Cloud or computing grid, which is honest-but-curious. We propose an approach to preserve input and output privacy based on CNF obfuscation, and present obfuscation algorithm and its corresponding solution recovery algorithm. By obfuscation, the CNF formula is transformed into another formula, with different circuit structure and over-approximated solution space. Solution of the original CNF can be extracted from the solution of obfuscated CNF by solution recovery. Theoretical analysis demonstrates that, obfuscation algorithm can significantly change the structure of CNF formula with polynomial time complexity, while solution recovery algorithm can filter out solution with linear time complexity. Experimental results on ISCAS89 benchmark show that obfuscation incurs acceptable negative impact on the performance of SAT solving.

Complementary synthesis can automatically synthesize the decoder circuit of an encoder. However, its user needs to manually specify an assertion on some configuration pins to prevent the encoder from reaching the nonworking states. To avoid this tedious task, this paper propose an automatic approach to infer this assertion, by iteratively discovering and removing cases without decoders. To discover all decoders that may exist simultaneously under this assertion, a second algorithm based on functional dependency is proposed to decompose , the Boolean relation that uniquely determines the encoder's input, into all possible decoders. To help the user select the correct decoder, a third algorithm is proposed to infer each decoder's precondition formula, which represents those cases that lead to this decoder's existence. Experimental results on several complex encoders indicate that our algorithm can always infer assertions and generate decoders for them. Moreover, when multiple decoders exist simultaneously, the user can easily select the correct one by inspecting their precondition formulas.

Complementary synthesis can automatically synthesize the decoder circuit of an encoder. However, its user needs to manually specify an assertion on some configuration pins to prevent the encoder from reaching the non-working states. To avoid this tedious job, we propose an automatic approach to infer this assertion. First, we propose a halting algorithm that can decide the existence of the decoder for every particular assertion. Second, for every invalid value of configuration pins that leads to the non-existence of the decoder, we use cofactoring and Craig interpolation to infer a new formula, which covers a larger set of such invalid values. This second step is repeated until all invalid values are covered by these inferred formulas. Finally, we obtain the final assertion by anding the inverses of all these inferred formulas. The decoder exists if and only if this final assertion is still satisfiable. To illustrate its usefulness, we have run our algorithm on several complex encoder circuits, including PCI-E and Ethernet. Experimental results show that our algorithm can always infer assertions for them.

Complementary synthesis automatically synthesizes the decoder circuit of an encoder. It determines the existence of the decoder by checking whether the encoder's input can be uniquely determined by its output. However, this algorithm will not halt if the decoder does not exist. To solve this problem, a novel halting algorithm is proposed. For every path of the encoder, this algorithm first checks whether the encoder's input can be uniquely determined by its output. If yes, the decoder exists; otherwise, this algorithm checks if this path contains loops, which can be further unfolded to prove the non-existence of the decoder for all those longer paths. To illustrate its usefulness and efficiency, this algorithm has been run on several complex encoders, including PCI-E and Ethernet. Experimental results indicate that this algorithm always halts properly by distinguishing correct encoders from incorrect ones, and it is more than three times faster than previous ones.

One of the most difficult jobs in designing communication and multimedia chips is to design and verify the complex complementary circuit pair (E,E-1), in which circuit E transforms information into a format suitable for transmission and storage, and its complementary circuitE-1recovers this information. In order to facilitate this job, we proposed a novel two-step approach to synthesize the complementary circuitE-1fromEautomatically. First, a SAT solver was used to check whether the input sequence ofEcan be uniquely determined by its output sequence. Second, the complementary circuitE-1was built by characterizing its Boolean function, with an efficient all-solution SAT solver based on discovering XOR gates and extracting unsatisfiable cores. To illustrate its usefulness and efficiency, we ran our algorithm on several complex encoders from industrial projects, including PCIE and 10 G Ethernet, and successfully built correct complementary circuits for them.

One of the most difficult jobs in designing communication and multimedia chips, is to design and verify complex complementary circuit pair (E, E-1), in which circuit E transforms information into a format that is suitable for transmission and storage, while E's complementary circuit E-1 recovers this information.

It is a hotly research topic to eliminate irrelevant variables from counterexample, to make it easier to be understood. BFL algorithm is the most effective Counterexample minimization algorithm compared to all other approaches, but its run time overhead is very large due to one call to SAT solver per candidate variable to be eliminated. So we propose a faster counterexample minimization algorithm based on refutation analysis and incremental SAT. First, for every UNSAT instance of BFL, we perform refutation analysis to extract the set of variables that lead to UNSAT, all variables not belong to this set can be eliminated simultaneously. In this way, we can eliminate many variables with only one call to SAT solver. At the same time, we employ incremental SAT approach to share learned clauses between similar instances of BFL, to prevent overlapped state space from being searched repeatedly. Theoretic analysis and experiment result shows that, our approach can be 1 to 2 orders of magnitude faster than BFL, and still retain the minimization ability of BFL.

A hot research topic is the elimination of irrelevant variables from a counterexample, to make it more easily understood. The BFL (brute force lifting) algorithm is the most effective counterexample minimization algorithm compared to all other approaches. But its time overhead is very large due to one call to the SAT (satisfiability) solver for each candidate variable to be eliminated. The key to reducing time overhead is to eliminate multiple variables simultaneously. Therefore, we propose a faster counterexample minimization algorithm based on refutation analysis. We perform refutation analysis on those UNSAT instances of BFL, to extract the set of variables that lead to UNSAT. All variables not belonging to this set can be eliminated simultaneously as irrelevant variables. Thus we can eliminate multiple variables with only one call to the SAT solver. Theoretical analysis and experimental results show that our algorithm can be 2 to 3 orders of magnitude faster than the existing BFL algorithm, and with only minor loss in counterexample minimization ability.