Verificação de circuitos digitais. Revisão

Vou tentar falar em geral sobre a verificação de circuitos digitais.

A verificação nesta área é um processo importante que requer o envolvimento de engenheiros experientes. Por exemplo, um especialista em verificação que trabalha em sistemas com uma CPU, como regra, deve possuir linguagens de script e linguagens de shell de comando (Tcl, bash, Makefile etc.), linguagens de programação (C, C ++, assembler), HDL / HDVL (SystemVerilog [10, Apêndice C - História da linguagem] [11], Verilog, VHDL), metodologias e estruturas modernas (UVM).

A proporção de tempo gasto na verificação chega a 70-80% do tempo total do projeto. Uma das principais razões para essa atenção é que você não pode liberar um "patch" para o chip depois que ele foi colocado em produção; você pode liberar apenas "silicon errata" (isso não se aplica a projetos FPGA / FPGA).

Por circuitos digitais, quero dizer:

• blocos funcionais complexos / propriedades intelectuais (SFB / IP);
• Chips personalizados ASIC (Circuito Integrado de Aplicação Específica)
• circuitos lógicos programáveis ​​/ matriz de portas programáveis ​​em campo (FPGA);
• sistemas em um chip / sistema em cristal (SoC / SoC);
• etc.

Problemas reais de verificação

O estado atual e as tendências no campo da verificação podem ser julgados pelos seguintes desafios e problemas que ele enfrenta [6]:

• O tamanho do objeto de verificação (OB) está aumentando constantemente. Mesmo um pequeno IC tipo microcontrolador é um conjunto de dezenas de submódulos, muitas vezes com funcionalidades complexas. Grandes CIs são complexos nos quais pode haver até dezenas de bilhões de transistores, e o esquema de gerenciamento de energia sozinho pode exceder alguns processadores em complexidade [8];
• é impossível elaborar uma especificação para o IMS no início do projeto e apenas segui-la no futuro, ela muda constantemente ao longo do processo de desenvolvimento (o cliente altera os requisitos, problemas técnicos ou encontra soluções mais ótimas para reconsiderar abordagens etc.). Com base nisso, todos os processos devem perceber a dinâmica das alterações nas especificações e ser modificados de acordo com os requisitos;
• freqüentemente, várias equipes distantes umas das outras trabalham na verificação do projeto, cujo número pode chegar a dezenas de pessoas;
• o número de testes individuais e seus tipos atinge um número enorme, seus resultados devem ser coletados e analisados;
• modelar até sistemas digitais requer muito tempo no computador;
• a completude das metas de preparação estabelecidas para o projeto depende em grande parte da competência e intuição dos especialistas em verificação;
• apesar da existência de indicadores de cobertura do projeto com testes (métricas), a única maneira de concluir a verificação é decidir suspendê-la, com base principalmente nas seguintes conclusões: o dinheiro ou o tempo gasto no estágio do projeto deve ser colocado em produção, parece que eles atingiram uma cobertura de código de 100 %, estamos testando há uma semana e não encontramos nenhum erro, etc.

Tipos de verificação

A verificação de circuitos digitais pode ser dividida nos seguintes tipos principais:

1. funcional (verificação funcional) - o nome fala por si, você verifica se o seu sistema está executando suas funções corretamente;
2. verificação formal - com essa verificação, é estabelecida a equivalência das representações do seu sistema em diferentes estágios da rota de design ou o cumprimento das instruções inseridas no código-fonte:
   
   • Verificação de equivalência (por exemplo, RTL para RTL, RTL para porta, porta a porta);
   • Verificação de propriedade (verificação de modelo) (verifica as propriedades (asserções) especificadas no código usando SVA (por exemplo)).
3. análise de código estático - verificação do código-fonte de acordo com critérios formais de conformidade com as regras de uso da linguagem e de suas construções. Muitas vezes, as regras de verificação configuradas são enviadas ao RMM [4]. Os programas para essa verificação geralmente são chamados de fiapos ou fiapos;
4. verificação física - basicamente implica verificações de DRC, LVS, PERC, etc., a representação física do sistema é verificada quanto à conformidade com os padrões tecnológicos e a conformidade das representações físicas e lógicas, etc. A composição das verificações é altamente dependente da tecnologia. Normalmente, a verificação física é realizada por um engenheiro ou equipe de projeto topológico.
5. prototipagem - o uso de FPGA para verificação funcional [18].

A verificação funcional no escopo de todo o trabalho é mais significativa e requer envolvimento humano direto.

A análise do código estático requer apenas a configuração inicial das ferramentas, que corresponde às regras internas de design adotadas pela empresa; a ferramenta se dedica ao fato de fornecer “orientações valiosas” aos desenvolvedores e não requer supervisão constante.

As ferramentas formais de verificação também costumam ser muito independentes, requer apenas uma análise cuidadosa dos relatórios que eles geram. Eles também são adequados para engenharia reversa, quando, por algum motivo, você sabe que precisa restaurar o código da lista de circuitos.

Exemplos de ferramentas de verificação

Exemplos de ferramentas de verificação de circuitos digitais (rota digital na parte superior):

