Лекция 1. Введение. Задача верификации аппаратуры и программного обеспечения (1185523), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

Ïðîãðàììèðîâàíèå óñëîæíÿåòñÿÐàçðàáîòêà ïðîãðàìì (è óæ òåì áîëåå ìèêðîýëåêòðîííûõ ñõåì)ñòàíîâèòñÿ ¾êàñêàäíûì¿ ïðîöåññîì, íà ðàçíûõ ýòàïàõêîòîðîãî ïðîèñõîäèò óòî÷íåíèå ìîäåëè ïðîãðàììû èëèìèêðîýëåêòðîííîé ñõåìû, îêàí÷èâàþùååñÿ èõ ðåàëèçàöèåé.Îøèáêè, ïðîïóùåííûå íà ðàííèõ ýòàïàõ, íåâîçìîæíîóñòðàíèòü íà ïîñëåäóþùèõ ñòàäèÿõ ïðîåêòèðîâàíèÿ.Ïîýòîìó íåîáõîäèì öåëûé àðñåíàë ìåòîäîâ âåðèôèêàöèè,êîòîðûå ìîæíî áûëî áû ïðèìåíÿòü íå òîëüêî ê ñàìèìïðîãðàììàì (ñõåìàì), íî è òàêæå è ê èõ ìîäåëÿì,ïðåäñòàâëåííûõ íà ðàçíûõ óðîâíÿõ àáñòðàêöèè.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?4.

Âîçðàñòàíèå òðóäîåìêîñòè âåðèôèêàöèèÂû÷èñëèòåëüíàÿ àïïàðàòóðà ñòàíîâèòñÿ äåøåâëå, àïðîèçâîäèòåëüíîñòü êîìïüþòåðîâ âîçðàñòàåò.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?4. Âîçðàñòàíèå òðóäîåìêîñòè âåðèôèêàöèèÂû÷èñëèòåëüíàÿ àïïàðàòóðà ñòàíîâèòñÿ äåøåâëå, àïðîèçâîäèòåëüíîñòü êîìïüþòåðîâ âîçðàñòàåò.Ïîÿâëÿþòñÿ íîâûå âîçìîæíîñòè àâòîìàòè÷åñêîãî ðåøåíèÿ âñåáîëåå è áîëåå ñëîæíûõ çàäà÷.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?4. Âîçðàñòàíèå òðóäîåìêîñòè âåðèôèêàöèèÂû÷èñëèòåëüíàÿ àïïàðàòóðà ñòàíîâèòñÿ äåøåâëå, àïðîèçâîäèòåëüíîñòü êîìïüþòåðîâ âîçðàñòàåò.Ïîÿâëÿþòñÿ íîâûå âîçìîæíîñòè àâòîìàòè÷åñêîãî ðåøåíèÿ âñåáîëåå è áîëåå ñëîæíûõ çàäà÷.Ïðîèñõîäèò óâåëè÷åíèå îáúåìîâ ïðîãðàììíîãî êîäà.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?4.

Âîçðàñòàíèå òðóäîåìêîñòè âåðèôèêàöèèÂû÷èñëèòåëüíàÿ àïïàðàòóðà ñòàíîâèòñÿ äåøåâëå, àïðîèçâîäèòåëüíîñòü êîìïüþòåðîâ âîçðàñòàåò.Ïîÿâëÿþòñÿ íîâûå âîçìîæíîñòè àâòîìàòè÷åñêîãî ðåøåíèÿ âñåáîëåå è áîëåå ñëîæíûõ çàäà÷.Ïðîèñõîäèò óâåëè÷åíèå îáúåìîâ ïðîãðàììíîãî êîäà.Âñëåäñòâèå ýòîãî, óâåëè÷èâàåòñÿ âåðîÿòíîñòü ïîÿâëåíèÿîøèáîê, êîòîðûå ìîãëè áûòü âíåñåíû â ýòîò êîä êàê íà ýòàïåïðîåêòèðîâàíèÿ ïðîãðàììû, òàê è â õîäå ðåàëèçàöèè ïðîåêòà.Çà÷åì íóæíà ôîðìàëüíàÿ âåðèôèêàöèÿïðîãðàìì?4. Âîçðàñòàíèå òðóäîåìêîñòè âåðèôèêàöèèÑîâðåìåííàÿ òåõíîëîãèÿ ïðîåêòðîâàíèÿ è ðàçðàáîòêèïðîãðàìì ïîçâîëÿåò ïîâûñèòü ïðîèçâîäèòåëüíîñòü òðóäàïðîãðàììèñòîâ, è îíà ðàñòåò ïî÷òè íàñòîëüêî æå áûñòðî,íàñêîëüêî óâåëè÷èâàåòñÿ îáúåì ïðîãðàììíîãî îáåñïå÷åíèÿ.Íî ýòî îòíîñèòñÿ ëèøü ê ðàçðàáîòêå ïðîãðàììíîãî êîäà.Âåðèôèêàöèÿ ïðîãðàìì áåç ñïåöèàëüíûõ ñðåäñòâ ðèñêóåòîñòàâàòüñÿ ýêñòåíñèâíûì òðóäîì, òðåáóþùèì âñå íîâûõ èíîâûõ êâàëèôèöèðîâàííûõ ðàáîòíèêîâ, çàíèìàþùèõñÿèñêëþ÷èòåëüíî ïîèñêîì îøèáîê â ïðîãðàììíîì êîäå.Îäíàêî äàæå òàêîé ñïîñîá íå ïîçâîëÿåò óáåäèòåëüíîîáîñíîâàòü íàäåæíîñòü ïðîãðàììíîãî ïðîäóêòà.

