Usando Verificação Formal para Avaliar Perturbações de Evento Único em um Núcleo RISC-V

A confiabilidade tem sido uma preocupação major em sistemas embarcados. Uma maior densidade de transistores e uma menor tensão de alimentação aumentam a vulnerabilidade dos sistemas embarcados a erros suaves. Uma Perturbação de Evento Único (SEU), que também é chamada de erro suave, pode inverter um bit em um elemento sequencial, resultando em uma falha do sistema. A injeção de falhas baseada em simulação tem sido amplamente utilizada para avaliar a confiabilidade, conforme sugerido pela ISO26262. No entanto, é praticamente impossível testar todas as falhas para um projeto complexo. A injeção aleatória de falhas é um compromisso que reduz a precisão e a cobertura de falhas. A verificação formal é uma abordagem alternativa. Neste artigo, usamos verificação formal, na forma de verificação de modelos, para avaliar a confiabilidade do hardware de um Núcleo RISC-V Ibex na presença de erros suaves. O rastreamento reverso é realizado para identificar e categorizar falhas de acordo com seus efeitos (sem efeito, Corrupção de Dados Silenciosa, travamentos e congelamentos). Ao usar verificação formal, todo o espaço de estado e lista de falhas podem ser explorados exaustivamente. Foi descoberto que instruções desalinhadas podem amplificar os efeitos das falhas. Também foi encontrado que alguns bits são mais vulneráveis a SEUs do que outros. De maneira geral, a maioria dos bits no Núcleo Ibex é vulnerável à Corrupção de Dados Silenciosa, e o segundo estágio do pipeline é mais vulnerável à Corrupção de Dados Silenciosa do que o primeiro.