שמונה הוכחות פורמליות ירוקות הפכו לחמש הניתנות להגשה כשביצעתי ביקורת על טענות ה-SystemVerilog

צפיתי בלוח אימות פורמלי סינתטי מדווח על 8/8 PROVEN, ולאחר מכן צפיתי בביקורת שלו מאשרת רק 5/8 כ-TRUSTWORTHY. התהפכות זו היא הבסיס ל-Proof Firewall, הדגמת ההפעלה שלנו למשילות של טענות SystemVerilog‏ (SVA) שנוצרו ב-AI, והיא שינתה את הרף שאני מצפה מהוכחה ירוקה לעמוד בו לפני שהיא מגיעה לסקירת חתימה (sign-off) ל-tape-out.

בניתי את הלוח עם מאפיינים שנכתבו עבור תרחישי בדיקה (fixtures) כמאפיינים ש״נכתבו על ידי LLM״ על גבי בורר (arbiter) סינתטי, צינור עיבוד (pipeline) דו-שלבי וחציית תחומי שעון (CDC), משום שהמקרה הלא נוח ראוי להיראות. טענה (assertion) יכולה להיראות מכובדת לחלוטין בפנקס המאפיינים. מנוע פורמלי יכול להחזיר תוצאה ירוקה. עם זאת, ייתכן שהגרירה הלוגית (implication) מעולם לא נדרשה לבצע עבודה כלשהי, או שהיא תמשיך לעבור בהצלחה גם לאחר שהתנהגות התכן הרלוונטית נשברה. התייחסתי למילה PROVEN כיעד סופי. בניית ההדגמה הזו חייבה אותי להתייחס אליה כאל תחילתה של בדיקת ראיות.

הדגמת Proof Firewall אינה מחליפה מנוע פורמלי, אינה קולטת RTL אמיתי ואינה קוראת ל-LLM חי בנתיב ברירת המחדל שלה. היא במכוון קטנה יותר וניתנת יותר לבדיקה מעמיקה: בודק מודלים (model checker) מפורש-מצבים ב-Python טהור מעריך ייצוג ביניים (IR) של מערכת מעברים סינתטית, ולאחר מכן שער משילות בודק נגישות תנאי קודם (antecedent reachability), קטילת מוטציות (mutation kills) וקונוס השפעה (COI). הפלט הוא או סיבה להגיש תעודת הדגמה חתומה או סיבה להשהות את התוצאה לבדיקה אנושית.

התחלתי עם הסוג הלא נכון של ירוק

אני זוכר שהגרסה הראשונה של הלוח הרגישה מרגיעה בדיוק משום שהייתה כה נקייה. שמונה מאפיינים, שמונה תגים ירוקים ותצוגת תהליך בסיסי (bare-flow) שגרמה לעבודה להיראות גמורה. האינסטינקט הראשוני שלי היה לגרום להדגמה להסביר טוב יותר את התוצאה הנקייה הזו. חשבתי שהמשימה ההנדסית הייתה הצגה: להציף את ההוכחות, להציג את הטענות, ולהפוך את לוח המחוונים לקל יותר לנתינת אמון. התוצאה הירוקה הייתה אמיתית, אך היא ענתה על שאלה קטנה יותר מזו שסוקר צריך לשאול.

לאחר מכן העברתי את אותם שמונה מאפיינים דרך הבדיקות ששיחת הגשה (filing) למעשה דורשת. האם התנאי הקודם (antecedent) התממש אי פעם כאמת? האם הטענה הייתה מתנגדת לו חלק רלוונטי בתכן היה משתנה? האם היא מגבילה COI משמעותי? שאלות אלו מחמיאות פחות מתג ירוק משום שהן שואלות מה ההוכחה הרוויחה בזכות, ולא רק מה הפותר (solver) החזיר.

נאלצתי לזנוח את המסגור הראשון של המבנה. מסך שהציג 8/8 PROVEN היה מבט מדויק על קו הבסיס של התהליך הגולמי, אך הוא היה חלקי כסיפור חתימה (sign-off). לאחר ביקורת חומת האש, לאותו לוח סינתטי קבוע יש חמש תוצאות TRUSTWORTHY, תוצאת VACUOUS אחת ושתי תוצאות WEAK. שלושת הנותרים אינם מתוייגים מחדש כהצלחה. הם מושהים יחד עם הראיות שמסבירות מדוע. תווית הוכחה והחלטת הגשה הן תוצרים שונים.

בחרתי את המילה ״משילות״ (governance) בקפידה כאן. הבדיקות הדטרמיניסטיות של ההדגמה הופכות את החלטת ההגשה לניתנת לבדיקה. מחבר SVA אופציונלי עשוי להציע טענה, אך בודק המודלים ושער המדיניות קובעים את פסק הדין. סוכנים מייעצים, קוד מחליט. ניסיתי להפוך את השער לברור מספיק כדי שהתוצאה השלילית תהיה מועילה ולא סתם מביכה. תוצאה מושהית זקוקה לסיבה שמהנדס אימות יכול לבדוק, לשחזר ולערער עליה.

