<!DOCTYPE article
PUBLIC "-//NLM//DTD JATS (Z39.96) Journal Publishing DTD v1.4 20190208//EN"
       "JATS-journalpublishing1.dtd">
<article xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" article-type="research-article" dtd-version="1.4" xml:lang="en">
 <front>
  <journal-meta>
   <journal-id journal-id-type="publisher-id">Bulletin of KSAU</journal-id>
   <journal-title-group>
    <journal-title xml:lang="en">Bulletin of KSAU</journal-title>
    <trans-title-group xml:lang="ru">
     <trans-title>Вестник КрасГАУ</trans-title>
    </trans-title-group>
   </journal-title-group>
   <issn publication-format="print">1819-4036</issn>
  </journal-meta>
  <article-meta>
   <article-id pub-id-type="publisher-id">78186</article-id>
   <article-categories>
    <subj-group subj-group-type="toc-heading" xml:lang="ru">
     <subject>МАТЕМАТИКА И ИНФОРМАТИКА</subject>
    </subj-group>
    <subj-group subj-group-type="toc-heading" xml:lang="en">
     <subject></subject>
    </subj-group>
    <subj-group>
     <subject>МАТЕМАТИКА И ИНФОРМАТИКА</subject>
    </subj-group>
   </article-categories>
   <title-group>
    <article-title xml:lang="en">FORMAL VERIFICATION IN VERY LARGE-SCALE INTEGRATIONDESIGNING</article-title>
    <trans-title-group xml:lang="ru">
     <trans-title>Формальная верификация при проектировании сверхбольших интегральных схем</trans-title>
    </trans-title-group>
   </title-group>
   <contrib-group content-type="authors">
    <contrib contrib-type="author">
     <name-alternatives>
      <name xml:lang="ru">
       <surname>Титовская</surname>
       <given-names>Т С</given-names>
      </name>
      <name xml:lang="en">
       <surname>Titovskaya</surname>
       <given-names>T S</given-names>
      </name>
     </name-alternatives>
     <xref ref-type="aff" rid="aff-1"/>
    </contrib>
    <contrib contrib-type="author">
     <name-alternatives>
      <name xml:lang="ru">
       <surname>Непомнящий</surname>
       <given-names>О В</given-names>
      </name>
      <name xml:lang="en">
       <surname>Nepomnyashchiy</surname>
       <given-names>O V</given-names>
      </name>
     </name-alternatives>
     <xref ref-type="aff" rid="aff-2"/>
    </contrib>
    <contrib contrib-type="author">
     <name-alternatives>
      <name xml:lang="ru">
       <surname>Леонова</surname>
       <given-names>А В</given-names>
      </name>
      <name xml:lang="en">
       <surname>Leonova</surname>
       <given-names>A V</given-names>
      </name>
     </name-alternatives>
     <xref ref-type="aff" rid="aff-3"/>
    </contrib>
    <contrib contrib-type="author">
     <name-alternatives>
      <name xml:lang="ru">
       <surname>Комаров</surname>
       <given-names>А А</given-names>
      </name>
      <name xml:lang="en">
       <surname>Komarov</surname>
       <given-names>A A</given-names>
      </name>
     </name-alternatives>
     <xref ref-type="aff" rid="aff-4"/>
    </contrib>
   </contrib-group>
   <aff-alternatives id="aff-1">
    <aff>
     <institution xml:lang="ru">Сибирский федеральный университет</institution>
     <country>ru</country>
    </aff>
    <aff>
     <institution xml:lang="en">Сибирский федеральный университет</institution>
     <country>ru</country>
    </aff>
   </aff-alternatives>
   <aff-alternatives id="aff-2">
    <aff>
     <institution xml:lang="ru">Сибирский федеральный университет</institution>
     <country>ru</country>
    </aff>
    <aff>
     <institution xml:lang="en">Сибирский федеральный университет</institution>
     <country>ru</country>
    </aff>
   </aff-alternatives>
   <aff-alternatives id="aff-3">
    <aff>
     <institution xml:lang="ru">Сибирский федеральный университет</institution>
     <country>ru</country>
    </aff>
    <aff>
     <institution xml:lang="en">Сибирский федеральный университет</institution>
     <country>ru</country>
    </aff>
   </aff-alternatives>
   <aff-alternatives id="aff-4">
    <aff>
     <institution xml:lang="ru">Сибирский федеральный университет</institution>
     <country>ru</country>
    </aff>
    <aff>
     <institution xml:lang="en">Сибирский федеральный университет</institution>
     <country>ru</country>
    </aff>
   </aff-alternatives>
   <pub-date publication-format="print" date-type="pub" iso-8601-date="2014-04-25T19:22:47+04:00">
    <day>25</day>
    <month>04</month>
    <year>2014</year>
   </pub-date>
   <pub-date publication-format="electronic" date-type="pub" iso-8601-date="2014-04-25T19:22:47+04:00">
    <day>25</day>
    <month>04</month>
    <year>2014</year>
   </pub-date>
   <issue>4</issue>
   <fpage>87</fpage>
   <lpage>89</lpage>
   <history>
    <date date-type="received" iso-8601-date="2014-04-21T19:22:47+04:00">
     <day>21</day>
     <month>04</month>
     <year>2014</year>
    </date>
    <date date-type="accepted" iso-8601-date="2014-04-23T19:22:47+04:00">
     <day>23</day>
     <month>04</month>
     <year>2014</year>
    </date>
   </history>
   <self-uri xlink:href="https://vestnik.kgau.ru/en/nauka/article/78186/view">https://vestnik.kgau.ru/en/nauka/article/78186/view</self-uri>
   <abstract xml:lang="ru">
    <p>Рассмотрены основные маршруты высокоуровневого синтеза вентильных описаний СБИС. Определены проблемы верификации проекта на функциональном уровне, присущие традиционным методам проектирования. Изложены основные положения разрабатываемой технологии архитектурно-независимого представления СБИС на основе функционально-потоковой парадигмы параллельного программирования. Предложен подход к формальной верификации проекта при высокоуровневом синтезе.</p>
   </abstract>
   <trans-abstract xml:lang="en">
    <p>The main routes of the high-level synthesisof the VLSI gated descriptions are considered. The project verification problems on the functional level, inherent in traditional methods of design are defined. The basic provisions of the developed architecture-independent technology for VLSI representation on the basis of the functional-flow paradigm of parallel programming are presented. The approach to the project formal verification in the high level synthesis is offered.</p>
   </trans-abstract>
   <kwd-group xml:lang="ru">
    <kwd>верификация</kwd>
    <kwd>сверхбольшие интегральные схемы (СБИС)</kwd>
    <kwd>функциональное программирование</kwd>
    <kwd>параллельные вычисления</kwd>
   </kwd-group>
   <kwd-group xml:lang="en">
    <kwd>verification</kwd>
    <kwd>very large-scale integration (VLSI)</kwd>
    <kwd>functional programming</kwd>
    <kwd>parallel computing</kwd>
   </kwd-group>
  </article-meta>
 </front>
 <body>
  <p></p>
 </body>
 <back>
  <ref-list/>
 </back>
</article>
