Γνωρίζετε με βεβαιότητα ότι το RISC-V RTL σας δεν περιέχει εκπλήξεις;

Δεδομένης της σχετικής καινοτομίας και πολυπλοκότητας των σχεδίων RISC-V RTL, είτε αγοράζετε έναν πυρήνα που υποστηρίζεται από το εμπόριο είτε κάνετε λήψη μιας δημοφιλής προσφοράς ανοιχτού κώδικα, υπάρχει ο μικρός αλλά μηδενικός κίνδυνος ανεπιθύμητων εκπλήξεων να διαφύγουν χωρίς να εντοπιστούν στο τελικό προϊόν σας. Με σειρά από υψηλή προς χαμηλή πιθανότητα, λάβετε υπόψη:

• Η παρουσία ενός παράξενου-αλλά-εντελώς-πιθανού σφάλματος στη γωνία
• Σφάλματα "μέσα" στις προσαρμοσμένες οδηγίες που δημιουργείτε εσείς ή ο προμηθευτής σας για την εφαρμογή σας
• Σφάλματα "στα άκρα" μιας προσαρμοσμένης εντολής — π.χ. η εντολή εκτελείται σωστά, αλλά με κάποιο τρόπο αφήνει το μηχάνημα σε κατεστραμμένη κατάσταση
• Σχετικά: μη τεκμηριωμένα και/ή κακώς καθορισμένα νέα χαρακτηριστικά που ανοίγουν άθελά τους τρύπες στο σχέδιο
• Κακόβουλη Trojan λογική εισάγεται κρυφά μέσω επίθεσης στην αλυσίδα εφοδιασμού

Κοινές προσεγγίσεις μετριασμού

Φυσικά, η πρώτη γραμμή άμυνας είναι η επιθεώρηση από εμπειρογνώμονες του εισερχόμενου ή αναπτυσσόμενου κώδικα RTL. Προφανώς, αυτό πρέπει να γίνει. αλλά θα πρέπει να είναι εξίσου προφανές ότι αυτή η τεχνική - όπως λένε στον μαθηματικό κόσμο - "είναι απαραίτητη αλλά όχι επαρκής" (ακόμα κι αν είχατε τον ίδιο τον καθηγητή Patterson να επανεξετάσει τον κώδικά σας).

Η επόμενη γραμμή άμυνας είναι η εφαρμογή προσεγγίσεων που βασίζονται σε προσομοίωση: Προσομοίωση σετ εντολών (ISS), αυτοματοποιημένη σύγκριση του DUT σας με ώριμα χρυσά μοντέλα, περιορισμένοι τυχαίοι πάγκοι δοκιμών UVM για προσομοίωση DUT RTL και ακόμη και διοχέτευση ερεθισμάτων πραγματικού κόσμου σε εξομοίωση υποβοηθούμενη από υλικό του DUT. Και πάλι, αυτές οι προσεγγίσεις είναι όλες πολύτιμες και πρέπει να γίνουν. αλλά όλοι πάσχουν από το ίδιο ελάττωμα: είναι εγγενώς ελλιπείς καθώς βασίζονται στη δημιουργία ερεθισμάτων. Για παράδειγμα, στην ακραία αλλά πιθανή περίπτωση επίθεσης στην αλυσίδα εφοδιασμού, ο προγραμματιστής της λογικής Trojan έχει σκόπιμα δημιουργήσει μια αλληλουχία ενεργοποίησης σημάτων και δεδομένων που πιθανότατα θα διαφύγουν τον εντοπισμό ακόμη και από τον πιο δημιουργικό χάκερ λευκού καπέλου. Και φυσικά, τα λειτουργικά σφάλματα έχουν τον δικό τους τρόπο να χρησιμοποιούν φυσικά την εντροπία για να παραμένουν κρυφά.

Η ουσία είναι ότι ο μόνος τρόπος για να είστε απόλυτα σίγουροι ότι το RISC-V RTL σας είναι απαλλαγμένο από φυσικές ή κακόβουλες εκπλήξεις είναι να εφαρμόσετε εξαντλητικές, επίσημες μεθόδους για την επαλήθευση του σχεδιασμού.

Εύκολα είπε από το κάνουμε, σωστά;

