list of contributions

Author: osmanyasar05

paper.tex

@@ -286,6 +286,13 @@
 
 \section{Introduction}
 
+\begin{itemize} 
+  \item Formalization of bitheap data structure and efficient compression algorithms in a theorem prover
+  \item Integration into an existing synthesis flow to provide formally verified datapath circuits to eliminate the SAT solver bottleneck
+  \item Integration of bitheap data structure into Lean 4's formally verified bit blaster to improve the solvers capabilities
+  \item Verified synthesis of existing datapath benchmark suite 
+\end{itemize}
+
 \section{Background}
 In digital arithmetic, an integer or fixed-point number is represented as follows:
 \[
@@ -345,6 +352,20 @@ \subsection{Dadda's Algorithm}
 \end{enumerate}
 \end{tcolorbox}
 
+\section{Formalization}
+
+\subsection{Bit Heap Data Structure}
+
+\subsection{Compression Algorithms}
+
+\section{Integration}
+
+\subsection{Datapath Synthesis Engine}
+
+\subsection{Bit Blaster}
+
+\section{Results}
+
 \section{Related Work}
 
 \section{Conclusion}