Ñîâðåìåííàÿâåðèôèêàöèÿ ïðîãðàìì òðåáóåò ñîâñåì äðóãèõ ñðåäñòâ, ïðèïîìîùè êîòîðûõ ìîæíî áûëî áû íå òîëüêî îáíàðóæèâàòüîøèáêè, íî è óáåæäàòüñÿ â èõ îòñóòñòâèè.Îñíîâíûå ïîäõîäû ê çàäà÷å âåðèôèêàöèèÏðîñòåéøèå ìåòîäû ïðîâåðêè ïðàâèëüíîñòè ïðîãðàìì èìèêðîýëåêòðîííûõ ñõåì èìèòàöèîííîå ìîäåëèðîâàíèå èòåñòèðîâàíèå .ïîäâåðãàåòñÿ àáñòðàêòíàÿñõåìà èëè ïðîòîòèï,ïðèìåíÿåòñÿíåïîñðåäñòâåííî ê ñàìîìó ïðîäóêòó. ñëó÷àå ýëåêòðîííûõ ñõåì, íàïðèìåð, èìèòàöèîííîìóìîäåëèðîâàíèþ ïîäâåðãàåòñÿ ïðîåêò ðàçðàáàòûâàåìîé ñõåìû,òîãäà êàê òåñòèðîâàíèþ ïîäâåðãàåòñÿ ñàìà ìèêðîñõåìà. Âîáîèõ ñëó÷àÿõ â ýòèõ ìåòîäàõ îïðåäåëåííûå ñèãíàëû îáû÷íîââîäÿòñÿ â çàäàííûõ òî÷êàõ ñõåìû, à â äðóãèõ òî÷êàõ ñíèìàþòñîîòâåòñòâóþùèå ïîêàçàíèÿ.Ýòè ìåòîäû ìîãóò áûòü âåñüìà ýêîíîìè÷íû äëÿ âûÿâëåíèÿìíîãèõ îøèáîê.

