Universidade Federal do Amazonas
PROGRAMA DE PÓS-GRADUAÇÃO EM ENGENHARIA ELÉTRICA
Verificação de Propriedades Temporais em
Filtros Digitais de Ponto-Fixo usando
Teorias do Módulo da Satisfatibilidade
Renato Abreu
[email protected]
1
Verificação de Sistemas
• Aplicado a hardware e software que em que a falha é inaceitável
• Métodos utilizados:
– Simulações e testes
– Métodos formais
- inserir entradas e observar saídas
- não cobre todas as possíveis combinações
- descreve o sistema usando lógica matemática
- garante corretude para todas as possíveis
Typecast
entradas e saídas
overflow!
2
Filtros Digitais
• Encontrados em:
–
–
–
–
–
carros
aeronaves
sistemas de comunicação
produtos eletrônicos
equipamentos médicos, etc
• Utilizados para:
– remoção de ruídos
– equalização de canal de comunicação
– análise espectral de sinais, etc
• Frequentemente implementados em:
– DSPs
– FPGAs
– Processadores de ponto fixo
3
Implementação em Ponto Fixo
Vantagens
Desvantagens
• Menor custo de hardware
• Efeitos de quantização
• Melhor desempenho (velocidade
• Menor intervalo dinâmico → overflow
e consumo de energia)
Referência
Overflow
• Ciclo limite
Filtro estável: anulando a
entrada a saída deve ir pra zero
Porém, em
ponto fixo...
Referência
Com quantização (10 bits)
Wrap-around
4
Aspectos da Implementação de Filtros
• Projeto de filtros feito em ponto flutuante, mas a implementação é
feita em ponto fixo
• Simulações e testes extensivos são insuficientes para detectar
todos os possíveis problemas (Cox et al., 2012)
• Determinar o comprimento da palavra (bits para parte inteira e parte
fracionária) considerando:
– Precisão
– Desempenho
– Custo
5
Objetivos
• Detectar problemas em filtros digitais em ponto fixo utilizando um
verificador BMC baseado em SMT
– Verificação de overflow, ciclo limite, restrições temporais e nível de
ruídos através de um BMC de prateleira
– Verificação de filtros de diversos tipos e com diferentes formatos de
ponto fixo
– Aprimorar implementação para diminuir tempo de verificação
– Verificação de benchmarks e comparação dos resultados
6
Implementação de Filtros
• 𝑦 𝑛 =−
𝑁
𝑘=1 𝑎𝑘
y n−k +
𝑀
𝑘=0 𝑏𝑘
x n−k
Sistema linear invariante no tempo
𝑀
−𝑘
float iirFilterI()
𝑌(𝑧)
𝑘=0 𝑏𝑘 𝑧
𝐻 𝑧 =
=
{
−𝑘
𝑋(𝑧) 1 + 𝑁
𝑘=1 𝑎𝑘 𝑧
float yn = 0;
for (int k = 0; k < M; k++)
{
yn += *b++ * *x--;
}
for (int k = 1; k < N; k++)
{
yn -= *a++ * *y--;
}
return yn;
}
Forma Direta I
7
Modelo Realista com Quantização
Quantização da
entrada
Quantização nas
operações intermediárias
DSPs modernos possuem
acumuladores para
armazenar os resultados
com maior
Quantização
dos precisão
Q(x)
coeficientes
2k-1-2-l
Máximo
2-l
2-l-1
Arredondamento:
-2-l-1 ≤ e(x) ≤ 2-l-1
Mínimo
-2k-1
Complemento de dois, k bits inteiros, l bits de precisão
8
Lógica Proposicional
• A sintaxe das fórmulas em lógica proposicional por:
𝐹𝑚𝑙 ∷= 𝐹𝑚𝑙 ∧ 𝐹𝑚𝑙 ¬𝐹𝑚𝑙
𝐹𝑚𝑙 | 𝐴𝑡𝑜𝑚
𝐴𝑡𝑜𝑚 ∷= 𝑉𝑎𝑟𝑖á𝑣𝑒𝑙 𝑡𝑟𝑢𝑒 𝑓𝑎𝑙𝑠𝑒
• Um solucionador SAT é um algoritmo que toma como entrada uma
fórmula ϕ na forma normal conjuntiva e decide se ela é satisfatível
ou insatisfatível
– Ex. 1:
( 1 ∨ 0 )⋀( 1 ∨ 0 ) ≡ 1
É satisfatível pois a fórmula é
verdadeira, por exemplo para:
𝑥1 ↦ 1, 𝑥2 ↦ 0, 𝑥3 ↦ 1, 𝑥4 ↦ 0
(𝑥1 ∨ 𝑥2)⋀(¬𝑥1 ∨ ¬𝑥2)
É insatisfatível pois a fórmula é
falsa para qualquer valor 𝑥1 e 𝑥2
(𝑥1 ∨ 𝑥2)⋀(𝑥3 ∨ 𝑥4)
– Ex. 2:
9
Teoria da Satisfatibilidade
• Um solucionador SMT decide sobre a satisfatibilidade de uma
fórmula de primeira ordem usando diferentes teorias de suporte e
então generaliza a satisfatibilidade proposicional
Teoria
Igualdade
Vetor de bits
Aritmetica linear
Exemplo
𝑥1 = 𝑥2 ∧ ¬(𝑥1 = 𝑥3) ⇒ ¬ 𝑥1 = 𝑥3
𝑏 ≫ 𝑖 &1 = 1
(4𝑦1 + 3𝑦2 ≥ 4) ∨ (𝑦2 − 3𝑦3 ≤ 3)
Arrays
𝑗 =𝑘∧𝑎 𝑘 =2 ⇒𝑎 𝑗 =2
Teorias combinadas
𝑗 ≤𝑘∧𝑎 𝑗 =2 ⇒𝑎 𝑖 <3
𝑘, 𝑙 × 𝑘, 𝑙 = 2𝑘, 2𝑙
2𝑘, 2𝑙 ≫ 𝑓 = 2𝑘, 𝑓
Verificar
overflow
10
BMC baseado em SMT
• Tem sido aplicado para verificação de softwares sequenciais
• Verifica a negação de uma determinada propriedade a uma
determinada profundidade
• Sistema de transição de estados M desdobrado k vezes
– Estado: contador de programa e variáveis do programa
– Desdobramento a partir do fluxo de controle (loops, trocas de contexto)
• Traduzido em uma condição de verificação ψ tal que
– ψ é satisfatível se e somente se ϕ tem um contraexemplo em uma
profundidade de no máximo k
11
BMC usando o ESBMC
OK
Código
C/C++
Fluxo de
controle
Programa
em GOTO
Forma
SSA
Conversão de
restrições e
Contexto propriedades
Lógico
Solver
SMT
Contraexemplo
12
Verificação de Filtros Digitais
• Projetar o filtro usando o método e ferramenta de preferência
• Estimar intervalo de saída para uma dada faixa de entrada
– Definir o comprimento da palavra, levando em conta o custo, problemas
de quantização e desempenho
• Entrar com parâmetros do filtro no modelo de estrutura em C
• Realizar análise do pior caso de tempo de execução (WCET)
• Configurar assertivas no modelo em C
–
–
–
–
Overflow
Ciclo limite
Restrições temporais
Outras propriedades (propriedades de projeto, SNR, etc)
• Executar verificação e caso falhe, obter contraexemplo
13
Exemplo1: Verificação de Overflow
• Filtro IIR com as seguintes especificações
–
–
–
–
Butterworth corta-faixa de 2ª ordem
Frequências de corte: 7 e 10 kHz
Frequência de amostragem: 48 kHz
Atenuação nas frequências de corte: 3dB
x(n)
0,75
y(n)
-0,703125
-0,703125
0,75
-0,5
14
Exemplo1: Verificação de Overflow
• Estimando o intervalo para a saída:
– Para um sistema estável, 𝑦 𝑛 ≤ 𝑥𝑚𝑎𝑥 ∞
𝑘=−∞ ℎ𝑘
– No Matlab a função impz calcula a resposta ao impulso ℎ
•
100
𝑘=0
ℎ𝑘 = 1,8178
•
Para x entre [-1,1], 𝑦 𝑛
•
Representando em 2, 6
≤ 1,82
-
Intervalo [-2, 1,984375]
-
Erro ±0,0078125
15
Exemplo1: Verificação de Overflow
• O verificador aplica entradas não-determinísticas dentro do intervalo
[-1,1] em busca da negação de:
– 𝑙𝑜𝑣𝑒𝑟𝑓𝑙𝑜𝑤 ⟺ (−2 ≤ 𝐹𝑃) ∧ (𝐹𝑃 ≤ 1,984375)
• Aqui a verificação retorna a seguinte entrada como contraexemplo:
– x = { 0.0f, 0.015625f, 0.0f, -0.890625f, 0.96875f, -0.890625f }
– xaux = { -0.890625f, 0.96875f, -0.890625f }
– yaux = { 0f, -0.671875f, 0.890625f }
-2,03125
-0,890625 × 0,75 = -0,6718750
+
0,968750 × -0,703125 = -0,6875
-0,703125
+
0,75 = -0,671875
-0,890625 × 0,75
+
-0,5
O filtro também falha
se implementado na
Forma Direta II, mas
não falha na Forma
Transposta II devido a
ordem de execução
das operações
16
Exemplo 2: Verificação de Ciclo Limite
• Filtro IIR de um pólo com 2 bits para inteiros e 4 bits de precisão
𝑦 𝑛 = −0,5 y n − 1 + x n
−0,5
Q[−0,5 ]
Wrap around
17
Verificação de Ciclo Limite
• Utilizamos uma entrada nula e valores não determinísticos para as
saídas anteriores
• Uma assertiva detecta uma falha caso o conjunto de estados
anteriores das saídas se repetir
Repetição com
entrada nula.
Ciclo Limite!
y
y(3) == -0,0625
y(2)
y(1)
y(0)
0,0625
=0
−𝟎, 𝟓
-0,0625
0,0625
-1
0
1
2
3
n
-0,0625
0,0625
0,125
18
Verificação de Restrições Temporais
• Baseada na análise de tempo de execução do pior caso (WCET)
• Exemplo de operação em um trecho de código para MSP430:
float iirFilterI() {
float yn = 0;
for (int k = 0; k < M; k++){
yn += *b++ * *x--;
} sum += *b++ * *x--;
for (int k = 1; k < N; k++){
yn -= *a++ * *y--;
}
return yn;
}
MOV.W
MOV.W
SUB.W
MOV.W
MOV.W
CALL
MOV.W
MOV.W
CALL
MOV.W
MOV.W
@r9+,r12
@r9+,r13
#4,r10
4(r10),r14
6(r10),r15
#__fs_mpy
r7,r14
r8,r15
#__fs_add
r12,r7
r13,r8
5 cycles
5 cycles
5 cycles
3 cycles
3 cycles
5 cycles
1 cycle
1 cycle
5 cycles
1 cycle
1 cycle
• Quantidade de instruções
• O verificador aplica uma entrada qualquer emdependerá
busca dadanegação
ordem dode
filtro.
• Duração das operações
– 𝑙𝑡𝑖𝑚𝑖𝑛𝑔 ⟺ (𝑁 × 𝑇) ≤ 𝐷
Deadline
dependerá da plataforma e do
tamanho da palavra
Número de ciclos Duração do ciclo
19
Avaliação Experimental
• Ambiente:
–
–
–
–
Intel Core i7-2600, 3.40 GHz com 24 GB de RAM, Fedora 64-bits
ESBMC v1.21
SMT solver Z3 v3.2, usando aritmética de vetor de bits
Timeout: 3600 segundos
• Filtros verificados
– obtidos da literatura ou projetados no Matlab
– Fs = 48KHz (típica em áudio)
– restrição temporal baseada em Fs de 48 KHz e clock de 16 MHz
(MSP430)
• Benchmarks disponíveis em www.esbmc.org
20
NúmeroNúmero
de Soma
de do módulo
Intervalo de Bits para
Tamanho
Tipo de
Tipo de
coeficientes
coeficientes
de da resposta
entrada
ao para
parte inteira
da entrada
filtro
falha obtida
realimentação
diretos impulsoaplicaçãoe fracionária
aplicada
Resultados
Tempo de
verificação (s)
OF
LC
TC
#
Filtro
Na
Nb
∑|hk|
Entrada
Bits
xsize
1
LP-IIR
2
1
2
[-1,1]
<2,4>
6
2
LP-Butterworth-IIR
3
3
1.2 Verificados
[-1.6,1.6]
<2,5>tipos 6
diferentes
3
LP-IIR
3
1
de diversas
ordens6
4 de filtros
[-1,1]
<3,4>
4
LP-IIR
3
1
1.56
[-1,1]
5
LP-FIR
1
31
1.93
[-1,1]
6
HP-ChebyshevI-IIR
3
3
7
BP-Elliptic-IIR
3
3
8
BS-Butterworth-IIR
3
3
9
BP-Elliptic-IIR
5
5
0.91
[-1.1,1.1]
<1,8>
10
OF, LC
7
20
<1
10
HP-Butterworth-IIR
5
5
1.58
[-1.27, 1.27]
<2,6>
10
LC
2468
1508
<1
11
BP-ChebyshevI-IIR
5
5
1.51
[-1.33, 1.33]
<2,6>
10
-
TO
TO
<1
12
HP-Elliptic-IIR
7
7
5.39
[-1,1]
<3,13>
14
TC
73
TO
<1
<2,4>
6
Falhas
OF, LC
39 de 4
Rápida
verificação
restrição
OF temporal.
579
634
Código sequencial.
<1
<1
OF, LC
210
29
<1
-
110
51
<1
<2,6> detectado
31
TC
TO
98
1
Overflow
para estimativa
1.33
[-1,1] mesmo
<2,10>
6
- verificação
853 de
2058
Rápida
filtros<1
de
conservadora
baixa
e com474
pequeno
1.24 Falha
[-1.0,1.0]
<2,10>
6
LC ordem
de restrição
Alto
tempo546
de verificação<1
tamanho de palavra
temporal
para filtros<2,8>
de
de
1.81
[-1.0,1.0]
6
OFfiltros mais
106 complexos
1299
<1
maior ordem
OF - Overflow, LC - Ciclo limite, TC - restrição temporal, TO - Time out
21
Conclusões
• Conclusões gerais
– Foi proposta uma abordagem para verificação de filtros digitais
utilizando um verificador BMC baseado em SMT
– Permite encontrar problemas relacionados a representação em ponto
fixo
– É possível detectar problemas que seriam difíceis de identificar através
de testes e simulações
• Contribuições
– Exploramos as vantagens do verificador de prateleira ESBMC em cima
de um modelo em C
– Estendemos a abordagem com a verificação de restrições temporais
baseadas em WCET em conjunto com o BMC
• Observações
– Alto tempo de verificação para filtros mais complexos
22
Trabalhos Futuros
• Aplicação do método para outras formas de filtros
– Forma Direta II, Forma Transposta, em Cascata, em Paralelo, etc
• Aumentar eficiência do sistema de verificação
– Implementação de uma biblioteca de ponto fixo
• Adicionar mais propriedades para verificação
– Especificações da resposta em frequência
– Nível de ruído (SNR)
• Outras aplicações em processamento digital de sinais
– Verificação de sistema OFDM
23
OBRIGADO!
24
Metodologia de Desenvolvimento
Tabela - Cronograma de atividades
26
Implementação de Filtros
• 𝑦 𝑛 =−
𝑁
𝑘=1 𝑎𝑘
y n−k +
𝑀
𝑘=0 𝑏𝑘
x n−k
Sistema linear invariante no tempo
Forma em Cascata
Forma
FormaTransposta
Direta III II
Forma
Direta
Forma em Paralelo
𝑀
−𝑘
𝑌(𝑧)
𝑘=0 𝑏𝑘 𝑧
𝐻 𝑧 =
=
−𝑘
𝑋(𝑧) 1 + 𝑁
𝑘=1 𝑎𝑘 𝑧
27
Representação em Ponto Fixo
• Representação em complemento de dois
• ⟨k, l⟩ sendo k bits para parte inteira e l bits para fracionária
• Um bit de sinal
• (bk−1 bk−2 ... b1 b0 · b−1 b−2 ... b−l)
• 𝑋 = −𝑏𝑘−1 2𝑘−1 +
−𝑙
𝑖
𝑏
2
𝑖
𝑖=𝑘−2
• Valor máximo 2𝑘−1 − 2−𝑙
• Valor mínimo −2𝑘−1
28
Fórmulas Lógicas
29
Referências
• Verificação de modelos
–
–
–
L. de Moura et al., “Z3: An efficient SMT solver,” TACAS, 2008
L. Cordeiro et al. “SMT-based bounded model checking for embedded ANSI-C software,” IEEE
Transactions on Software Engineering, 2012
E. Clarke et al., “A tool for checking ANSI-C programs,” TACAS, 2004
• Verificação de restrições temporais
–
–
S. Kim et al., “Using a model checker to determine worstcase execution time,” Columbia
University Reports, 2009
R. Barreto et al., “Verifying Embedded C Software with Timing Constraints Using an Untimed
Bounded Model Checker,” SBESC, 2011
• Verificação de filtros digitais
–
–
–
–
D.A. Bailey and A.A. Beex, “Simulation of filter structures for fixedpoint implementation,”
Proceedings of the 28th Southeastern Symposium on System Theory, 1996
Behzad Akbarpour and Sofiène Tahar, “Error analysis of digital filters using HOL theorem
proving,” Journal of Applied Logic, 2007
C.F. Fang et al., “Fast, accurate static analysis for fixed-point finite-precision effects in DSP
designs,” ICCAD, 2003
A. Cox et al., “A bit too precise? Bounded verification of quantized digital filters,” TACAS, 2012
30