Checagem de equivalência de sequências de estados de projetos digitais em RTL com modelos de referência em alto nível e de protocolo de comunicação (2014)
- Authors:
- Autor USP: MARQUEZ, CARLOS IVAN CASTRO - EP
- Unidade: EP
- Sigla do Departamento: PSI
- Assunto: PROTOCOLOS DE COMUNICAÇÃO
- Language: Português
- Abstract: A tendência à miniaturização de dispositivos dos processos de fabricação tem levado à criação de CIs cada vez mais complexos, o que, por sua vez, permite a construção de sistemas eletrônicos com mais e melhores serviços. Tal fato não somente satisfaz as exigências do mercado tecnológico, mas também, aumenta o patamar dos padrões esperados para futuros produtos no que diz respeito às suas características, tanto físicas, como funcionais. Diante da complexidade dos CIs digitais atuais, existe uma grande probabilidade de se inserir, desapercebidamente, um número indeterminado de erros durante a fase de projeto dos circuitos. A verificação funcional é o conjunto de tarefas destinado a descobrir tais erros, e representa um importante desafio ao estar diretamente relacionada com a eficiência ao longo do ciclo inteiro de produção. Estima-se que até um 80% dos custos totais de projeto são devidos à verificação, situação que tem se mantido durante as duas últimas décadas, tornando esta atividade no gargalo principal na tentativa de reduzir todo tipo de recursos de produção. A verificação funcional pode ser descrita como a tarefa de avaliar se um modelo de circuito descrito em nível RTL atende às especificações definidas para o projeto ou a algum modelo executável de especificação. Tal problemática tem provocado a aparição de diversas estratégias para diminuir o esforço, ou para aumentar a exaustão da validação. No primeiro caso utiliza-se a simulação, que permite descobrir um número razoável de erros de projeto, especialmente em etapas iniciais da verificação. Contudo, a natureza aleatória dos estímulos utilizados na simulação, e a lentidão da simulação de descrições RTL, tornam mínima a cobertura real de estados desta técnica. Os métodos formais fornecem, alternativamente, alta cobertura de estados.A checagem de modelos é um de tais métodos, o qual checa a validade de um conjunto de propriedades para todos os estados de um modelo formal do DUV. No entanto, esta técnica padece do problema de explosão de estados, e da dificuldade de especificar um conjunto robusto de propriedades. Outra alternativa formal é a checagem de equivalência que, ao invés de propriedades, verifica o projeto em comparação com um modelo de referência. As técnicas de checagem de equivalência tradicionais apresentam a restrição de serem aplicáveis, unicamente, a descrições no mesmo nível de abstração, e com conjuntos de interfaces, variáveis, e sinais idênticas. Dadas as grandes diferenças de descrição normalmente existentes entre um modelo de implementação RTL e um modelo de especificação, há poucos registros na literatura técnica que tratem do problema de equivalência entre eles. Neste trabalho apresenta-se uma metodologia de verificação formal, através do uso de técnicas de checagem de equivalência, para determinar a validade de uma implementação em RTL, comparando-a com um modelo de referência em alto nível, e com um modelo formal do protocolo de comunicação. Para permitir tal checagem, a metodologia se baseia no conceito de sequências de estados, ao invés de estados individuais como na checagem de equivalência tradicional. As discrepâncias entre níveis diferentes de abstração são consideradas, incluindo alfabetos diferentes, mapeamento entre estados, e dessemelhanças temporais. No quadro teórico introduzido, a validade da metodologia é demonstrada formalmente. Uma ferramenta para aplicação prática da metodologia foi desenvolvida, e os resultados demonstram efetividade e eficiência na verificação formal de tipos diversos de circuitos digitais.Também, evidencia-se a capacidade da ferramenta para descobrir erros de tipo combinatório e sequencial, dentro de tempos e quantidades de iterações praticáveis em casos reais.
- Imprenta:
- Data da defesa: 20.02.2014
-
ABNT
CASTRO MÁRQUEZ, Carlos Iván. Checagem de equivalência de sequências de estados de projetos digitais em RTL com modelos de referência em alto nível e de protocolo de comunicação. 2014. Tese (Doutorado) – Universidade de São Paulo, São Paulo, 2014. Disponível em: http://www.teses.usp.br/teses/disponiveis/3/3140/tde-23122014-155143/. Acesso em: 26 abr. 2024. -
APA
Castro Márquez, C. I. (2014). Checagem de equivalência de sequências de estados de projetos digitais em RTL com modelos de referência em alto nível e de protocolo de comunicação (Tese (Doutorado). Universidade de São Paulo, São Paulo. Recuperado de http://www.teses.usp.br/teses/disponiveis/3/3140/tde-23122014-155143/ -
NLM
Castro Márquez CI. Checagem de equivalência de sequências de estados de projetos digitais em RTL com modelos de referência em alto nível e de protocolo de comunicação [Internet]. 2014 ;[citado 2024 abr. 26 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3140/tde-23122014-155143/ -
Vancouver
Castro Márquez CI. Checagem de equivalência de sequências de estados de projetos digitais em RTL com modelos de referência em alto nível e de protocolo de comunicação [Internet]. 2014 ;[citado 2024 abr. 26 ] Available from: http://www.teses.usp.br/teses/disponiveis/3/3140/tde-23122014-155143/
How to cite
A citação é gerada automaticamente e pode não estar totalmente de acordo com as normas