Íî ïðîâåðèòüâîçìîæíûå âçàèìîäåéñòâèÿè îáîçðåòüìûñëèìûå ¾ñöåíàðèè¿, ïðèìåíÿÿ ëèøüìîäåëèðîâàíèå è òåñòèðîâàíèå, âðÿä ëè óäàñòñÿ.Èìèòàöèîííîìó ìîäåëèðîâàíèþòåñòèðîâàíèåÂÑÅÂÑÅÎñíîâíûå ïîäõîäû ê çàäà÷å âåðèôèêàöèèÔîðìàëüíûå ìåòîäû âåðèôèêàöèè ïðåäíàçíà÷åíû äëÿòîãî, ÷òî â ïðîåêòèðóåìîé ñèñòåìå ÍÅÒîøèáîê îïðåäåëåííîãî âèäà.Îñíîâíûå ïîäõîäû ê ôîðìàëüíîé ïðîâåðêå ïðàâèëüíîñòèñëîæíûõ óïðàâëÿþùèõ ñèñòåì (ïðîãðàìì è ïðîåêòîâìèêðîýëåêòðîííîé àïïàðàòóðû):1.(equivalence checking),2.(proof-theoretic approach),3.(model checking).äîêàçàòåëüñòâàïðîâåðêà ýêâèâàëåíòíîñòèäåäóêòèâíûé àíàëèçâåðèôèêàöèÿ ìîäåëåé ïðîãðàììÎñíîâíûå ïîäõîäû ê çàäà÷å âåðèôèêàöèèÏðîâåðêà ýêâèâàëåíòíîñòèÊàæäàÿ óïðàâëÿþùàÿ ñèñòåìà îïðåäåëÿåòñÿ äâóìÿñîñòàâëÿþùèìè:I óïðàâëÿþùàÿ ñõåìà Σ (ñèíòàêñè÷åñêàÿ õàðàêòåðèñòèêà),I âû÷èñëÿåìàÿ ôóíêöèÿ FΣ (ôóíêöèîíàëüíàÿõàðàêòåðèñòèêà).Çàäà÷à ïðîâåðêè ýêâèâàëåíòíîñòè : äëÿ çàäàííîé ïàðû ñõåì Σ1è Σ2 ïðîâåðèòü âûïîëíèìîñòü ñîîòíîøåíèÿFΣ1 = FΣ2 .Ïðîâåðêà ýêâèâàëåíòíîñòèÑèñòåìà íà êðèñòàëëå ïðè ïðîåêòèðîâàíèè ïðåäñòàâëÿåòñÿ íàðàçíûõ óðîâíÿõ àáñòðàêöèè.

Ìàðøðóò ïðîåêòèðîâàíèÿ Synopsisâêëþ÷àåò â ñåáÿ òðè îñíîâíûõ óðîâíÿ:1. Ñèñòåìíûé óðîâåíü :I Ýòàï 1: ñîçäàíèå àëãîðèòìè÷åñêîé ìîäåëè è ååâåðèôèêàöèÿ;I Ýòàï 2: ñîçäàíèå ìîäåëè óðîâíÿ òðàíçàêöèé (ìîäåëèìàêðîàðõèòåêòóðû) è åå âåðèôèêàöèÿ;I Ýòàï 3: ñîçäàíèå ò.í. "çîëîòîé ìîäåëè" ñèñòåìû íàêðèñòàëëå êàê òåõíè÷åñêîãî çàäàíèÿ äëÿ ïðîåêòèðîâàíèÿñõåìû.Ïðîâåðêà ýêâèâàëåíòíîñòè2. Ëîãè÷åñêèé , èëè âåíòèëüíûé , óðîâåíü, ñîñòîÿùèé èç ïÿòèýòàïîâ:I Ýòàï 1: ñîçäàíèå ñèíòåçèðóåìîé RTL-ìîäåëè ñèñòåìû íàêðèñòàëëå íà îäíîì èç ÿçûêîâ îïèñàíèÿ àïïàðàòóðû(Verilog, VHDL);I Ýòàï 2: ëîãè÷åñêàÿ âåðèôèêàöèÿ RTL-ìîäåëè ïîñðåäñòâîììîäåëèðîâàíèÿ;I Ýòàï 3: ôèçè÷åñêàÿ âåðèôèêàöèÿ ïîñðåäñòâîìïðîòîòèïèðîâàíèÿ;I Ýòàï 4: ñèíòåç â áàçèñå âåíòèëüíûõ ñõåì è àâòîìàòè÷åñêàÿãåíåðàöèÿ òåñòîâûõ ñòðóêòóð äëÿ êîíòðîëÿ ãîäíîñòè;I Ýòàï 5 ëîãè÷åñêàÿ è ôîðìàëüíàÿ âåðèôèêàöèÿ ñïèñêàöåïåé.3.