Ναι και όχι: Πριν από 14 χρόνια, αυτού του είδους η ανάλυση ήταν εφικτή μόνο από ερευνητές σε επίπεδο διδακτορικού χρησιμοποιώντας τα δικά τους χειροποίητα προγράμματα. Αλλά από το 2008, τα εργαλεία και οι τεχνικές έχουν παραχθεί έτσι ώστε όποιος είναι εξοικειωμένος με τις βασικές αρχές της επίσημης επαλήθευσης και τη σύνταξη του προτύπου IEEE System Verilog Assertions (SVA) μπορεί γρήγορα να εφαρμόσει και να πετύχει εδώ.

Μια τυπική διαδικασία τριών σταδίων

Η συνιστώμενη τυπική ροή εκτυλίσσεται ως εξής:

1. Δημιουργήστε έναν επίσημο πάγκο δοκιμών που «μοντελοποιεί» την προδιαγραφή DUT
2. Καθορίστε τους περιορισμούς εισόδου και τους ελέγχους που θα εκτελεστούν έναντι του DUT
3. Εκτελέστε ανάλυση

Βήμα 1 – Δημιουργήστε έναν επίσημο πάγκο δοκιμών που «μοντελοποιεί» την προδιαγραφή DUT

Η βάση αυτής της μεθοδολογίας είναι να γράψει ένα σύνολο ιδιοτήτων που αντιπροσωπεύουν τη συμπεριφορά κάθε εντολής στο σχεδιασμό RISC-V. Ο στόχος είναι να καταγράψουμε το αποτέλεσμα μιας δεδομένης εντολής στις εξόδους και τις εσωτερικές αρχιτεκτονικές καταστάσεις του IP (στον κόσμο RISC-V, αυτός είναι ο μετρητής προγράμματος (PC) και το αρχείο καταχωρητή (RF)) για οποιαδήποτε δεδομένη αυθαίρετα μεγάλη ακολουθία εισόδου. Αυτό γίνεται χρησιμοποιώντας μια ειδικά κατασκευασμένη επέκταση στο IEEE SVA που ονομάζεται Operational SVA. Με λίγα λόγια, αυτή είναι μια βιβλιοθήκη που αποστέλλεται με το επίσημο εργαλείο επαλήθευσης επεξεργαστή. και από την άποψη του μηχανικού επαλήθευσης, μοιάζει με ένα διαισθητικό υποσύνολο οικείου κώδικα SVA. Το σχήμα 1 δείχνει τη γενική δομή:

ιδιότητα instruction_A; // εννοιολογική κατάσταση t ##0 ready_to_issue() και // trigger t ##0 opcode==instr_A_opc υποδηλώνει // εννοιολογική κατάσταση t ##0 ready_to_issue() και // έξοδοι διεπαφών μνήμης // ανάγνωση της επόμενης εντολής t ##0 imem_access(instr_A_opc) και // φόρτωση δεδομένων/αποθήκευση t ##1 dmem_access(instr_A_opc) και // αρχιτεκτονικοί καταχωρητές t ##1 RF_update(instr_A_opc) and t ##1 PC_update(instr_A_opc) endproperty 

Εικ. 1: Δομή του λειτουργικού κώδικα SVA που καταγράφει τις προδιαγραφές μιας εντολής επεξεργαστή. [1]

Αναφερόμενοι στο σχήμα 1, στην αριστερή πλευρά του ΕΠΙΠΤΩΣΕΙΣ (το τμήμα του κώδικα πάνω από η λέξη-κλειδί υποδηλώνει) προσδιορίζει πότε το μηχάνημα είναι έτοιμο να εκδώσει μια νέα εντολή και πότε εκδίδεται η οδηγία. Ο ισχυρισμός αποτυπώνει τις τρέχουσες αξίες των αρχιτεκτονικών καταστάσεων και, στη δεξιά πλευρά του υπονοούμενου (τμήμα κώδικα παρακάτω η λέξη-κλειδί υποδηλώνει), αποδεικνύει τις επόμενες αξίες τους.

