Formal methods for test and reliability
Authors: Δεληγιάννης Νικόλαος 
Published: November 2024

Στο ταχέως εξελισσόμενο τοπίο της νανοτεχνολογίας, όπου οι καινοτομίες υπόσχονται πρωτοποριακές εξελίξεις σε διάφορους κλάδους, η διασφάλιση της αξιοπιστίας και της ασφάλειας των ψηφιακών κυκλωμάτων καθίσταται υψίστης σημασίας. Αν και αυτό ισχύει για την ευρεία κατηγορία των εμπορικών έτοιμων προϊόντων, γίνεται σημαντικά πιο εμφανές όταν εξετάζονται τομείς ή βιομηχανικοί κλάδοι, όπως η αυτοκινητοβιομηχανία, η αεροπορία, οι σιδηρόδρομοι και ο βιοϊατρικός τομέας, που εμπίπτουν στην κατηγορία των κρίσιμων για την ασφάλεια εφαρμογών. Σε αυτές τις περιπτώσεις, η πιθανότητα ένα σφάλμα να ενεργοποιηθεί και να μεταδοθεί σε αστοχία που θα έθετε σε κίνδυνο ανθρώπινες ζωές ή θα προκαλούσε περιβαλλοντική ζημία θα πρέπει να αξιολογείται προσεκτικά και να διατηρείται κάτω από προκαθορισμένα όρια. Για να επιτευχθεί αυτό το αποτέλεσμα, οι κατασκευαστές πρέπει να συμμορφώνονται με αυστηρά πρότυπα και διαδικασίες ασφαλείας που επιβάλλουν αυστηρά όρια κάλυψης και ολοκληρωμένα πρωτόκολλα δοκιμών. Από το τέλος της κατασκευής έως και τη φάση της εγκατάστασης στο πεδίο, κάθε ολοκληρωμένο κύκλωμα (IC) υποβάλλεται σε διάφορες διαδικασίες δοκιμών για να διασφαλιστεί ότι πληροί αυστηρά πρότυπα ποιότητας, λειτουργεί αξιόπιστα εντός καθορισμένων παραμέτρων και παραμένει ανθεκτικό σε διάφορες περιβαλλοντικές συνθήκες καθ' όλη τη διάρκεια της λειτουργικής του ζωής. Οι τεχνικές Design-for-Testability (DfT) ενσωματώνονται κατά τις φάσεις σχεδιασμού των ηλεκτρονικών κυκλωμάτων για τη βελτίωση της διαδικασίας δοκιμής.Ωστόσο, παρά την παρουσία ισχυρών βοηθητικών προγραμμάτων αυτοματοποίησης ηλεκτρονικού σχεδιασμού (EDA), όπως τα automatic test pattern generation (ATPG) εργαλεία, που προορίζονται για χρήση παράλληλα με κυκλώματα συμβατά με DfT κατά τη διάρκεια των δοκιμών, η αδιάκοπη εξέλιξη της τεχνολογίας επιφέρει ταχύτερα, μικρότερα και πυκνότερα κυκλώματα. Αυτή η εξέλιξη καθιστά ορισμένα βοηθητικά προγράμματα ανεπαρκή, καθώς η πολυπλοκότητα της διαδικασίας δοκιμής αυξάνεται σημαντικά, όπως συμβαίνει με το Burn-In (BI) τέστ. Το Burn-In, ένα πανταχού παρόν βήμα στην αλυσίδα δοκιμών για προϊόντα που προορίζονται για χρήση σε κρίσιμους τομείς ασφαλείας, διεξαγόταν, μέχρι πρόσφατα, με την παραδοσιακή στατική μορφή του. Παρά την αποτελεσματικότητά της, η στατική δοκιμή BI κατέστη λιγότερο αποτελεσματική για τις νεότερες, πυκνότερες τεχνολογίες, καθώς διαπιστώθηκε ότι στη στατική της μορφή δεν εξασκούσε πλήρως όλα τα εσωτερικά μέρη των ολοκληρωμένων κυκλωμάτων. Ως εκ τούτου, εξελίχθηκε σε νέες δυναμικές μορφές, όπου τα διανύσματα καταπόνησης εφαρμόζονται με εσωτερικό τρόπο επιπλέον της εξωτερικής αύξησης της θερμοκρασίας και της τάσης. Ωστόσο, η δημιουργία κατάλληλου κώδικα που προκαλεί καταπόνηση είναι μια δαπανηρή και επίπονη εργασία για τους μηχανικούς, λόγω της έλλειψης αυτοματισμού που θα βοηθούσε τη διαδικασία της δημιουργίας τους. Ένας άλλος τομέας που θα μπορούσε να επωφεληθεί σημαντικά από την αυτοματοποίηση είναι το in-field τεστ. Το in-field τέστ επιτρέπει την ανίχνευση σφαλμάτων ή ανωμαλιών που μπορεί να εμφανιστούν με την πάροδο του χρόνου. Η έγκαιρη ανίχνευση πιθανών προβλημάτων επιτρέπει την προληπτική συντήρηση ή τη λήψη διορθωτικών μέτρων, μειώνοντας τον κίνδυνο αποτυχίας του συστήματος σε κρίσιμες καταστάσεις. Ωστόσο, το έργο της ανάπτυξης κατάλληλων βιβλιοθηκών, Software Test Libraries (STL), για τέτοια σενάρια είναι συνήθως ένα έργο που απαιτεί μεγάλη χειρωνακτική προσπάθεια από την πλευρά του μηχανικού. Στην πραγματικότητα, όχι μόνο το τέστ πρέπει να λαμβάνει υπόψη παραμέτρους όπως ο χρόνος εφαρμογής και το αποτύπωμα μνήμης, αλλά και να αποφεύγει τη στόχευση σε μη ελέγξιμα σφάλματα του σχεδιασμού. Αυτό σημαίνει ότι η δοκιμή πρέπει να εστιάζει μόνο σε εκείνα τα σφάλματα που είναι σε θέση να προκαλέσουν αποτυχία στο σενάριο λειτουργίας, αγνοώντας εκείνα που δεν μπορούν να προκαλέσουν καμία (κρίσιμη) αποτυχία. Η παρούσα διδακτορική διατριβή προτείνει λύσεις, βασισμένες σε Τυπικές Μεθόδους, Formal Methods (FM), που αντιμετωπίζουν τα προαναφερθέντα θέματα δοκιμών. Το χειρόγραφο οργανώνεται σε τρία κύρια μέρη. Το αρχικό μέρος παρέχει μια εισαγωγή και επισκόπηση της επιτακτικής ανάγκης για δοκιμές και αξιοπιστία στη σύγχρονη ψηφιακή εποχή. Εμβαθύνει στους διακριτούς τομείς δοκιμών που αποτελούν το επίκεντρο της παρούσας διατριβής. Το δεύτερο μέρος περιλαμβάνει τις τρεις κύριες συνεισφορές της διατριβής. Αρχικά παρουσιάζεται μια ενότητα που προτείνει λύσεις βασισμένες στις FM για τη δημιουργία δυναμικών διανυσμάτων καταπόνησης που προορίζονται για το BI. Αυτές οι μέθοδοι εξετάζουν διάφορες μετρικές μεταγωγικής δραστηριότητας και η αποτελεσματικότητά τους παρουσιάζεται με την εφαρμογή τους σε κλιμακωτούς επεξεργαστές. Η δεύτερη συνεισφορά αφορά λύσεις βασισμένες σε FM που στοχεύουν στον εντοπισμό λειτουργικά μη ελέγξιμων σφαλμάτων σύμφωνα με τα μοντέλα σφαλμάτων stuck-at και cell-aware. Τέλος, η τελευταία συνεισφορά αφορά μεθοδολογίες που βοηθούν στη δημιουργία STL για μικροεπεξεργαστές και GPUs. Στο τελευταίο μέρος παρατίθενται τα συμπεράσματα της συνολικής εργασίας.