Towards completely automatic decoder synthesis
Hsiou-Yuan Liu, Yen-Cheng Chou, Chen-Hsuan Lin, Jie-Hong Roland Jiang · 2011
Upon receiving the output sequence streaming from a sequen-tial encoder, a decoder reconstructs the corresponding input sequence that streamed to the encoder. Such an encoding and decoding scheme is commonly encountered in commu-nication, cryptography, signal processing, and other applica-tions. Given an encoder specification, decoder design can be error-prone and time consuming. Its automation may help designers improve productivity and justify encoder correct-ness. Though recent advances showed promising progress, there is still no complete method that decides whether a de-coder exists for a finite state transition system. The quest for completely automatic decoder synthesis remains. This paper presents a complete and practical approach to au-tomating decoder synthesis via incremental SAT solving and Craig interpolation. Experiments show that, for decoder-existent cases, our method synthesizes decoders effectively; for decoder-nonexistent cases, our method concludes the non-existence instantly while prior methods may fail.