• ferramentas de gerenciamento de verificação
  
  • Mentor Graphics - Gerenciamento de verificação de questa
  • Cadência - vManager
  • Sinopse - Verdi, VC Execution Manager ("ExecMan")
• funcional - geralmente simuladores
  
  • Mentor Graphics - ModelSim, QuestaSim
  • Cadência - Incisivo, Xcelium
  • Sinopse - VCS
  • Software livre de desenvolvedores independentes - simuladores Verilator, Icarus [5]
• formal
  
  • Mentor Graphics - Formal Pro, Questa Formal Verification
  • Cadence - JasperGold, LEC conforme, Plataforma de verificação formal incisiva
  • Sinopse - Formalidade, VC formal
• análise de código estático
  
  • Gráficos de mentores - Questa AutoCheck
  • Cadência - HAL, JasperGold
  • Sinopse - SpyGlass Lint
• verificação física
  
  • Mentor Graphics - Calibre
  • Cadence - Pegasus, Sistema de verificação física,
  • Sinopse - Hercules, Validador de IC

Métodos de verificação funcional

Verificação funcional - é um conjunto de testes, permitirei dividir-me condicionalmente em três grupos (não é um dogma, é da experiência pessoal):

1. Ramos positivos - verificação do comportamento em situações normais, regulado pela especificação do dispositivo ou padrão, etc. I.e. Verificamos situações em que tudo está indo bem.
2. Ramificações negativas - verificação de desvios de situações padrão, mas dentro da estrutura de uma especificação ou padrão, por exemplo - uma incompatibilidade da soma de verificação, o número de dados recebidos etc. I.e. quando algo dá errado, mas sabíamos que poderia ser e sabemos como trabalhar nessa situação.
3. Situações fora do padrão - qualquer situação aleatória, desde violações de protocolos de comunicação, a ordem dos dados, até colisões físicas em interfaces, alterações aleatórias no estado dos elementos lógicos, etc. I.e. é quando tudo pode acontecer e você precisa garantir que o OB sairá depois disso para a condição de trabalho.

Os dois primeiros estágios podem ser automatizados usando UVC / VIP (componente de verificação universal / IP de verificação) e rapidamente você pode aumentar o volume de vários testes, incluindo os gerados automaticamente. O terceiro estágio é uma "obra-prima" na verificação; este estágio requer uma abordagem e uma experiência extraordinárias, é muito difícil de automatizar, porque a maioria das situações é um algoritmo separado, talvez um script para CAD ou instruções para verificações "manuais".

Tipos de métricas de verificação funcional

Métricas são indicadores da cobertura de teste de um projeto. Eles são necessários para entender quais outros testes precisam ser desenvolvidos para verificar possíveis situações e quanto tempo a verificação pode levar [16].

Infelizmente, apenas um tipo de métrica é avaliado com base no código-fonte do projeto, a definição de critérios para os demais tipos é o resultado do trabalho intelectual.

Além disso, deve-se lembrar que a obtenção dos indicadores desejados por um tipo de métrica não significa trabalhabilidade em geral, é sempre necessário avaliar o complexo.

Tipos de métricas [3]:

• revestimento funcional . Mostra quanto a função OB foi testada. Os critérios para essa cobertura podem ser determinados pelo plano de teste e pela introdução de construções especiais (covergroup [1]) no ambiente de teste e / ou OM, monitorando se uma função / ação específica foi ou não executada, se os dados foram alterados de uma certa maneira etc. Informações de projetos incorporados no código fonte podem ser coletadas automaticamente pelo CAD.
• cobertura de código - alterando o estado das construções de código-fonte durante os testes. Ele é coletado automaticamente pelo CAD, não requer a introdução de nenhuma estrutura no código-fonte. Por exemplo:
  
  • troca de registros (Toggle Coverage);
  • atividade de cada linha de código (Cobertura de Linha);
  • atividade de expressões (Cover de declaração), de fato - trata-se de Cover Line, mas pode rastrear expressões que são mais de uma linha no editor;
  • atividade de um segmento de código dentro de uma declaração ou procedimento condicional (Cobertura de bloco), uma variação da Cobertura de declaração;
  • atividade de todos os ramos de declarações condicionais, como se, caso, enquanto, repita, para sempre, para, loop (Cobertura de ramo);
  • alteração de todos os estados (verdadeiro, falso) das expressões lógicas do componente (Cobertura de Expressão);
  • estado da máquina de estado (Cobertura de máquina de estado finito).
• cobertura de reivindicações . As declarações são construções de linguagem especiais que rastreiam vários eventos e seqüências e, de acordo com critérios especificados, determinam a legalidade de sua ocorrência.

Métodos de verificação funcional

Método de Testes Direcionados (DTM)

Testes diretos e significativos. Se esse método for adotado no projeto, o plano de verificação será composto de testes que visam verificar o comportamento da matéria orgânica em pontos de interesse específicos (estados). Verificar todas as situações possíveis, especialmente em projetos complexos, é quase impossível.
Ao mesmo tempo, problemas que podem surgir em situações não cobertas por testes não são detectados antes que o dispositivo seja iniciado para ser usado em condições reais. Normalmente, esses testes usam métricas de cobertura funcional.

