\begin{abstract}
Verilog-2005 is a powerful Hardware Description Language (HDL) that
-can be used to easily create complex designs from small HDL code.
+can be used to easily create complex designs from small HDL code.
BTOR~\cite{btor} is a bit-precise word-level format for model
checking. It is simple format and easy to parse. It allows to model
-the model checking problem over extensional theory of bit-vectors with
+the model checking problem over theory of bit-vectors with
one-dimensional arrays, thus enabling to model verilog designs with
-registers and memories.
-Yosys \cite{yosys} is an Open-Source Verilog synthesis tool that can
-be used to convert Verilog designs with simple assertions to BTOR format.
+registers and memories. Yosys \cite{yosys} is an Open-Source Verilog
+synthesis tool that can be used to convert Verilog designs with simple
+assertions to BTOR format.
\end{abstract}