Òîïîëîãè÷åñêèé óðîâåíüÏðîâåðêà ýêâèâàëåíòíîñòèÒàêèì îáðàçîì, íà ïðîòÿæåíèè ïðîåêòèðîâàíèÿ ÑÁÈÑïîñëåäîâàòåëüíî ñòðîÿòñÿ 5 îïèñàíèé ñèñòåìû:I Àëãîðèòìè÷åñêîå îïèñàíèå ñèñòåìû (íà ÿçûêå C/C++);I Ìàêðîàðõèòåêòóðíîå îïèñàíèå ñèñòåìû (íà ÿçûêåSystem-C);I Ìèêðîàðõèòåêòóðíîå (RTL) îïèñàíèå ñèñòåìû (íà ÿçûêàõVHDL èëè Verilog);I Îïèñàíèå ñïèñêà öåïåé (íà ÿçûêàõ VHDL èëè Verilog è âôîðìàòàõ IEEE PDEF, DEF, LEF);I Îïèñàíèå òîïîëîãèè ÑÁÈÑ (â ôîðìàòå GDSII).Îñíîâíîé ïðèíöèï ìíîãîóðîâíåãî ïðîåêòèðîâàíèÿ:ôóíêöèîíàëüíîñòü áîëåå âûñîêîãî óðîâíÿ àáñòðàêöèè íåäîëæíà íàðóøàòüñÿ ïðè ïåðåõîäå íà áîëåå íèçêèé óðîâåíü.Ïðîâåðêà ýêâèâàëåíòíîñòèÂîçíèêàåò ñëåäóþùàÿ çàäà÷à âåðèôèêàöèè.Log 2Top : Ëîãè÷åñêàÿ ñõåìà Σ⇓Mod :Òîïîëîãè÷åñêàÿ ðåàëèçàöèÿ ñõåìû T ,Òîïîëîãè÷åñêàÿ ðåàëèçàöèÿ ñõåìû T⇓Top2Log :Óëó÷øåííàÿ òîïîëîãè÷åñêàÿ ðåàëèçàöèÿ ñõåìû T 0Òîïîëîãè÷åñêàÿ ðåàëèçàöèÿ ñõåìû T 0⇓Ëîãè÷åñêàÿ ñõåìà Σ0 .Çàäà÷à: ïðîâåðèòü âûïîëíèìîñòü ñîîòíîøåíèÿ FΣ = FΣ .Äëÿ ëîãè÷åñêèõ ñõåì ýòà çàäà÷à ñâîäèòñÿ ê ïðîáëåìåâûïîëíèìîñòè áóëåâûõ ôîðìóë SAT.0Äåäóêòèâíûé àíàëèçÒåðìèí äåäóêòèâíûé àíàëèç ïîäðàçóìåâàåò ïðèìåíåíèå àêñèîìè ïðàâèë âûâîäà äëÿ äîêàçàòåëüñòâà ïðàâèëüíîñòèôóíêöèîíèðîâàíèÿ ñèñòåìû.Íà ðàííèõ ýòàïàõ èññëåäîâàíèé ïî äåäóêòèâíîìó àíàëèçóîñíîâíîå âíèìàíèå óäåëÿëîñü îáåñïå÷åíèþ ïðàâèëüíîñòèðàáîòû êðèòè÷åñêè âàæíûõ ñèñòåì, è òàêèå äîêàçàòåëüñòâàñòðîèëèñü èñêëþ÷èòåëüíî âðó÷íóþ.Ñî âðåìåíåì ïîÿâèëèñü èíñòðóìåíòàëüíûå ñðåäñòâà (ïðóâåðû),ïîçâîëÿþùèå ïðèìåíÿòü ñèñòåìàòè÷åñêèé ïåðåáîð ñ öåëüþïîèñêà ðàçëè÷íûõ íàïðàâëåíèé ïîñòðîåíèÿ äîêàçàòåëüñòâà.Äåäóêòèâíûé àíàëèçÏðèíöèïû äåäóêòèâíîãî àíàëèçà ïðîãðàìì òàêîâû:1.

Ïðîãðàììà (ñõåìà) π âû÷èñëÿþò îòíîøåíèå Rπ ìåæäóäàííûìè âõîäå è íà âûõîäå ïðîãðàììû (ñõåìû);Äåäóêòèâíûé àíàëèçÏðèíöèïû äåäóêòèâíîãî àíàëèçà ïðîãðàìì òàêîâû:1. Ïðîãðàììà (ñõåìà) π âû÷èñëÿþò îòíîøåíèå Rπ ìåæäóäàííûìè âõîäå è íà âûõîäå ïðîãðàììû (ñõåìû);2. Òåêñò ïðîãðàììû (îïèñàíèå ñõåìû) ýòî ôîðìàëüíîåîïèñàíèå îòíîøåíèÿ Rπ íà ÿçûêå ïðîãðàììèðîâàíèÿ;Äåäóêòèâíûé àíàëèçÏðèíöèïû äåäóêòèâíîãî àíàëèçà ïðîãðàìì òàêîâû:1. Ïðîãðàììà (ñõåìà) π âû÷èñëÿþò îòíîøåíèå Rπ ìåæäóäàííûìè âõîäå è íà âûõîäå ïðîãðàììû (ñõåìû);2. Òåêñò ïðîãðàììû (îïèñàíèå ñõåìû) ýòî ôîðìàëüíîåîïèñàíèå îòíîøåíèÿ Rπ íà ÿçûêå ïðîãðàììèðîâàíèÿ;3. Òðåáîâàíèå (ñïåöèôèêàöèÿ) ïðàâèëüíîñòè Φ ïðîãðàììû ýòî îïèñàíèå òîãî îòíîøåíèÿ, êîòîðîå äîëæíàðåàëèçîâûâàòü ïðîãðàììà, íî íà äðóãîì ÿçûêå (èëè âäðóãîé ôîðìå);Äåäóêòèâíûé àíàëèçÏðèíöèïû äåäóêòèâíîãî àíàëèçà ïðîãðàìì òàêîâû:1. Ïðîãðàììà (ñõåìà) π âû÷èñëÿþò îòíîøåíèå Rπ ìåæäóäàííûìè âõîäå è íà âûõîäå ïðîãðàììû (ñõåìû);2.

