Lab for Automated Reasoning and Analysis LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

sav08:bitwidth_analysis [2008/05/20 18:58]
vkuncak
sav08:bitwidth_analysis [2015/04/21 17:30] (current)
Line 3: Line 3:
 Given a language with signed 64 bit integers, determine as small as possible set of bits needed to store values of variables. Given a language with signed 64 bit integers, determine as small as possible set of bits needed to store values of variables.
   * e.g. if analysis derives that a subset of $\{0,​1,​2,​\ldots,​7\}$ is sufficient, then we can use //byte// type to store the value   * e.g. if analysis derives that a subset of $\{0,​1,​2,​\ldots,​7\}$ is sufficient, then we can use //byte// type to store the value
 +      * instead of having multiple integer types, we can have analysis infer the right '​subtypes'​ (ranges)
   * the analysis becomes even more important if we generate hardware from C code: analysis would enable us to save circuits and power   * the analysis becomes even more important if we generate hardware from C code: analysis would enable us to save circuits and power
  
Line 16: Line 17:
 One simple rule: $g(x)=$ ​ One simple rule: $g(x)=$ ​
 ++++| ++++|
-\[\begin{array}{l}+\begin{equation*}\begin{array}{l}
 let\ L = \min(g(y)) + \min(g(z))-1 \\ let\ L = \min(g(y)) + \min(g(z))-1 \\
 let\ U = \max(g(y)) + \max(g(z))+1 \\ let\ U = \max(g(y)) + \max(g(z))+1 \\
Line 22: Line 23:
 else\ [L,U] else\ [L,U]
 \end{array} \end{array}
-\]+\end{equation*}
 ++++ ++++
  
 
sav08/bitwidth_analysis.txt · Last modified: 2015/04/21 17:30 (external edit)
 
© EPFL 2018 - Legal notice