ARB3 הפך את הבעיה לבלתי אפשרית להתעלמות

מצאתי את הכשל הברור ביותר ב-ARB3, מאפיין הבורר הסינתטי assert (g0 && g1) |-> (turn == 0). בתהליך הגולמי, הוא ירוק. כשפתחתי את צורת הגל (waveform) וראיות הנגישות שלו, התנאי הקודם (antecedent) g0 && g1 היה בלתי מושג באותו בורר סינתטי. הגרירה הלוגית (implication) הוכחה רק במובן הצר שלפיו היא מעולם לא נאלצה לתת דין וחשבון על המצב שתיארה. התנאי הקודם לעולם אינו מופעל.

קל לומר את ההבחנה הזו, אך קשה לזכור אותה כאשר לוח המחוונים של האימות מלא בירוק. בתחילה קראתי את הגרירה הלוגית כטענה על התנהגות הבורר. תוצאת הנגישות שינתה את מה שהבטתי בו. זו הייתה טענה שתנאי ההפעלה שלה מעולם לא התרחש. כינוי מצב זה כ-VACUOUS מועיל יותר מאשר שמירה על תווית ירוקה, מכיוון שהוא מכוון את הסוקר לעבר ההנחה או התמריץ (stimulus) שהפכו את ההוכחה לריקה מתוכן.

המשכתי לחזור לפאנל זה בזמן שעבדתי על תוויות המדיניות. VACUOUS עשוי להישמע כמו תוצאה קשה עד ששוקלים את החלופה. אם רשומת חתימה (sign-off) שומרת הוכחה מבלי לתעד שהתנאי הקודם שלה לעולם אינו מופעל, הסקירה קיבלה מסקנה ללא התנאי שמעניק לה משמעות. הרשומה הטובה יותר היא זו שמבהירה את המגבלה באופן מפורש ומשאירה לאדם משהו קונקרטי לחקור. רשומת הנגישות הזו שייכת למקום שלצד פסק הדין.

הייתי צריך גם להתנגד להתייחסות לריקנות (vacuity) כאזהרה קוסמטית בלבד. אם המאפיין נועד להגביל תנאי בוררות, התנהגות הפעלה בלתי מושגת היא ראיה מרכזית לשאלה האם המאפיין הפעיל את ההתנהגות המיועדת. לוח המחוונים לא צריך לבקש מסוקר להסיק זאת מתוצאה ירוקה. עליו לשמר את ממצא הנגישות, לנתב את התוצאה אל מחוץ לנתיב התעודה, ולהפוך את פעולת הסקירה הבאה לברורה מאליה.

ההקשר התעשייתי חידד עבורי את הסיכונים. מחקר Wilson Research Group / Siemens EDA לשנת 2024 המצוטט במפרט ההדגמה מדווח על 14% הצלחה בסיליקון ראשון (first-silicon success). זו אינה מדידה של Veriprajna, ולוח סינתטי זה אינו טוען להסביר נתון זה. הדבר אכן גורם לי להיות פחות מוכן להתייחס למצב נעים בלוח המחוונים כראיה בפני עצמו.

מאפיין צינור העיבוד שרד את השבירה שציפיתי שיתפוס

נתקלתי בכשל השני בזמן שבדקתי את PIPE3, מאפיין סינתטי של צינור עיבוד (pipeline) דו-שלבי: assert v2 |-> (s2 == s2). רציתי דוגמה תמציתית לטענה שנקראה בצורה הגיונית מספיק כדי לחמוק בסקירה שטחית. התנאי הנגרר (consequent) הוא טאוטולוגיה. הוא אומר ש-s2 שווה לעצמו. התנאי הנגרר אינו מגביל דבר.

הצעד החשוב בהדגמה אינו רק זיהוי הטאוטולוגיה בטקסט. שער המשילות מזריק מוטציות תכן נקודתיות רלוונטיות ושואל האם המאפיין קוטל אותן. עבור מקרה הצינור החלש המוצג, PIPE3 מתעד תוצאת קטילת מוטציות של 0/6. המאפיין שורד את הגרסאות השבורות הרלוונטיות. זו הסיבה שהמדיניות מקצה WEAK במקום לאפשר לתוצאת ה-PROVEN הגולמית לעמוד כראיית הגשה. תוצאת המוטציה בודקת רגישות שימושית.

למדתי משהו לא נוח מהניסיון לגרום לדוגמה זו להרגיש פחות ברורה מאליה. אדם יכול לקרוא s2 == s2 ולפסול זאת במהירות. חולשות רבות לא יכריזו על עצמן בצורה כה גלויה. זו הסיבה שלא רציתי שההדגמה תסתמך על כך שהמפעיל יבחין במחרוזת חשודה. התוצר המועיל הוא התהליך: נגישות (reachability), מבחן קטילת מוטציות רלוונטי, COI והחלטת מדיניות המתעדת את הסיבה שלה.

