כמדען המחשבים הישראלי מאוניברסיטת רייס מתאר כיצד שיטות אימות שהתפתחו לכלי עבודה בתעשיית השבבים מקבלות חשיבות מחודשת בעידן הקוד האוטומטי, ומזהיר מפני העדפת מהירות ומחיר על פני אמינות
היכולת של בינה מלאכותית לכתוב קוד במהירות מעבירה את מרכז הכובד של הפיתוח אל שאלה ותיקה: איך יודעים שהתוצר עושה את מה שהוא אמור לעשות? לדברי פרופ׳ משה ורדי (Moshe Y. Vardi), מדען מחשבים ישראלי מאוניברסיטת רייס ביוסטון, זו אחת הסיבות לכך ששיטות האימות הפורמלי, שמילאו תפקיד חשוב בתכנון שבבים, זוכות כעת לעניין מחודש גם בעולם התוכנה.
״פעם הקידוד היה החלק הקשה. היום יש מלא קוד, אבל נשאר החלק היותר קשה: איך אתה יודע שהקוד עושה מה שהוא צריך לעשות?״, אומר ורדי בשיחה עם אבי בליזובסקי. ארבעים שנה אחרי המאמר שפרסם עם פייר וולפר (Pierre Wolper) על אימות אוטומטי של תוכניות באמצעות אוטומטים, הוא רואה הזדמנות חדשה לתחום שבו עסק במשך עשורים.
ורדי, זוכה פרס גדל לשנת 2000 עם וולפר, אינו מציע לראות בכתיבת קוד אוטומטית סוף לתהליך ההנדסי. מבחינתו, הקוד שנוצר הוא תחילתה של בעיית בקרת איכות: צריך להגדיר מה מצופה ממנו, לבדוק את התנהגותו ולברר אילו הבטחות באמת אפשר לתת לגביו.
לתכנן עיר עד רמת החלון הבודד
כדי להסביר את מורכבותו של תכנון שבב, ורדי משתמש בדימוי של תכנון עיר שלמה. ״תחשוב שאתה מתכנן את העיר ניו יורק ברמה של כל חלון בודד״, הוא אומר. המורכבות מחייבת דיוק שקשה לבני אדם לשמור עליו לאורך תהליך התכנון.
ורדי כתב את תוכנית המחשב הראשונה שלו בפורטרן ב־1970. כבר אז, הוא מספר, התברר לו הפער בין התחושה שהתוכנית כתובה נכון לבין התוצאה בפועל. אדם שמקבל הוראות יכול לעיתים להבין שהדובר התכוון למשהו אחר ולתקן את הטעות בעצמו. מחשב מבצע את ההוראות כפי שנכתבו.
בדיקות באמצעות הרצת המערכת על קלטים שונים הן חלק חיוני מהפיתוח. אבל בתכנון שבבים, מספר המצבים וצירופי האירועים עצום. לדבריו, אי אפשר לבנות את הביטחון בתקינות המערכת רק על ניסיון להריץ כל תרחיש אפשרי.
מכאן הצורך בשיטות משלימות, המבוססות על תיאור מתמטי של ההתנהגות הנדרשת ועל בדיקה אלגוריתמית שלה. הן מאפשרות לבדוק תכונות מוגדרות של התכנון ביחס למודל ולדרישות שנוסחו, בלי להסתפק באוסף דוגמאות שעברו בדיקה.
להפריד בין מה שהשבב צריך לעשות לבין איך עושים זאת
ההבחנה המרכזית בהסבר של ורדי היא בין מימוש לבין מפרט. שפת תכנות או שפת תיאור חומרה מתארת כיצד המערכת פועלת. מפרט הצהרתי מתאר את התכונות שהמערכת צריכה לקיים.
לדוגמה, אפשר לדרוש שמערכת לא תגיע למצב אסור, או שבקשה תקבל בסופו של דבר תגובה. הדרישה מתארת את ההתנהגות הרצויה, בלי להכתיב את כל צעדי המימוש. הגדרתה באופן מדויק מאפשרת לבדוק אם התכנון אכן עומד בה.
ורדי מדגיש שלא הוא המציא את הרעיון של אימות פורמלי. הוא מצביע על תרומתו של אמיר פנואלי (Amir Pnueli), שהביא את לוגיקת הזמן אל מדעי המחשב. לוגיקה זו מאפשרת לתאר תכונות של התנהגות לאורך רצף אירועים, ולכן התאימה לבדיקת מערכות הפועלות לאורך זמן.
תרומתם של ורדי וולפר הייתה בפיתוח גישה אלגוריתמית המבוססת על תורת האוטומטים. במאמרם מ־1986 הראו כיצד אפשר לתרגם דרישות לוגיות לייצוג שעליו ניתן לבצע בדיקות חישוביות. ורדי מסביר זאת באמצעות ההקבלה למהדר: כשם שמתרגמים שפה עילית לייצוג שהמחשב יכול לעבד, אפשר לתרגם גם דרישות ברמה גבוהה למבנים המתאימים לאימות.
מהמאמר המתמטי לכלי עבודה בתעשיית השבבים
המעבר מן הרעיון לכלי תעשייתי לא התרחש מיד. בתחילה, מספר ורדי, הייתה זו תוצאה מתמטית. בהמשך פותחו דרכי מימוש, והוא עבד במשך שנים עם אינטל כדי להביא את הגישה לרמת כלי פיתוח ולסייע בהפיכת שפות לתיאור דרישות לשפות המתאימות לתעשייה.
לדבריו, התקינה הייתה חלק חשוב בתהליך. כאשר שפה נשארת כלי פנימי של חברה אחת, השימוש בה מוגבל לסביבה מסוימת. תקן מאפשר לספקי כלי תכנון ואימות לתמוך בה ולמשתמשים להסתמך על תשתית רחבה יותר.
״זה מתחיל בפילוסופיה ונגמר בכלי עבודה״, הוא מתאר את המסלול. עבור קוראי תעשיית השבבים, זהו גם סיפור על הזמן שנדרש לרעיון יסודי להגיע לתהליכי עבודה ולכלי EDA, אוטומציה של תכנון אלקטרוני.
האימות הפורמלי אינו הבטחה גורפת שאין במערכת שום טעות. תוקף המסקנה תלוי במודל שנבדק, בדרישות שנוסחו ובהנחות העבודה. היתרון הוא האפשרות לתת תשובה שיטתית ומדויקת לשאלות שהוגדרו מראש.
מדוע היה קל יותר להצדיק את ההשקעה בחומרה
ורדי מסביר כי שיטות פורמליות נתפסו לאורך שנים כטובות אך יקרות. בתעשיית השבבים היה קל יחסית להצדיק את ההשקעה, משום שטעות שהתגלתה אחרי הייצור עלולה להיות קשה ויקרה לתיקון.
תוכנה אפשר לעיתים לעדכן באמצעות תיקון או גרסה חדשה. בחומרה, שינוי בתכנון עשוי לחייב מהלך מורכב הרבה יותר. ורדי מזכיר את פרשת טעות החילוק במעבדי פנטיום של אינטל כדוגמה למחיר של שגיאת תכנון.
לפי התיעוד ההיסטורי של אינטל, הפרשה התרחשה ב־1994 והובילה להחלפת מעבדים ולהוצאה חשבונאית של 475 מיליון דולר. הדוגמה ממחישה כיצד תקלה בחישוב, גם כשהיא מתגלה בתנאים מסוימים, יכולה להפוך לאירוע עסקי משמעותי.
הטענה הרחבה של ורדי היא שהשיקול אינו רק כמה עולה האימות. צריך להביא בחשבון גם את המחיר של תקלה ואת הקושי לתקן מערכת שכבר נמצאת אצל לקוחות.
AI כותבת את הקוד — ואולי תסייע גם לבדוק אותו
הבינה המלאכותית יוצרת כעת מצב שבו אפשר להפיק יותר קוד בפחות זמן, אך הצורך בבקרה אינו מצטמצם בהתאם. ורדי מצביע על הפער בין שטף הייצור לבין היכולת של צוותים לבדוק את התוצרים.
הוא מתאר עניין גובר בשימוש בשיטות פורמליות לבדיקת קוד שנוצר ב־AI. לצד זאת, עולה האפשרות להשתמש ב־AI גם כדי להוזיל את עבודת האימות עצמה. השאלה איננה רק האם מודל יכול לכתוב תוכנית, אלא כיצד אפשר לשלב אותו בתהליך שמפיק תוצאה אמינה ובת־בדיקה.
אין בכך הנחה שאפשר לקבל את תשובתו של מודל שני כהוכחה שהמודל הראשון צדק. במסגרת אימות פורמלי נדרשים מפרט ושיטת בדיקה שנותנים משמעות מוגדרת למסקנה. היכולת של AI לסייע בתהליך והיכולת לאמת את התוצאה הן שתי שאלות הקשורות זו בזו.
ורדי מספר שבכנס על שיטות פורמליות בפורטוגל חש תחושה של שינוי במעמד התחום: ״הרגע שלנו הגיע״. תחום שנחשב לעיתים יקר ומיוחד מקבל, לדבריו, תשומת לב רחבה יותר כאשר ייצור הקוד נעשה מהיר ונפוץ.
מהירות, עלות וחוסן
את שאלת האימות הוא מציב בתוך מתח רחב יותר בין יעילות לחוסן. השוק מתגמל פיתוח מהיר ועלויות נמוכות, אבל מערכות שעליהן נשענים משתמשים וארגונים צריכות להמשיך לתפקד גם כשהתנאים אינם אידיאליים.
״בסוף אנחנו צריכים מערכות שיהיו אמינות״, הוא אומר. היכולת להפיק קוד מהר יכולה להיות מועילה מאוד, אך היא אינה פוטרת מהצורך לברר אם הקוד מתאים לדרישות ואם ניתן להסתמך עליו.
מבחינת תעשיית השבבים, המסר הוא שידע שנצבר במשך עשורים על ניסוח דרישות ואימות התנהגות מקבל משמעות נוספת. כאשר AI מאיצה את שלב יצירת התכנון או הקוד, שאלת התקינות נשארת חלק מרכזי מהעבודה ההנדסית.
— סוף הכתבה —
מקור: שיחה של אבי בליזובסקי עם פרופ׳ משה ורדי, 4 באוקטובר 2026.
רקע מקצועי: הגישה לאימות אוטומטי של ורדי וולפר, 1986: https://www.cs.rice.edu/CS/Logic/Games/Research/index-bib.html
אימות הפרט ההיסטורי על פנטיום: https://timeline.intel.com/1994/pentium%27s-flaw
