Advances in Completely Automatic Decoder Synthesis
This presentation by Y.C. Chou and H.S. Liu on "Towards Completely Automatic Decoder Synthesis" covers topics such as motivation, preliminary concepts, main algorithms, and experimental results in the field of communication and cryptography systems. The content delves into notation, SAT solvers, Craig interpolation, state transition systems, and problem statements related to decoder synthesis. The preliminary section includes discussions on Boolean vectors, cardinality, and transition states. The presentation aims to enhance understanding and implementation of automatic decoder synthesis techniques.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. Download presentation by click this link. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
E N D
Presentation Transcript
Towards Completely Automatic Decoder Synthesis Presented by Y. C. Chou & H. S. Liu Dec. 3, 2010
Outline Introduction Preliminary Main Algorithm Experimental Result Conclusion
Outline Introduction Preliminary Main Algorithm Experimental Result Conclusion
Introduction Motivation Data processing Communication, cryptography Encode-decode system Prior work Craig interpolation
Outline Introduction Preliminary Notation SAT Solver Craig Interpolation State Transition System Problem Statement Main Algorithm Experimental Result Conclusion
Preliminary Notation Boolean vector Cardinality Set of truth valuation
Preliminary SAT Solver For a Boolean vector and a Boolean function , SAT Solver asks whether That is whether is unsatisfiable.
Preliminary Craig interpolation refers to the common variables of and such that unsatisfiable
Preliminary State Transition System Initial states Transition relation Input variables Current-/Next-state variables Output variables
Preliminary State Transition System Furthermore ? ? At time t T Duplication ? ? Duplication at time t
Preliminary State Transition System T0 T 1 Tp T n T1 T* n T* 1 T*0 T*1 T*p
Preliminary State Transition System Dangling, recurrent and transition states dangling transient recurrent recurrent
Preliminary Problem Statement Streaming decoder Time-frame expansion of an encoder Finite observing window Prefix and postfix issue Care-state
Outline Introduction Preliminary Main Algorithm Decoder Existence Decoder Synthesis Disjunction on CNF Incremental SAT Experimental Result Conclusion
Main Algorithm Decoder Existence Naive approach Keep adding timeframe to find decoder If decoder not exists?
Main Algorithm Decoder Existence We propose a complete method
Main Algorithm Decoder Existence An Infinite loop occurs iff the condition is met
Main Algorithm Decoder Existence Efficient implementation
Main Algorithm Decoder Existence Decoder existence checking flow
Main Algorithm Decoder Synthesis T n T 1 T0 T1 Tp = = = = = T* n T* 1 T*0 T*1 T*p
Main Algorithm Decoder Synthesis Bitwise over the input alphabet Common variables selected for interpolant-based decoder 1 T n T 1 T0 T1 Tp ? = = = = = ? 0 T* n T* 1 T*0 T*1 T*p
Main Algorithm (Recall) Craig interpolation refers to the common variables of and such that unsatisfiable
Main Algorithm Decoder Synthesis Bitwise over the input alphabet Common variables selected for interpolant-based decoder 1 T n T 1 T0 T1 Tp ? = = = = = ? 0 T* n T* 1 T*0 T*1 T*p
Main Algorithm Disjunction on CNF Satisfiability equivalence (? ?) (? ?) (? ?) (?1 ?)(?2 ?)(? ?)(?1 ?)(?2 ?)(?3 ?)(? ? ?) (?1 ?2) (?1 ?2 ?3)
Main Algorithm Incremental SAT T n T 1 T0 T1 Tp = = = = = T* n T* 1 T*0 T*1 T*p
Main Algorithm Incremental SAT T T n T 1 T0 T1 Tp = = = = = = T* T* n T* 1 T*0 T*1 T*p
Main Algorithm Incremental SAT T 1 T n 1 T 2 T0 T1 Tp = = = = = = T* 1 T* n 1 T* 2 T*0 T*1 T*p
Outline Introduction Preliminary Main Algorithm Experimental Result Decoder Generation Existence Checking Both Conclusion
Experimental Result Comparison on Decoder Generation Generation time + Optimization time AIG size/AIG level
Experimental Result Comparison on Existence Checking Time to check circuit without decoder Ours is complete method
Experimental Result Existence Checking and Decoder Generation At least 1 order speed up in time Slightly circuit size increment
Outline Introduction Preliminary Main Algorithm Experimental Result Conclusion
Conclusion Future Work Case study Hamming Code Optimization XOR optimization Another data structure Error Correction Code (ECC) synthesis Encoder Synthesis
