From d9444878cc52bc35e4ae696b5d13e82874b6b3b1 Mon Sep 17 00:00:00 2001 From: Ahmed Irfan Date: Mon, 3 Nov 2014 18:35:50 +0100 Subject: [PATCH] corrected abstract of appnote --- manual/APPNOTE_012_Verilog_to_BTOR.tex | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/manual/APPNOTE_012_Verilog_to_BTOR.tex b/manual/APPNOTE_012_Verilog_to_BTOR.tex index 170f7378a..c441d9502 100644 --- a/manual/APPNOTE_012_Verilog_to_BTOR.tex +++ b/manual/APPNOTE_012_Verilog_to_BTOR.tex @@ -57,14 +57,14 @@ \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}