Òåêñò ïðîãðàììû (îïèñàíèå ñõåìû) ýòî ôîðìàëüíîåîïèñàíèå îòíîøåíèÿ Rπ íà ÿçûêå ïðîãðàììèðîâàíèÿ;3. Òðåáîâàíèå (ñïåöèôèêàöèÿ) ïðàâèëüíîñòè Φ ïðîãðàììû ýòî îïèñàíèå òîãî îòíîøåíèÿ, êîòîðîå äîëæíàðåàëèçîâûâàòü ïðîãðàììà, íî íà äðóãîì ÿçûêå (èëè âäðóãîé ôîðìå);4. Ïðîâåðêà ïðàâèëüíîñòè ïðîãðàììû π îòíîñèòåëüíîñïåöèôèêàöèè Φ ýòî äîêàçàòåëüñòâî òîãî, ÷òî Rπ ⇒ Φ .Äåäóêòèâíûé àíàëèçÏðèíöèïû äåäóêòèâíîãî àíàëèçà ïðîãðàìì òàêîâû:1. Ïðîãðàììà (ñõåìà) π âû÷èñëÿþò îòíîøåíèå Rπ ìåæäóäàííûìè âõîäå è íà âûõîäå ïðîãðàììû (ñõåìû);2. Òåêñò ïðîãðàììû (îïèñàíèå ñõåìû) ýòî ôîðìàëüíîåîïèñàíèå îòíîøåíèÿ Rπ íà ÿçûêå ïðîãðàììèðîâàíèÿ;3. Òðåáîâàíèå (ñïåöèôèêàöèÿ) ïðàâèëüíîñòè Φ ïðîãðàììû ýòî îïèñàíèå òîãî îòíîøåíèÿ, êîòîðîå äîëæíàðåàëèçîâûâàòü ïðîãðàììà, íî íà äðóãîì ÿçûêå (èëè âäðóãîé ôîðìå);4.

Ïðîâåðêà ïðàâèëüíîñòè ïðîãðàììû π îòíîñèòåëüíîñïåöèôèêàöèè Φ ýòî äîêàçàòåëüñòâî òîãî, ÷òî Rπ ⇒ Φ .Îáû÷íî ñïåöèôèêàöèÿ çàäàåòñÿ ïðåäóñëîâèåì ϕ ,îïèñûâàþùèì ìíîæåñòâî äàííûõ, êîòîðûå ìîãóò ïîñòóïàòü íàâõîä ïðîãðàììû, è ïîñòóñëîâèåì ψ , îïèñûâàþùèì îòíîøåíèåìåæäó âõîäíûìè è âûõîäíûìè äàííûìè.Äåäóêòèâíûé àíàëèçÄåäóêòèâíûé àíàëèç îêàçàë çíà÷èòåëüíîå âëèÿíèå íà ïîäõîäûê ðàçðàáîòêå ïðîãðàììíîãî îáåñïå÷åíèÿ (íàïðèìåð, ïîíÿòèåèíâàðèàíòà çàèìñòâîâàíî èç èññëåäîâàíèé ïî äåäóêòèâíîìóàíàëèçó).Òåì íå ìåíåå, îí çàíèìàåò ìíîãî âðåìåíè è ìîæåò áûòüîñóùåñòâëåí òîëüêî ýêñïåðòàìè, îáëàäàþùèìè çíàíèÿìè âîáëàñòè ëîãè÷åñêîãî âûâîäà è èìåþùèìè íåìàëûéïðàêòè÷åñêèé îïûò.

Характеристики

Список файлов лекций