הגעתי להבנה שבדיקת המוטציות היא דרך ממושמעת לסרב לקריאה נוחה מדי של הוכחה. המטרה אינה לייצר כשל דרמטי. היא לשאול האם המאפיין היה מבחין בשינוי מקומי רלוונטי בהתנהגות שהוא אמור להגביל. כאשר הוא אינו מבחין בכך, התוצאה אומרת לסוקר משהו מעשי: טענה זו זקוקה לחיזוק או לנתיב סקירה שונה לפני שתוכל לתמוך ברשומת החתימה (sign-off).

זו גם הסיבה לכך שהבנצ'מרק של ההדגמה זקוק לתיאור מדויק וצר. הרצת ה-python -m backend.bench המקומית משיגה ציון של 18/18 מול סט טענות סינתטי קבוע ומתוייג, ומזהה 6 הוכחות שקו הבסיס הלא-מבוקר של ההדגמה עצמה היה מאשר כחותמת גומי. מספרים אלה הם בדיקת שחזוריות עבור תרחישי הבדיקה המתוייגים של הדגמה זו. הם אינם קצב ייצור, טענה כללית לגבי טענות שנכתבו על ידי AI, או השוואה לכלים פורמליים מסחריים.

הפסקתי לנסות לגרום לשער להיראות מתירני

עמדה בפניי בחירה תכנונית לאחר תוצאות הביקורת הראשונות: לרכך את פסקי הדין המושהים כדי שהלוח ירגיש אופטימי יותר, או לתת ללוח לסרב לאשר את מה שאינו יכול להגן עליו. בחרתי באפשרות השנייה מכיוון שסקירת חתימה (sign-off) אמיתית זקוקה ליכולת להבחין בין הוכחה מלאה להוכחה חסומה (bounded), בין תנאי קודם בלתי מושג למאפיין בעל משמעות, ובין בדיקה חלשה לבדיקה המגיבה להתנהגות שבורה רלוונטית. השהיה היא תוצאת סקירה, לא דרך ללא מוצא.

בחירה זו באה לידי ביטוי באוצר המילים של המדיניות. TRUSTWORTHY זוכה בתעודת ההדגמה החתומה. BOUNDED-PROVEN, VACUOUS, WEAK, DEAD, ו-VIOLATED משמרים סיבות שונות להשהיית אותה תעודה או להסלמת התוצאה. ברכיב הבדיקה של CDC, למשל, המאפיין החזק יותר assert (req && !ack) |-> ##1 req מקבל את הסטטוס VIOLATED ומייצר צורת גל קונקרטית של דוגמה נגדית (counterexample) סינתטית. הוא ממחיש מחלקת כשלים של עסקאות אבודות (lost-transaction) או כשל CDC. הוא אינו מעיד דבר על שבב של לקוח.

אינני רואה בכך הצעה להחלפת המנוע הקיים של צוות אימות. הכיוון בסביבת ייצור אינו תלוי במנוע מסוים (engine-agnostic): להציב שער סביב תהליך עבודה פורמלי קיים, ולאחר מכן להפוך את קריטריוני הקבלה שלו לניתנים לבדיקה. מתאמים למנועים אמיתיים וקליטת RTL נדחים בהדגמה זו. הגבול המודגם צר במכוון. גבול זה חשוב מכיוון שהוא שומר על הטענה פרופורציונלית למה שרץ בפועל.

עכשיו אני רוצה את הקבלה לצד פסק הדין

אני ממשיך לחשוב על התוצר שפגישת חתימה (sign-off) זקוקה לו כאשר מחבר הטענות נעזר ב-AI. זה אינו ציון ביטחון (confidence score) מהמחבר. זוהי רשומה שמציינת אילו בדיקות רצו, מה הייתה תוצאת הנגישות, אילו מוטציות נקטלו, מה הכיל ה-COI, ומדוע המדיניות אישרה או השהתה את ההסמכה. הסקירה זקוקה לראיות שניתן לפתוח מחדש.

זה מה שההדגמה מייצאת בקובץ signoff_certificate.json: פסקי דין לכל מאפיין, נגישות, תוצאות מוטציות, COI, רשומות של דוגמאות נגדיות במידת הצורך, ושדה SHA-256. בניתי את התעודה כרשומת הדגמה משום שסוקר צריך להיות מסוגל לשחזר את ההחלטה מבלי לקבל תג ירוק מתוך אמונה עיוורת. תעודה צריכה לשמר את הנתיב לפסק הדין שלה.

ואם אתם מעדיפים לראות זאת במקום לקרוא את התיאור שלי, הנה הדבר כולו רץ מקצה לקצה.

הפכתי את ההדגמה לניתנת להרצה כדי שניתן יהיה לבדוק את המהפך מ-8/8 ל-5/8 במקום לחזור עליו כסיסמה. התוצאה שאני לוקח ממנה היא צנועה אך עמידה: הוכחה שראויה להגשה נושאת ראיות למה שהיא הגבילה, למה שהיא שרדה, ולסיבה שבגללה מישהו יכול להסתמך עליה. ירוק נותר שימושי. הוא פשוט זקוק לרשומה שתאפשר לסוקר הבא להחליט האם הוא ראוי להמשיך הלאה.