Çıktı Yönelimli Teknik Etkinlik: Bir üretim biriminin mevcut girdilerini en

O m´odulo de identifica¸c˜ao de similaridades ´e respons´avel por encontrar similari- dades estruturais entre os circuitos que est˜ao sendo verificados. As similaridades encontradas podem ser utilizadas para diminuir o espa¸co de busca dos resolve- dores SAT, diminuindo a complexidade do problema a ser resolvido.

Durante o presente trabalho foi desenvolvido um m´odulo de identifica¸c˜ao de similaridades baseado em cl´ausulas de conflito geradas pelo resolvedor SAT durante o processamento do problema. O Cap´ıtulo 4 ´e dedicado ao m´odulo de identifica¸c˜ao de similaridades desenvolvido.

Explorando as similaridades

estruturais

Na maioria dos ambientes de projetos de circuitos, Equivalence Checking ´e apli- cada para estabelecer a equivalˆencia entre duas descri¸c˜oes de um circuito. Tipi- camente uma descri¸c˜ao ´e derivada de outra atrav´es de v´arios passos, que s˜ao partes do processo de projeto do circuito. Muitos destes passos possuem um pe- queno efeito na estrutura global do circuito. Desta forma, ´e bastante prov´avel que existam similaridades estruturais entre os circuitos a serem verificados, ou seja, n˜ao somente as sa´ıdas s˜ao funcionalmente equivalentes mas alguns sinais in- ternos tamb´em. Por exemplo, quando ´e verificada a exatid˜ao de um processo de mapeamento de tecnologia, ambos os circuitos tˆem uma estrutura global muito parecida. Outro exemplo ´e a verifica¸c˜ao de um circuito que teve altera¸c˜oes manuais realizadas pela equipe de projetistas, onde apenas pequenas partes do circuito foram provavelmente alteradas.

As similaridades estruturais possuem um papel de grande importˆancia em Equivalence Checking. Algumas vezes ´e muito dif´ıcil verificar todo o miter (cir- cuitos a serem verificados com as sa´ıdas alimentando uma porta l´ogica XOR) por completo, devido ao seu tamanho. J´a se constatou que o grau de dificul- dade da Equivalence Checking depende, principalmente, do tamanho do miter e n˜ao do tamanho da l´ogica que o envolve[1]. Desta forma a identifica¸c˜ao de similaridades estruturais pode ser bastante ´util para o processo de Equivalence Checking. As t´ecnicas que exploram estas similaridades reduzem a complexi- dade do problema a ser resolvido, identificando sinais do circuito idˆenticos. Se dois sinais dos circuitos a serem verificados s˜ao idˆenticos, estes sinais podem ser unidos e apenas uma das l´ogicas, associada aos sinais, deve ser verificada. Esta

Figura 4.1: Circuitos contendo equivalˆencias internas

redu¸c˜ao na quantidade de l´ogica dos circuitos pode apresentar uma redu¸c˜ao sig- nificativa no problema de verifica¸c˜ao dos circuitos. Na Figura 4.1 pode ser visto um miter, composto por dois circuitos a serem verificados, que possuem pontos de equivalˆencia estrutural internos.

Basicamente, o processo de explorar as similaridades estruturais entre os circuitos consiste de dois passos. Iniciando a partir das entradas prim´arias e movendo em dire¸c˜ao `as sa´ıdas:

1. Identifique equivalˆencias entre os sinais internos do miter;

2. Substitua os n´os correspondentes por seus equivalentes identificados.

Por fim, ´e necess´ario provar a equivalˆencia dos circuitos provando a satisfa- bilidade da sa´ıda do miter.

Um exemplo de como as similaridades estruturais podem ser utilizadas para reduzir a complexidade dos circuitos a serem verificados ´e mostrado na Figura 4.2.

Inicialmente s˜ao mostrados os dois circuitos a serem verificados com suas sa´ıdas alimentando a porta l´ogica XOR, como pode ser visto na Figura 4.2(a). Ao lado direito ´e apresentada a primeira similaridade estrutural identificada, entre os sinais d e e. Como os sinais d e e s˜ao iguais, eles podem ser ligados e a l´ogica de maior complexidade associada aos sinais ´e removida. A Figura 4.2(b) mostra o circuito resultante da uni˜ao dos dois sinais. Ao lado direito, ´e mostrado

Circuito Similaridade identificada

a)

b)

c)

d)

Figura 4.2: Utiliza¸c˜ao de similaridades estruturais internas entre os circuitos a segunda similaridade estrutural identificada: os sinais h e j s˜ao idˆenticos. Seguindo o mesmo procedimento, os sinais h e j s˜ao ligados e novamente a l´ogica de maior complexidade associada aos sinais ´e suprimida. A Figura 4.2(c) apresenta o circuito resultante do ´ultimo passo da identifica¸c˜ao. Por fim, como as duas entradas da porta l´ogica XOR s˜ao alimentadas pelo mesmo sinal, ´e realizada uma nova simplifica¸c˜ao do circuito que conduz ao circuito final ap´os a identifica¸c˜ao de todas as similaridades estruturais internas, como mostrado na Figura 4.2(d).

Diversos m´etodos foram propostos para realizar a identifica¸c˜ao de similari- dades estruturais entre os circuitos, dentre eles:

• Aplicar padr˜oes randˆomicos para determinar candidatos para pares de sinais equivalentes e ent˜ao provar a equivalˆencia atrav´es de SAT ou ATPG [1];

dizado recursivo [32]

• Utilizar BDDs locais para identificar parti¸c˜oes do circuito relevantes[50][51][52]. Neste trabalho ´e proposta uma nova metodologia para identifica¸c˜ao de sim- ilaridades estruturais, baseado em cl´ausulas de conflito geradas durante a veri- fica¸c˜ao dos circuitos pelo resolvedor SAT.

Algumas das vantagens da abordagem proposta s˜ao:

• N˜ao ´e necess´ario um conhecimento pr´evio da estrutura do circuito. Baseado nas cl´ausulas CNF geradas a partir do circuito, o resolvedor gera, durante o seu curso, cl´ausulas de conflito.

• A metodologia aproveita as cl´ausulas geradas a partir da resolu¸c˜ao para encontrar as similaridades, ou seja, o aumento de tempo introduzido por esta metodologia ´e menor do que em outras t´ecnicas.

As pr´oximas subse¸c˜oes s˜ao dedicadas `a apresenta¸c˜ao da metodologia.

4.1

Metodologia de identifica¸c˜ao de similaridades

estruturais a partir de cl´ausulas de conflito

A metodologia proposta utiliza cl´ausulas de conflito geradas pelo resolvedor SAT para identificar similaridades estruturais entre os circuitos a serem verificados.

Para permitir o perfeito entendimento da metodologia, ´e necess´ario conhec- imento sobre os resolvedores SAT e a maneira como estes geram as cl´ausulas de conflito utilizadas para a identifica¸c˜ao das similaridades estruturais. Portanto, a Se¸c˜ao 4.1.1 apresenta uma breve explica¸c˜ao sobre o processo de resolu¸c˜ao SAT e a gera¸c˜ao de cl´ausulas de conflito. A Se¸c˜ao 4.1.2 ´e dedicada `a apresenta¸c˜ao da metodologia.

4.1.1

Gera¸c˜ao de cl´ausulas de conflito em resolvedores