Lab for Automated Reasoning and Analysis LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
Next revision
Previous revision
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