1 | \documentclass[11pt,a4paper]{article} |
---|
2 | \usepackage{color} |
---|
3 | \usepackage[utf8]{inputenc} |
---|
4 | \usepackage[ruled,linesnumbered]{algorithm2e} |
---|
5 | \usepackage{amsmath} |
---|
6 | \usepackage{graphicx} |
---|
7 | \usepackage[english]{babel} |
---|
8 | \usepackage{url} |
---|
9 | \usepackage{supertabular} |
---|
10 | \usepackage{multirow} |
---|
11 | \usepackage{booktabs} |
---|
12 | \usepackage{ae,aecompl,aeguill} % meilleur rendu que T1 fontenc |
---|
13 | \usepackage{subfigure} |
---|
14 | |
---|
15 | % dimensions de page (reglages probablement non optimaux...) |
---|
16 | \evensidemargin=0cm |
---|
17 | \oddsidemargin=0cm |
---|
18 | \topmargin=-1.5cm |
---|
19 | \textheight=25cm |
---|
20 | \leftmargin=0cm |
---|
21 | \textwidth=19cm |
---|
22 | \sloppy |
---|
23 | \flushbottom |
---|
24 | \parindent 1em |
---|
25 | \hoffset -0.5in |
---|
26 | \oddsidemargin 0pt |
---|
27 | \evensidemargin 0pt |
---|
28 | \marginparsep 10pt |
---|
29 | \RequirePackage{geometry} |
---|
30 | \geometry{reset, |
---|
31 | papersize={210mm,297mm}, |
---|
32 | text={180mm,260mm}, |
---|
33 | headheight=50pt, |
---|
34 | headsep=10pt, |
---|
35 | hoffset=0cm, |
---|
36 | voffset=0cm, |
---|
37 | } |
---|
38 | |
---|
39 | \graphicspath{{fig/}} |
---|
40 | \newcommand{\TODO}[1] {\par\textcolor{red}{TODO : #1}\par} |
---|
41 | \newcommand{\remark}[2]{\textcolor{blue}{#1: #2}} |
---|
42 | |
---|
43 | \begin{document} |
---|
44 | % entête |
---|
45 | \thispagestyle{empty} |
---|
46 | |
---|
47 | \title{Experiments with the Huffman Decoder/Encoder\\ |
---|
48 | (VIS bench) |
---|
49 | } |
---|
50 | \date{\today} |
---|
51 | \author{Cécile Braunstein} |
---|
52 | \maketitle |
---|
53 | |
---|
54 | \section{Original platform from VIS} |
---|
55 | \subsection{Model architecture} |
---|
56 | \begin{figure}[h] |
---|
57 | \centering |
---|
58 | \includegraphics[]{ArchGeneral} |
---|
59 | \caption{\label{fig:huff_original_arch} Architecture of Huffman original} |
---|
60 | \end{figure} |
---|
61 | \begin{figure}[h] |
---|
62 | \centering |
---|
63 | \subfigure[Encoder automaton]{ |
---|
64 | \includegraphics[]{encoder_aut} |
---|
65 | \label{fig:huff_original_encod} |
---|
66 | } |
---|
67 | \subfigure[Decoder automaton]{ |
---|
68 | \includegraphics[]{decoder_aut} |
---|
69 | \label{fig:huff_original_decod} |
---|
70 | } |
---|
71 | \end{figure} |
---|
72 | The Huffman circuit describes the implementation of static (English) Huffman |
---|
73 | encoder/decoder. |
---|
74 | \begin{itemize} |
---|
75 | \item Encoder: Read a character and return the encoding form bit by bit |
---|
76 | \item Decoder: Explore the encoding tree and return the character when it |
---|
77 | reaches a leaf. |
---|
78 | \end{itemize} |
---|
79 | |
---|
80 | |
---|
81 | \subsection{Robustness Analysis} |
---|
82 | The robustness analysis has been performed for usut and msmt faults only. The |
---|
83 | set of safe states for robustness 4 is the reach set of states. |
---|
84 | \begin{table}[htbp] |
---|
85 | \input{./experiments/huff_original_res_small} |
---|
86 | \caption{Robustness of the Huffman circuit from the VIS |
---|
87 | bench\label{table:orig_vis}} |
---|
88 | \end{table} |
---|
89 | The table \ref{table:orig_vis} shows the robustness analysis of the original |
---|
90 | circuit in VIS bench. |
---|
91 | There exists $eds$ from where the circuits will never recover. |
---|
92 | After analyzing these path (by producing counterexample), |
---|
93 | we were able to avoid them path by modifying the encoder automaton. The case |
---|
94 | were {\tt shiftreg} equals 0 is not taken into account on this automaton. |
---|
95 | This can be solved by replacing the guard transition from SHIFT to INIT. |
---|
96 | |
---|
97 | From this point, we will considered only this modified version of the Huffman |
---|
98 | circuit. |
---|
99 | \begin{table}[htbp] |
---|
100 | \input{experiments/huff_my_orig} |
---|
101 | \caption{Robustness of the corrected Huffman circuit from the VIS |
---|
102 | bench\label{table:orig_cor}} |
---|
103 | \end{table} |
---|
104 | |
---|
105 | \begin{table}[htbp] |
---|
106 | |
---|
107 | \input{experiments/huff_grade2} |
---|
108 | \caption{Register grading of the corrected Huffman circuit from the VIS |
---|
109 | bench\label{table:grade_cor}} |
---|
110 | \end{table} |
---|
111 | |
---|
112 | This circuit is not completely robust due to the desynchronization between the |
---|
113 | encoder and the decoder machine. The fault may have change the code of |
---|
114 | character in the encoder while the decoder where decoding it. |
---|
115 | The original circuit does not have a mechanism to prevent such |
---|
116 | desynchronization such as handshake protocol. |
---|
117 | |
---|
118 | \section{Huffman decoder/encoder synchronization} |
---|
119 | We synchronized the behavior of the decoder and the encoder device. |
---|
120 | The decoder starts only when the encoder said so. The encoder may restarts the |
---|
121 | decoder even when the decoding part is not over. |
---|
122 | |
---|
123 | This mechanism ensure the robustness level 4 with the set of reachable states |
---|
124 | considered as safe states. Nevertheless this does not ensure the |
---|
125 | synchronization with the golden behavior. |
---|
126 | The non-robustness 3 comes from the fact that the environment does not have |
---|
127 | constraints. Moreover, it comes also from the lack of synchronization between the |
---|
128 | environment and the model under test. |
---|
129 | |
---|
130 | \begin{figure}[htbp] |
---|
131 | \centering |
---|
132 | \subfigure[Encoder automaton]{ |
---|
133 | \includegraphics[scale=1]{encoder_synchro} |
---|
134 | \label{fig:huff_synchro_encod} |
---|
135 | } |
---|
136 | \subfigure[Decoder automaton]{ |
---|
137 | \includegraphics[scale=1]{decoder_synchro} |
---|
138 | \label{fig:huff_synchro_decod} |
---|
139 | } |
---|
140 | \end{figure} |
---|
141 | \begin{table}[htbp] |
---|
142 | \input{experiments/huff_synchro} |
---|
143 | \caption{Robustness Huffman circuit with internal |
---|
144 | synchronization\label{table:rob_synchro}} |
---|
145 | \end{table} |
---|
146 | |
---|
147 | \begin{table}[htbp] |
---|
148 | |
---|
149 | \input{experiments/huff_grade_synchro} |
---|
150 | \caption{Register grading Huffman circuit with internal |
---|
151 | synchronization\label{table:grade_synchro}} |
---|
152 | \end{table} |
---|
153 | |
---|
154 | \section{Huffman with a constraint environment} |
---|
155 | \subsection{Environment: a given text} |
---|
156 | We build an environment synchronized with the encoder. The environment send |
---|
157 | the letter A and E alternatively when it received the acknowledgment from the |
---|
158 | encoder saying that the character code is sent. |
---|
159 | |
---|
160 | \begin{figure}[htbp] |
---|
161 | \centering |
---|
162 | \subfigure[Environment]{ |
---|
163 | \includegraphics[scale=1]{environment} |
---|
164 | \label{fig:environment} |
---|
165 | } |
---|
166 | \subfigure[New Encoder]{ |
---|
167 | \includegraphics[scale=1]{encoder_with_env} |
---|
168 | \label{fig:encod_with_env} |
---|
169 | } |
---|
170 | \end{figure} |
---|
171 | |
---|
172 | We perform a robustness analysis with a new rob3~:\\ |
---|
173 | The faulty and the golden have got the same inputs from the environment. The |
---|
174 | environment only reacts to the outputs from the faulty circuits. |
---|
175 | |
---|
176 | The set of safe states are the ones where the golden and the faulty states are |
---|
177 | observably equivalent. |
---|
178 | |
---|
179 | \input{experiments/huff_with_env} |
---|
180 | |
---|
181 | Self stabilized after 10 steps, there is not healthy states before. |
---|
182 | Just checking the \verb+AX:9 AG (golendOut == faultyOut) + |
---|
183 | \verb+and AX:10 AG (golendOut == faultyOut)+ |
---|
184 | |
---|
185 | \subsection{Synchronized with the decoder} |
---|
186 | Our goal is to model the basis functionnalities that an environment should at |
---|
187 | least have. |
---|
188 | In this experiments any character may be encode. The environment is waiting |
---|
189 | that the encoder is ready to take a letter (\verb+ack = 1+) and send a letter in a non |
---|
190 | deterministic time (free input \verb+i_val+). |
---|
191 | This modeling implies that we need to add |
---|
192 | fairness constraints to avoid the infinite path where the environment never |
---|
193 | asks for a new encoding. |
---|
194 | \begin{figure}[htbp] |
---|
195 | \centering |
---|
196 | \includegraphics[scale=1]{env_start} |
---|
197 | \label{fig:environment_nd} |
---|
198 | \caption{Less constraint environment} |
---|
199 | |
---|
200 | \end{figure} |
---|
201 | \begin{table}[htbp] |
---|
202 | |
---|
203 | \input{experiments/huff_basic_env} |
---|
204 | \caption{Robustness with any text environment\label{table:basic_env}} |
---|
205 | \end{table} |
---|
206 | |
---|
207 | |
---|
208 | \subsection{Separate study for decoder and encoder} |
---|
209 | The encoder is completely robust (rob3 and rob4) under the fairness constraint |
---|
210 | that the environment should ask for a new computation from time to time. |
---|
211 | |
---|
212 | The decoder has got the same characteristic. It is robust iff his environment |
---|
213 | always need a new computation. |
---|
214 | The encoder verifies this property \verb+(AG(AF(start = 1)))+, hence the |
---|
215 | composition of the decoder and encoder is 100\% robust. |
---|
216 | \end{document} |
---|