Cosa ha trovato Silica

Questi risultati usano ISA_A64_xml_A_profile-2026-06_mc (Armv9.6-A). La scansione è stata suddivisa in 256 shard verificati indipendentemente che coprono tutte le 2³² codifiche.

Accordo con la specifica sulla validità di una codifica:

Il grande divario di validità ha cause identificabili. Unicorn verifica la validità eseguendo un'istruzione e osservando i trap, mentre gli altri oracoli decodificano senza esecuzione. Un piccolo numero di regioni è anche influenzato da condizioni UNDEFINED in fase di decodifica che l'oracolo della specifica compilata non valuta. Silica registra queste limitazioni invece di attenuarle nel risultato.

Testo delle istruzioni

Confrontare mnemoniche e operandi renderizzati è molto più costoso che registrare un bit di validità. Silica valuta quindi il testo su un campione deterministico di 1.000.000 di parole estratte da 1.266.064.016 candidate in cui tutti e quattro gli oracoli considerano la codifica valida. Questo è un risultato campionato ed è deliberatamente tenuto separato dalle cifre esaustive di validità.

Il campione è utile per individuare il lavoro di normalizzazione e presentazione; non pretende una copertura esaustiva di ogni rendering testuale.

Esplora i risultati

Il motore di scansione produce un grande dataset di ricerca. silica-scope è l'applicazione terminale complementare che rende quel dataset accessibile. Apre una directory di artefatti Silica completata e consente di sfogliare le metriche principali, ispezionare la mappa di codifica a 256 shard, filtrare i disaccordi, cercare qualsiasi parola a 32 bit e leggere i riproduttori pronti per la segnalazione.

Installalo da PyPI con Python 3.11 o superiore:

Poi eseguilo da un checkout di Silica o puntalo a una directory di artefatti:

silica-scope è un lettore in puro Python senza dipendenze da decoder nativi. Non avvia la scansione esaustiva e gestisce con grazia il set di artefatti pubblicati più piccolo del repository. Consulta la guida al lettore terminale per i pannelli, i controlli da tastiera e le opzioni di scoperta degli artefatti.

Come funziona

Il percorso ad alto volume è scritto in Rust e chiama ciascun decoder in-process. Memorizza un bit per codifica per oracolo, il che mantiene il confronto esaustivo compatto e rende il disaccordo una diretta operazione su bitmap. I crash vengono bisecati fino alla parola di istruzione esatta.

Python gestisce la compilazione della specifica, la normalizzazione, il reporting e il livello di verifica indipendente. Gli schemi degli artefatti, le regole di campionamento e le limitazioni note sono documentati in docs/formats.md.

Riprodurre il lavoro

Crea l'ambiente con versioni bloccate e verifica che gli input locali richiesti siano disponibili:

La specifica XML di Arm non è inclusa nel repository a causa della sua licenza. silica doctor segnala dove Silica si aspetta di trovarla e qualsiasi altro prerequisito mancante.

Per eseguire l'intera pipeline da un checkout preparato:

Questa è una scansione completa di 2³², non un rapido smoke test. Produce l'oracolo compilato, i record degli shard, le bitmap di validità, il corpus dei disaccordi, le metriche pubblicate, i riproduttori e un hash del risultato SHA-256 stabile.

Fidati, ma verifica

Sette verificatori indipendenti ricalcolano le affermazioni del progetto dagli artefatti grezzi. Non si fidano di un riepilogo generato, e ogni verificatore ha una fixture che dimostra che rileva il difetto da cui si protegge. Non esiste uno stato saltato o provvisorio.

Le versioni bloccate dei decoder e un hash del risultato ricalcolato da zero rendono comparabili esecuzioni separate. Gli obiettivi di verifica e il loro stato attuale sono registrati in GOALS.yml.

Ambito

Silica attualmente copre la decodifica A64 base e Advanced SIMD. SVE, SVE2, SME, A32/T32, RISC-V, i round trip dell'assembler e i test di esecuzione generali sono fuori dallo studio v1.

L'ispirazione più vicina è Sandsifter, che esplora lo spazio di istruzioni a lunghezza variabile di x86. Silica applica lo stesso spirito di scetticismo sistematico ad AArch64, dove le codifiche a larghezza fissa e una specifica indipendente consentono un confronto completo e con giudizio.