Verificação orientada para cobertura, verificação orientada para métricas (CDV, MDV) [17]

O conceito de criação de testes com o objetivo de obter uma certa "cobertura de teste" de substâncias orgânicas. Eles contam com métricas para entender quais testes precisam ser adicionados ao plano de verificação para atingir os objetivos de prontidão do projeto.
Você precisa usar as ferramentas de análise de cobertura para ver o que mais adicionar ao plano de verificação. De fato, se começarmos a ajustar o plano de verificação no DTM, contando com pelo menos a "cobertura de código", já podemos assumir que passamos suavemente de DTM para CDV.

Verificação aleatória restrita (CRV)

Verificação enviando influências aleatórias. Estes são realmente testes automáticos com a geração de efeitos aleatórios no OM, mas é difícil imaginá-los sem simbiose com o ABV.
O método é muito caro no começo, porque Leva muito tempo para preparar as ferramentas. Após a conclusão do estágio inicial de preparação, o teste pode ser iniciado automaticamente, repetidamente com diferentes dados iniciais. Se uma incompatibilidade de asserção for detectada, a equipe de desenvolvimento e verificação começará a analisar o erro detectado.
Em um projeto real, não se pode limitar-se apenas a esse método, porque Usando esse método, você pode coletar cobertura de código e declaração, e eles não podem dizer nada sobre a operação correta do sistema operacional, ou seja, conformidade com as especificações. Deve ser complementado com testes funcionais.
Para implementar essa metodologia, é necessário:

1. implementar "afirmação" em todos os pontos importantes do código fonte do OB e do ambiente de teste;
2. desenvolver geradores de efeitos aleatórios e cenários de seu trabalho, ou seja, os impactos são aleatórios, mas têm limitações de alcance (não temos tempo para resolver tudo), a ordem de arquivamento etc.

Verificação baseada em asserção [9] (ABV)

Verificação com declarações. Provavelmente, esse nem é um método independente, mas algum componente ou componente básico dos itens acima.

Uma questão importante com a ABV é como distribuir asserções, quais são melhor colocadas no código-fonte do OB, quais devem estar no ambiente de teste.

Deve-se notar imediatamente que a linguagem Verilog não possui asserções em seu padrão (elas podem ser criadas usando as construções básicas da linguagem, mas são necessárias diretrizes para o sintetizador, para que não lide com a conversão). As asserções aparecem apenas no padrão SystemVerilog e também estavam originalmente no padrão de idioma VHDL e.

Eu sugiro que você se familiarize com as recomendações de especialistas, incluindo Clifford Cummings [12, artigos sobre SVA] sobre a distribuição de trabalhos na redação deles, bem como materiais sobre ABV no site da Verification Academy [13].

Referências

1. IEEE Std 1800TM-2012. Padrão IEEE para SystemVerilog - Linguagem unificada de design, especificação e verificação de hardware
2. Clive Maxfield. Projeto FPGA. Arquitetura, ferramentas e métodos. O curso do jovem lutador. ISBN 978-5-94120-147-1 (RUS), ISBN 0-7506-7604-3 (ENG)
3. Academia de verificação. Livro de receitas de cobertura. Cobertura de teste profissional
4. Michael Keating, Pierre Bricaud. Manual de metodologia de reutilização para projetos de sistema em um chip. Imprimir ISBN 1-4020-7141-8, eBook ISBN 0-306-47640-1
5. Lista de CAD licenciado e distribuído gratuitamente
6. Mentor Graphics. Um exemplo de estatísticas sobre o estado atual e o escopo da verificação
7. WikiChip. Chips Wikipedia
8. Wikipedia Dados generalizados sobre o número de transistores no IC
9. Harry Foster, Adam Krolnik, David Lacey. Design baseado em asserção.Print ISBN 1-4020-8027-1, eBook ISBN 1-4020-8028-X
10. Stuart Sutherland, Simon Davidmann, Peter Flake. SystemVerilog for Design. ISBN-10: 0-387-33399-1, eBook ISBN-10: 0-387-36495-1
11. Chris Spear, Greg Tumbush. SystemVerilog for Verification. ISBN da impressão: 978-1-4614-0714-0, eBook ISBN: 978-1-4614-0715-7
12. Projeto Sunburst. Artigos
13. Academia de verificação. Curso ABV
14. Doulos. Materiais úteis on-line e livros de referência
15. Prakash Rashinkar, Peter Paterson, Leena Singh. Verificação do sistema em um chip. metodologia e técnicas. ISBN da impressão: 0-792-37279-4, ISBN do eBook: 0-306-46995-2
16. Academia de verificação. Métricas na verificação de SoC
17. Doulos. Metodologia de verificação orientada a cobertura
18. Doug Amos, Austin Lesea, Rene Richter. Manual de metodologia de prototipagem baseada em FPGA: Melhores práticas em Design para prototipagem (FPMM). ISBN da impressão: 978-1617300042. Baixe gratuitamente no site da Synopsys