Daniel Vidal
RA 099049
[email protected]
Enos A. V. F. de Lima
RA 032455
[email protected]
VERIFICAÇÃO FORMAL DE
BLOCOS COMPLEXOS
Conteúdo
2




Introdução
Métodos
Dificuldades e problemas
Considerações e conclusões
Verificação formal de sistemas complexos
Introdução - Funcionalidade
3

Verificaçao de funcionalidade:



implementação X especificação
Cada vez mais funcionalidades são integradas nos
circuitos integrados
Verificação mais complexa que a funcionalidade
em si
Verificação formal de sistemas complexos
Introdução - Funcionalidade
4

Tradicionalmente verificado por simulação onde
deve-se observar:
Controlabilidade – estimular o circuito
 Obersvabilidade
– observar o circuito
 Exaustividade
– verificar todos os cenários



Simulações de sistemas complexos são bem
comportadas em níveis altos de abstração.
Para níveis baixos de abstração as simulações são
complexas e demoradas
Verificação formal de sistemas complexos
Introdução – Verificação formal
5


Processo sistemático baseado em provas matemáticas
para verificar a correspondência entre espeficação e
implementação.
Processo estático – diferente da tradicional simulação


Não depende da qualidade/quantidade de vetores de
entrada
Comparativamente mais rápido que simulação.
Verificação formal de sistemas complexos
Verificação de equivalência
6
Modelo referência



X
Modelo verificado
Circuitos integrados sofrem diversas modificações de
nível de abstração até o circuito em silício
O sistema também sofre modificações estruturais
(circuito para testes, árvore de clock, etc.)
Simular o circuito em todos os níveis de abstração e
após cada modificação demanda muito tempo e
recursos computacionais.
Verificação formal de sistemas complexos
Verificação de equivalência
7

Utilizando a verificação de equivalência:
O modelo de mais alto nível é verificado quanto a
funcionalidade e dado como correto.
 O sistema em implementação é comparado com o modelo
correto a cada transformação estrutural ou de nível de
abstração
 Mais rápido e usa menos recursos que a simulação


Há várias ferramentas comerciais e é muito usado pelos
projetistas
Verificação formal de sistemas complexos
Verificação de equivalência
8
RTL
Equivalence
checking
d
Céllulas
lógicas
D
SET
Q
q
clk
CLR
Q
Equivalence
checking
Transistores
Verificação formal de sistemas complexos
Verificação de Modelo
9
Modelo do sistema



X
Especificação
A especificação é descrita por meio de
propriedades bem precisas
O modelo é expandido para todos os possíveis
estados
Todos os estados do modelo devem satisfazer as
propriedades especificadas
Verificação formal de sistemas complexos
Verificação de Modelo
10



Se todos o modelo satisfaz as propriedades para
todos os estados ele é correto
Se não, pode-se corrigir o modelo com a ajuda de
um contra-exemplo onde uma dada propriedade
falha
Relativamente novo para os projetistas
Verificação formal de sistemas complexos
Verificação de Modelo
11
Verificação formal de sistemas complexos
Dificuldades e problemas
12

Tamanho da lógica
 Complexidade
cresce exponencialmente com o espaço
de estados e numero de entradas.

Complexidade Inerente da lógica
 Mesmo
com um número pequeno de estados a lógica
envolvida pode ser muito complexa.

Complexidade de interface e protocolos
Verificação formal de sistemas complexos
Dificuldades e problemas
13

Lógica difusa
 Não
ligada às funcionalidades primárias
 Presente em todo o projeto

Recursos
A
complexidade tem impacto direto nos recursos
computacionais necessários.
Verificação formal de sistemas complexos
Mitigação dos problemas
14

Drivers VF
 Limitar
o espaço entradas eliminando as entradas
irreais.

Aplicação serial de propriedades
 Dividir
o conjunto de propriedades em máis de uma
análise

Divisão do espaço de entradas
 Dividir
o espaço de entradas em sub-espaços e aplicar
a verificação a cada um dos sub-espaços
Verificação formal de sistemas complexos
Mitigação dos problemas
15

Redução de lógica não influente


Para um conjunto de propriedades a lógica que não as
influecia pode ser eliminada da verificação reduzindo o
numero de estados.
Localização
Substituição de lógica interna por aleatoriedade
 Extrapolação de condições. Eficiência algoritmica


Combinação de algoritmos
Aproveitar as vantagens de cada um dos algoritmos
 Otimizar cobertura x recursos necessários

Verificação formal de sistemas complexos
Considerações e conclusões
16



Verificação formal não garante que o circuito é
100% correto
Verificação formal não substitui totalmente a
simulação
Pode ser usado em projetos grandes e complexos
Verificação formal de sistemas complexos
Considerações e conclusões
17



A verificação formal pode ser usada por qualquer
projetista
A verificação formal diminui o tempo do projeto
Verificação formal de modelos não é uma tarefa
trivial
Verificação formal de sistemas complexos
Considerações e conclusões
18



A verificação formal pode ser usada por qualquer
projetista
A verificação formal diminui o tempo do projeto
Verificação formal de modelos não é uma tarefa
trivial
Verificação formal de sistemas complexos
Considerações e conclusões
19

A verificação formal pode complementar a
verificação tradicional
 Aproveitar
as vantagens
 Contornar limitações
 Pode
aumentar e otimizar o alcance da verificação!
Verificação formal de sistemas complexos