Επιπλέον, οι έξοδοι του επεξεργαστή πρέπει να αποδεικνύονται σωστές — σε αυτήν την περίπτωση για να βεβαιωθείτε ότι η εντολή έχει πρόσβαση στις αναμενόμενες θέσεις δεδομένων και μνήμης εντολών. Ο ισχυρισμός αποδεικνύει επίσης ότι το μηχάνημα είναι έτοιμο να εκδώσει μια νέα οδηγία για τον επόμενο κύκλο. Αυτό είναι ζωτικής σημασίας για την αποσύνδεση της επαλήθευσης μιας εντολής από την ακολουθία εντολών της οποίας θα μπορούσε να είναι μέρος. Για παράδειγμα, η εντολή Α θα μπορούσε να εκτελεστεί σωστά, αλλά να αφήσει το μηχάνημα σε κατεστραμμένη κατάσταση. Αυτή η λανθασμένη κατάσταση θα μπορούσε να προκαλέσει την επόμενη εντολή Β να παράγει λανθασμένα αποτελέσματα χωρίς δική της ευθύνη. Ως εκ τούτου, με την προσέγγιση λειτουργικής SVA, η εντολή επαλήθευσης ισχυρισμών Β θα περνούσε, ενώ η εντολή επαλήθευσης ισχυρισμού Α θα αποτύγχανε (όπου οι λειτουργίες μνήμης ανάγνωσης και εγγραφής θα μπορούσαν να διαρκέσουν αρκετούς κύκλους).

Κατώτατη γραμμή: οι συναρτήσεις που αντιπροσωπεύουν αρχιτεκτονικές καταστάσεις στον λειτουργικό κώδικα SVA πρέπει να αντιστοιχίζονται στα σήματα υλοποίησης και πρέπει να αντικατοπτρίζουν τη μικροαρχιτεκτονική του επεξεργαστή. Η κατάσταση του RF, για παράδειγμα, μπορεί να εξαρτάται από την ενεργοποίηση των διαδρομών προώθησης. [1]

