[105] | 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} |
---|