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.

• Automatic Decoder Synthesis
• Communication Systems
• Cryptography
• SAT Solver
• State Transition Systems

indiyah Follow

Uploaded on Oct 06, 2024 | 0 Views

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.

Presentation Transcript

1. Towards Completely Automatic Decoder Synthesis Presented by Y. C. Chou & H. S. Liu Dec. 3, 2010

2. Outline Introduction Preliminary Main Algorithm Experimental Result Conclusion

3. Outline Introduction Preliminary Main Algorithm Experimental Result Conclusion

4. Introduction Motivation Data processing Communication, cryptography Encode-decode system Prior work Craig interpolation

5. Outline Introduction Preliminary Notation SAT Solver Craig Interpolation State Transition System Problem Statement Main Algorithm Experimental Result Conclusion

6. Preliminary Notation Boolean vector Cardinality Set of truth valuation

7. Preliminary SAT Solver For a Boolean vector and a Boolean function , SAT Solver asks whether That is whether is unsatisfiable.

8. Preliminary Craig interpolation refers to the common variables of and such that unsatisfiable

9. Preliminary State Transition System Initial states Transition relation Input variables Current-/Next-state variables Output variables

10. Preliminary State Transition System Furthermore ? ? At time t T Duplication ? ? Duplication at time t

11. Preliminary State Transition System T0 T 1 Tp T n T1 T* n T* 1 T*0 T*1 T*p

12. Preliminary State Transition System Dangling, recurrent and transition states dangling transient recurrent recurrent

13. Preliminary Problem Statement Streaming decoder Time-frame expansion of an encoder Finite observing window Prefix and postfix issue Care-state

14. Outline Introduction Preliminary Main Algorithm Decoder Existence Decoder Synthesis Disjunction on CNF Incremental SAT Experimental Result Conclusion

15. Main Algorithm Decoder Existence Naive approach Keep adding timeframe to find decoder If decoder not exists?

16. Main Algorithm Decoder Existence We propose a complete method

17. Main Algorithm Decoder Existence An Infinite loop occurs iff the condition is met

18. Main Algorithm Decoder Existence Efficient implementation

19. Main Algorithm Decoder Existence Decoder existence checking flow

21. Main Algorithm Decoder Synthesis T n T 1 T0 T1 Tp = = = = = T* n T* 1 T*0 T*1 T*p

22. 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

23. Main Algorithm (Recall) Craig interpolation refers to the common variables of and such that unsatisfiable

24. 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

25. Main Algorithm Disjunction on CNF Satisfiability equivalence (? ?) (? ?) (? ?) (?1 ?)(?2 ?)(? ?)(?1 ?)(?2 ?)(?3 ?)(? ? ?) (?1 ?2) (?1 ?2 ?3)

26. Main Algorithm Incremental SAT T n T 1 T0 T1 Tp = = = = = T* n T* 1 T*0 T*1 T*p

27. Main Algorithm Incremental SAT T T n T 1 T0 T1 Tp = = = = = = T* T* n T* 1 T*0 T*1 T*p

28. 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

29. Outline Introduction Preliminary Main Algorithm Experimental Result Decoder Generation Existence Checking Both Conclusion

30. Experimental Result Comparison on Decoder Generation Generation time + Optimization time AIG size/AIG level

32. Experimental Result Comparison on Existence Checking Time to check circuit without decoder Ours is complete method

33. Experimental Result Existence Checking and Decoder Generation At least 1 order speed up in time Slightly circuit size increment

34. Outline Introduction Preliminary Main Algorithm Experimental Result Conclusion

35. Conclusion Future Work Case study Hamming Code Optimization XOR optimization Another data structure Error Correction Code (ECC) synthesis Encoder Synthesis