[Σημείωση: Για όσους από εσάς γνωρίζουν είτε την προσομοίωση είτε την επίσημη λειτουργική κάλυψη, αυτή η έννοια της πληρότητας δεν βασίζεται σε μετρήσεις δομικής κάλυψης ή στη δημιουργία και συλλογή μετρήσεων για ένα μοντέλο λειτουργικής κάλυψης. Αντ 'αυτού (και να προχωρήσουμε λίγο πιο μπροστά από τα υπόλοιπα βήματα και αποτελέσματα), το αποτέλεσμα της ανάλυσης εδώ έχει να κάνει με τη λήψη πλήρους αποδείξεων για όλες τις ιδιότητες. Οι πλήρεις αποδείξεις δείχνουν επίσης σιωπηρά ότι δεν υπάρχει καμία άλλη λειτουργικότητα — η οποία ήταν απροσδιόριστη ή απροσδόκητη (προδιαγραφές ή σφάλμα κωδικοποίησης) ή εισήχθη κακόβουλα — που να μην καταγράφεται από αυτό το σύνολο ιδιοτήτων. Αναδιατυπώνοντας, αυτή η μεθοδολογία έχει να κάνει με την επίτευξη 100% «κάλυψης σχεδίου δοκιμής», όπως επαληθεύεται από τα εξαντλητικά επίσημα αποτελέσματα ανάλυσης — όπου τίποτα δεν είναι πιο «πλήρες» από μια μαθηματική απόδειξη!]

Βήμα 2 – Καθορίστε τους περιορισμούς εισόδου και τους ελέγχους που θα εκτελεστούν έναντι του DUT

Για να συμπληρωθούν οι ιδιότητες προδιαγραφών για κάθε εντολή, το επόμενο βήμα είναι να καθοριστούν οι περιορισμοί εισόδου και τυχόν πρόσθετοι έλεγχοι εξόδου. Και πάλι, χρησιμοποιείται το Operational SVA, όπου ο χρήστης καθορίζει τώρα ένα "σχέδιο πληρότητας" για να ορίσει τόσο νόμιμες εισόδους όσο και παράνομη σηματοδότηση που το DUT θα πρέπει να αγνοεί. Σύμφωνα με το παράδειγμα που φαίνεται στο σχήμα 2, υπάρχουν τρεις ενότητες: υποθέσεις προσδιορισμού, απαιτήσεις προσδιορισμού και γράφημα ιδιοτήτων.

επεξεργαστής πληρότητας? προσδιορισμός_υποθέσεις: // ΕΙΣΟΔΟΙ προσδιορίστηκαν(imem_data_i); προσδιορισμένο(dmem_valid_i); εάν (dmem_valid_i) καθορίζεται(dmem_data_i) endif; determination_requirements: // ΕΞΟΔΕΣ προσδιορίζονται(imem_read_o), if (imem_read_o) defined(imem_addr_o) endif; προσδιορισμένο(dmem_enable_o); if (dmem_enable_o) προσδιορισμένο(dmem_rd_wr_o), προσδιορισμένο(dmem_addr_o) endif; // ΑΡΧΙΤΕΚΤΟΝΙΚΕΣ ΚΑΤΑΣΤΑΣΕΙΣ προσδιορίζονται (PC); προσδιορισμένο (RF); ιδιοκτησία_γραφήματος: all_instructions := instruction_not_a, instruction_add_a, instruction_sub_a, [...] all_instructions -> all_instructions; Τελική πληρότητα? 

Εικ. 2: Παράδειγμα σχεδίου πληρότητας με υποθέσεις και απαιτήσεις προσδιορισμού υπό όρους.

Για να αναλύσουμε:

• Το "determination_assumptions" είναι απλώς ένα φανταχτερό όνομα για περιορισμούς τιμής εισόδου
• Το "determination_requirements" είναι ένας ορισμός των σημάτων που πρέπει να επαληθευτούν (τόσο τα σήματα εξόδου του επεξεργαστή όσο και οι αρχιτεκτονικές καταστάσεις)
• Η ενότητα "property_graph" είναι απλώς μια σύνδεση αυτού του αρχείου με όλες τις ιδιότητες που δημιουργήθηκαν στο Βήμα 1

Ανακεφαλαιώνοντας το σημείο που βρισκόμαστε σε αυτό το σημείο: στο Βήμα 1 δημιουργήσατε αυτό που είναι ουσιαστικά ένα μοντέλο με ακρίβεια κύκλου του DUT που πρέπει να αποδεικνύεται αληθές για πάντα και όλες τις εισόδους. στο Βήμα 2 ορίζετε τους περιορισμούς και τυχόν ειδικές συμπεριφορές που πρέπει να προσέχετε. Προσθέστε τα μαζί και ουσιαστικά έχετε έναν επίσημο πάγκο δοκιμών που είναι έτοιμος να τρέξει!

Βήμα 3 – Εκτέλεση ανάλυσης

Ο στόχος όλων των επίσημων εργαλείων είναι να αποδείξουν εξαντλητικά ότι όλες οι ιδιότητες είναι αληθείς για πάντα και όλες τις εισροές. Στην περίπτωση της επαλήθευσης επεξεργαστή RISC-V, το εργαλείο λειτουργεί για να αποδείξει ότι οποιαδήποτε αυθαίρετα μεγάλη ακολουθία εισόδου μπορεί να αντιστοιχιστεί σε μια μοναδική ακολουθία του καθορισμένου λειτουργικού SVA που προβλέπει τις τιμές των εξόδων και των αρχιτεκτονικών καταστάσεων.

Και αυτό ακριβώς συμβαίνει. Εάν εντοπιστεί κάποια διαφορά στη συμπεριφορά μεταξύ της προδιαγραφής και του DUT, το επίσημο εργαλείο παρέχει μια κυματομορφή «αντιπαραδείγματος» που δείχνει ακριβώς τη σειρά των σημάτων εισόδου και των δεδομένων που μπορεί να δημιουργήσουν παραβίαση της προδιαγραφής. Όπως αναφέρθηκε παραπάνω, τέτοιες αστοχίες μπορούν να βρεθούν στο εσωτερικό της λογικής RTL της διδασκαλίας ή στη «λογική μεταβίβασης» που συνδέει τον επόμενο νομικό κλάδο/οδηγία.

Είτε έτσι είτε αλλιώς, όταν επιδιορθωθούν αυτά τα ζητήματα και το εργαλείο αποδείξει όλες τις ιδιότητες, τα αποτελέσματα είναι πραγματικά "πλήρη" - δηλαδή, μπορείτε να είστε μαθηματικά σίγουροι ότι δεν υπάρχουν σφάλματα κωδικοποίησης RTL - η επίσημη ανάλυση έχει κυριολεκτικά αποδείξει την απουσία σφαλμάτων !

Αποτελέσματα

Πρώτον, όπως σημειώθηκε παραπάνω, με τα χρόνια πολλοί προγραμματιστές επεξεργαστών επωφελήθηκαν από αυτή τη ροή [2], [3], [4].

Δοκιμάζοντας αυτή τη μεθοδολογία με το RISC-V, οι συνάδελφοί μου έκαναν μια μελέτη περίπτωσης χρησιμοποιώντας τον δημοφιλές πυρήνα ανοιχτού κώδικα Rocket Chip. Συγκεκριμένα, εξετάστηκε η διαμόρφωση RV64IMAFDC – sv39 vm. Αυτός είναι ένας πυρήνας επεξεργαστή 64 bit με σύστημα εικονικής μνήμης 39 bit [5] και επεκτάσεις, όπως συμπιεσμένες και ατομικές οδηγίες [6]. Αυτή η εφαρμογή ανοιχτού κώδικα, RISC-V ISA χρησιμοποιεί μια διοχέτευση σειράς πέντε σταδίων, μονού ζητήματος, με ολοκλήρωση εκτός σειράς για οδηγίες μεγάλης καθυστέρησης, όπως αποτυχίες διαίρεσης ή προσωρινής μνήμης. Ο πυρήνας υποστηρίζει επίσης την πρόβλεψη διακλάδωσης και την τροποποίηση χρόνου εκτέλεσης του καταχωρητή "misa", επιτρέποντάς του να απενεργοποιήσει ορισμένες επεκτάσεις συνόλου εντολών.

Παρόλο που αυτό το στιγμιότυπο του Rocket Chip είχε επαληθευτεί εκτενώς και είχε μαγνητοσκοπηθεί πολλές φορές, εντοπίστηκαν τέσσερις μέχρι πρότινος άγνωστες, ύποπτες συμπεριφορές, και αναφέρθηκαν στους προγραμματιστές του Rocket Core RTL. Αυτά τα ζητήματα ([7], [8], [9] και [10]) ανακαλύφθηκαν αποκλειστικά μέσω της συστηματικής εφαρμογής της πλήρους επίσημης προσέγγισης επαλήθευσης που περιγράφεται σε αυτό το άρθρο.

Αναλύοντας το [10] συγκεκριμένα — την ανακάλυψη μιας μη τυπικής εντολής CEASE (Opcode 0x30500073) στο RTL: σαφώς η ομάδα Rocket Chip έμεινε πίσω στην τεκμηρίωσή της (και το διόρθωσαν σχεδόν αμέσως μετά την υποβολή του αιτήματος έλξης GitHub). Το μεγαλύτερο σημείο είναι ότι αυτό δείχνει ότι η λογική που απαιτείται για την υλοποίηση μιας ολόκληρης εντολής - δεκάδες γραμμές κώδικα και πολλές πύλες συνθετικής, τοποθετημένης και δρομολογημένης λογικής - μπορεί να ξεφύγει από την ανίχνευση με οπτική επιθεώρηση, προσομοίωση RTL, προσομοίωση επιπέδου πύλης, το σύνολο διαδικασία υλοποίησης back-end και πρωτότυπα υλικού στο εργαστήριο!

Τι γίνεται όμως με την απόδοση αυτής της ροής;

Αρχικά, ας εξετάσουμε την ευρύτερη έννοια της «απόδοσης». Λόγω της νέας φύσης του σχεδιασμού του Rocket Chip, για αυτήν τη μελέτη περίπτωσης χρειάστηκαν περίπου 20 εβδομάδες μηχανικής για να αναπτύξουν οι επίσημοι επαγγελματίες επαλήθευσης ολόκληρου του πάγκου δοκιμών και των περιορισμών. Ωστόσο, οι προηγούμενες εφαρμογές αυτής της ροής σε πιο δομημένη, εμπορική ΔΙ συνήθως χρειάστηκαν ένα κλάσμα αυτού του χρόνου. Φυσικά, η όλη διαδικασία εμφάνισης θα πάει πολύ πιο γρήγορα όσο πιο σταθερές και ώριμες είναι οι προδιαγραφές, πόσο καλά τεκμηριωμένος και ευανάγνωστος είναι ο κώδικας DUT RTL και πόση πρόσβαση έχετε στους μηχανικούς σχεδιασμού για Q&A.

Μόλις ρυθμιστεί το περιβάλλον, ο χρόνος εκτέλεσης του ρολογιού τοίχου ήταν 2 ώρες — δηλαδή, πολύ λιγότερος από ό,τι θα μπορούσατε εύλογα να περιμένετε από την περιορισμένη τυχαία προσομοίωση RTL και ακόμη και την επαλήθευση με τη βοήθεια υλικού. Επιπλέον, θυμηθείτε ότι τα αποτελέσματα αυτής της ανάλυσης ισχύουν για όλες τις εισροές και για όλες τις εποχές — με μια λέξη, είναι εξαντλητικά [11].

Χαρακτηριστικά

Η πλήρης, τυπική προσέγγιση επαλήθευσης επεξεργαστή που παρουσιάζεται σε αυτό το άρθρο χρησιμοποιεί μια επέκταση στο IEEE SVA, Operational SVA, για να επαληθεύσει επίσημα ότι ένα RISC-V ISA δεν έχει κενά και ασυνέπειες. Σε αντίθεση με τους πάγκους δοκιμών περιορισμένης τυχαίας προσομοίωσης, την εξομοίωση ή τη φυσική πρωτότυπη, το πλήρες σύνολο ιδιοτήτων και περιορισμών εντοπίζει εξαντλητικά πολλούς τύπους σφαλμάτων RTL, καθώς και την παρουσία μη τεκμηριωμένων ή κακώς καθορισμένου κώδικα και κακόβουλων Trojans.

αναφορές

1 – 2019 Συνέδριο GOMACTech, Αλμπουκέρκη, NM, 28 Μαρτίου 2019: Πλήρης επίσημη επαλήθευση των IP επεξεργαστών RISC-V για αξιόπιστα IC χωρίς Trojan, David Landolll, et.al.

2 – DVCon 2007: Πλήρης επίσημη επαλήθευση του TriCore2 και άλλων επεξεργαστών, Infineon Gmbh.

3 - 51^st Διάσκεψη Αυτοματισμού Σχεδίασης (DAC): Η επίσημη επαλήθευση εφαρμόζεται στην πλατφόρμα σχεδίασης MCU Renesas με χρήση των εργαλείων OneSpin

4 – DVCon Europe 2019: Πλήρης επίσημη επαλήθευση μιας οικογένειας DSP αυτοκινήτων, Bosch Gmbh.

5 – The RISC-V Instruction Set Manual, Volume II: Privileged Architecture, Document Version 1.10.

6 - https://github.com/freechipsproject/rocket-chip [πρόσβαση στις 20 Δεκεμβρίου 2018]

7 – Το αποτέλεσμα εντολών DIV δεν γράφτηκε στο αρχείο εγγραφής
https://github.com/freechipsproject/rocket-chip/issues/1752

8 – Οδηγίες JAL και JALR Αποθηκεύστε διαφορετικό υπολογιστή επιστροφής
https://github.com/freechipsproject/rocket-chip/issues/1757

9 – Επαναλαμβάνονται παράνομοι κωδικοί λειτουργίας και προκαλούν απροσδόκητες παρενέργειες
https://github.com/freechipsproject/rocket-chip/issues/1861

10 – Μη τυπική εντολή CEASE (Opcode 0x30500073) Ανακαλύφθηκε στο RTL, https://github.com/freechipsproject/rocket-chip/issues/1868

11 – Ιστολόγιο Verification Horizons, Πώς μπορείτε να πείτε ότι η επίσημη επαλήθευση είναι εξαντλητική;, Joe Hupcey III
https://blogs.sw.siemens.com/verificationhorizons/2021/09/16/how-can-you-say-that-formal-verification-is-exhaustive/

Πηγή: https://semiengineering.com/do-you-know-for-sure-your-risc-v-rtl-doesnt-contain-any-surprises/