Automatic Decoder Synthesis: Methods and Case Studies

Autor:	Jie-Hong R. Jiang, Chen-Hsuan Lin, Yen-Cheng Chou, Hsiou-Yuan Liu
Rok vydání:	2012
Předmět:	Correctness Craig interpolation Data_CODINGANDINFORMATIONTHEORY Sequential decoding Computer Graphics and Computer-Aided Design Soft-decision decoder Encoding (memory) Electrical and Electronic Engineering Boolean satisfiability problem Algorithm Encoder Software Decoding methods Mathematics
Zdroj:	IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 31:1319-1331
ISSN:	1937-4151 0278-0070
DOI:	10.1109/tcad.2012.2191288
Popis:	Upon receiving the output sequence streaming from a sequential encoder, a decoder reconstructs the corresponding input sequence that streamed to the encoder. Such an encoding and decoding scheme is commonly encountered in communication, cryptography, signal processing, and other applications. Given an encoder specification, decoder design can be error-prone and time consuming. Its automation may help designers improve productivity and justify encoder correctness. Though recent advances showed promising progress, there is still no complete method that decides whether a decoder exists for a finite state transition system. The quest for completely automatic decoder synthesis remains. This paper presents a complete and practical approach to automating decoder synthesis via incremental Boolean satisfiability solving and Craig interpolation. Experiments show that, for decoder-existent cases, our method synthesizes decoders effectively; for decoder-nonexistent cases, our method concludes the nonexistence instantly while prior methods may fail. Case studies are also conducted in synthesizing decoders for linear error-correcting codes.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::fb10f2f003f0938afc493f8d6db60988 https://doi.org/10.1109/tcad.2012.2191288 Zobrazit plný text záznamu