Manufactura industrial
Internet industrial de las cosas | Materiales industriales | Mantenimiento y reparación de equipos | Programación industrial |
home  MfgRobots >> Manufactura industrial >  >> Industrial programming >> VHDL

Verificación aleatoria restringida

La verificación aleatoria restringida es una estrategia de banco de pruebas que se basa en generar transacciones pseudoaleatorias para el dispositivo bajo prueba (DUT). El objetivo es lograr una cobertura funcional de una serie de eventos predefinidos a través de la interacción aleatoria con el DUT.

La Metodología de verificación de VHDL de código abierto (OSVVM) es una biblioteca de VHDL gratuita que incluye varios paquetes convenientes para crear bancos de pruebas aleatorios restringidos. Estamos particularmente interesados ​​en RandomPkg y CoveragePck, que usaremos en este artículo. Recomiendo visitar la página OSVVM GitHub para obtener más información sobre las características de esta biblioteca.

El dispositivo bajo prueba

Voy a sumergirme directamente en un ejemplo para explicar mejor en qué se diferencia un banco de pruebas aleatorio restringido del banco de pruebas clásico, que usa pruebas dirigidas. Creamos un FIFO de búfer de anillo en el artículo anterior de este blog, pero no creamos un banco de pruebas de autocomprobación para verificar la corrección del módulo.

Vamos a crear un banco de pruebas adecuado para el FIFO del búfer de anillo que utiliza verificación aleatoria restringida.

entity ring_buffer is
  generic (
    RAM_WIDTH : natural;
    RAM_DEPTH : natural
  );
  port (
    clk : in std_logic;
    rst : in std_logic;

    -- Write port
    wr_en : in std_logic;
    wr_data : in std_logic_vector(RAM_WIDTH - 1 downto 0);

    -- Read port
    rd_en : in std_logic;
    rd_valid : out std_logic;
    rd_data : out std_logic_vector(RAM_WIDTH - 1 downto 0);

    -- Flags
    empty : out std_logic;
    empty_next : out std_logic;
    full : out std_logic;
    full_next : out std_logic;

    -- The number of elements in the FIFO
    fill_count : out integer range RAM_DEPTH - 1 downto 0
  );
end ring_buffer;

La entidad del módulo de búfer de anillo se muestra en el código anterior. Vamos a tratar el DUT como una caja negra, lo que significa que no asumiremos ningún conocimiento de cómo se implementa el DUT. Después de todo, este artículo trata sobre el banco de pruebas, no sobre el FIFO del búfer de anillo.

Instanciaremos el DUT en el banco de pruebas usando el método de instanciación de entidades. La creación de instancias es trivial, por lo que omitiré el código por ahora, pero se puede descargar más adelante en este artículo.

Los genéricos DUT se asignarán a los siguientes valores:

Estrategia de banco de pruebas

Repasemos la estrategia de prueba antes de comenzar a implementar algo. La siguiente imagen muestra el concepto principal del banco de pruebas que estamos a punto de crear.

Realizaremos transacciones de escritura aleatorias en el lado de entrada del DUT. Los datos de entrada se establecerán en un valor aleatorio en cada ciclo de reloj, y las luces estroboscópicas en la entrada de habilitación de escritura tendrán una duración aleatoria.

Del mismo modo, realizaremos lecturas al azar. Haremos valer la señal de habilitación de lectura en ráfagas que duran un número aleatorio de ciclos de reloj.

Habrá un modelo de comportamiento en paralelo con el DUT. Este es un FIFO que se implementa de manera diferente al búfer de anillo que se usa en el DUT, pero aún tiene la misma interfaz. A diferencia del DUT, el modelo de comportamiento no tiene que ser sintetizable. Esto nos da la libertad de usar funciones avanzadas de programación VHDL para crearlo.

Compararemos la salida del DUT con la salida del modelo de comportamiento en un proceso separado. Este proceso será el único responsable de hacer esta comparación en cada ciclo de reloj mediante declaraciones de afirmación. Si las dos implementaciones FIFO se comportan de manera diferente en cualquier momento, una falla de aserción hará que la simulación termine con un error.

Finalmente, recopilaremos datos de cobertura funcional observando las transacciones que van y vienen del DUT. Un punto de cobertura funcional podría significar, por ejemplo, una lectura y escritura simultáneas, o que el FIFO se llene al menos una vez. Supervisaremos estos eventos en nuestro proceso principal del secuenciador del banco de pruebas. La simulación se detendrá cuando se hayan producido todos los eventos de cobertura funcional que estamos monitorizando.

Importación de la biblioteca OSVVM

La biblioteca OSVVM se puede utilizar con cualquier simulador compatible con VHDL-2008. Es posible que ya esté incluido con las bibliotecas predeterminadas que vienen con su simulador. Está incluido en ModelSim PE Student Edition, que se puede descargar de forma gratuita desde Mentor Graphics.

ModelSim viene con una versión anterior de OSVVM, pero está bien, tiene todo lo que necesitamos. Podemos seguir adelante e importar los paquetes aleatorios y de cobertura como este:

library osvvm;
use osvvm.RandomPkg.all;
use osvvm.CoveragePkg.all;

La última versión de la biblioteca OSVVM siempre se puede descargar desde la página de GitHub. Haga esto si su simulador no lo tiene incluido o si desea utilizar las últimas funciones de la biblioteca.

Declaración de las variables OSSVM

La biblioteca OSVVM contiene paquetes con tipos protegidos. Las variables creadas a partir de ellas tendrían un alcance limitado al proceso en el que se definieron. Por lo tanto, las declararemos como variables compartidas en la región declarativa de la arquitectura del banco de pruebas, como se muestra en el código a continuación.

 -- OSVVM variables
  shared variable rv : RandomPType;
  shared variable bin1, bin2, bin3, bin4, bin5, bin6 : CovPType;

El rv variable de tipo RandomPType es para generar valores aleatorios. Solo necesitamos uno de estos, porque podemos usar el mismo objeto en cada proceso donde necesitamos generar valores aleatorios. La última línea de código declara seis variables de tipo CovPType .

Declaramos seis variables de cobertura porque vamos a tener seis objetivos de cobertura, nos referiremos a estos objetos como "contenedores". Las variables compartidas deben inicializarse antes de que puedan utilizarse para recopilar datos de cobertura. Hacemos esto llamando al AddBins procedimiento en cada uno de los CovPType contenedores.

    -- Set up coverage bins
    bin1.AddBins("Write while empty", ONE_BIN);
    bin2.AddBins("Read while full", ONE_BIN);
    bin3.AddBins("Read and write while almost empty", ONE_BIN);
    bin4.AddBins("Read and write while almost full", ONE_BIN);
    bin5.AddBins("Read without write when almost empty", ONE_BIN);
    bin6.AddBins("Write without read when almost full", ONE_BIN);

Proporcionamos una descripción de cadena del contenedor de cobertura como primer parámetro para el AddBins procedimiento. Esta cadena volverá a aparecer al final de la simulación cuando imprimamos las estadísticas para cada uno de los intervalos de cobertura. Como puede ver en las descripciones de texto, vamos a utilizar los contenedores para comprobar si se han producido o no algunos casos de esquina muy específicos.

AddBins es un procedimiento sobrecargado que se puede usar para crear varios marcadores dentro de las variables bin. Sin embargo, solo tendremos un marcador asociado a cada contenedor. Por lo tanto, proporcionaremos la constante de conveniencia ONE_BIN como parámetro del AddBins procedimiento. Esto inicializará el CovPType variables con un contenedor cada una. Los marcadores representados por los bins se consideran cubiertos cuando los eventos que monitorean se han producido al menos una vez.

Generando entrada aleatoria

Comencemos creando el proceso que genera datos de entrada al DUT. El FIFO del búfer circular está diseñado para ignorar los intentos de sobrescritura y sobrelectura. Por lo tanto, podemos simplemente escribir datos aleatorios en ráfagas de duración aleatoria. No tenemos que pensar si el DUT realmente está listo para absorber los datos o no.

  PROC_WRITE : process
  begin
    wr_en <= rv.RandSlv(1)(1) and not rst;

    for i in 0 to rv.RandInt(0, 2 * RAM_DEPTH) loop
      wr_data <= rv.RandSlv(RAM_WIDTH);
      wait until rising_edge(clk);
    end loop;
  end process;

La única consideración que toma este proceso es que el DUT no está en reinicio. Habilitamos o deshabilitamos aleatoriamente la señal de habilitación de escritura en la primera línea de este proceso, pero solo se habilitará si rst es '0' .

El bucle for subsiguiente escribirá datos aleatorios en el dispositivo bajo prueba durante un número aleatorio de ciclos de reloj, incluso si la señal de habilitación no está activa. Podemos hacer esto porque se supone que el DUT ignora el wr_data puerto a menos que el wr_en la señal es '1' . Después del ciclo for, el programa regresará al inicio del proceso, desencadenando otra transacción de escritura aleatoria.

Realización de lecturas aleatorias

El proceso que lee datos del DUT es similar al proceso de escritura. Podemos activar aleatoriamente el rd_en señal en cualquier momento porque el DUT está diseñado para ignorar los intentos de lectura cuando está vacío. Los datos que aparecen en el rd_data el puerto no está realmente marcado. Este proceso solo controla la señal de habilitación de lectura.

  PROC_READ : process
  begin
    rd_en <= rv.RandSlv(1)(1) and not rst;

    for i in 0 to rv.RandInt(0, 2 * RAM_DEPTH) loop
      wait until rising_edge(clk);
    end loop;
  end process;

Verificación de comportamiento

Construiremos un modelo de comportamiento del DUT dentro de nuestro banco de pruebas para verificar su comportamiento. Esta es una estrategia de banco de pruebas bien conocida. Primero, alimentamos el modelo de comportamiento simultáneamente con la misma entrada que el DUT. Luego, podemos comparar la salida de los dos para verificar si el DUT tiene el comportamiento correcto.

La imagen de arriba muestra el diseño básico de dicho banco de pruebas. El modelo de comportamiento funciona en paralelo con el DUT. Lo usamos como modelo para comparar las salidas del DUT.

El banco de pruebas FIFO

Usaremos una lista enlazada para implementar el modelo de comportamiento. Las listas enlazadas no se pueden sintetizar, pero son perfectas para bancos de pruebas. Puede recordar Cómo crear una lista enlazada en VHDL artículo si eres un lector asiduo de este blog. Usaremos su código para implementar el modelo de comportamiento para el FIFO del búfer circular.

package DataStructures is
   type LinkedList is protected
 
      procedure Push(constant Data : in integer);
      impure function Pop return integer;
      impure function IsEmpty return boolean;
 
   end protected;
end package DataStructures;

La declaración del paquete para la lista enlazada FIFO se muestra en el código anterior. Es un tipo protegido que tiene las tres funciones; Empuje, haga estallar y está vacío. Estos se utilizan para agregar y eliminar elementos del FIFO, así como para verificar si quedan cero elementos en él.

  -- Testbench FIFO that emulates the DUT
  shared variable fifo : LinkedList;

Los tipos protegidos son construcciones similares a clases en VHDL. Crearemos un objeto de la lista enlazada declarando una variable compartida en la región declarativa del banco de pruebas, como se muestra en el código anterior.

El modelo de comportamiento

Para emular completamente el comportamiento del FIFO del búfer de anillo, declaramos dos nuevas señales que reflejan las señales de salida del DUT. La primera señal contiene los datos de salida del modelo de comportamiento y la segunda es la señal válida asociada.

  -- Testbench FIFO signals
  signal fifo_out : integer;
  signal fifo_out_valid : std_logic := '0';

El código anterior muestra la declaración de las dos señales de salida del modelo de comportamiento. No necesitamos señales de entrada dedicadas para el modelo de comportamiento, porque son las mismas que están conectadas al DUT. Usamos señales para emular la salida del dispositivo bajo prueba porque nos permite recopilar fácilmente datos de cobertura, como veremos más adelante en este artículo.

PROC_BEHAVIORAL_MODEL : process
begin
  wait until rising_edge(clk) and rst = '0';

  -- Emulate a write
  if wr_en = '1' and full = '0' then
    fifo.Push(to_integer(unsigned(wr_data)));
    report "Push " & integer'image(to_integer(unsigned(wr_data)));
  end if;
    
  -- Emulate a read
  if rd_en = '1' and empty = '0' then
    fifo_out <= fifo.Pop;
    fifo_out_valid <= '1';
  else
    fifo_out_valid <= '0';
  end if;
  
end process;

El proceso que implementa el modelo de comportamiento del FIFO del búfer de anillo se muestra en el código anterior. Este proceso se activará en cada flanco ascendente del reloj, si la señal de reinicio no está activa.

El modelo de comportamiento envía un nuevo valor al FIFO del banco de pruebas cada vez que wr_en la señal se afirma mientras el full la señal es '0' . De manera similar, la lógica de lectura en el proceso del modelo de comportamiento funciona al escuchar el rd_en y empty señales Este último está controlado por el DUT, pero verificaremos que esté funcionando en el siguiente proceso que crearemos.

Comprobación de las salidas

Toda la lógica responsable de verificar las salidas del DUT se recopila en un proceso llamado «PROC_VERIFY». Estamos utilizando declaraciones de aserción para verificar que las salidas del DUT coincidan con las del modelo de comportamiento. También verificamos que el DUT y el modelo de comportamiento coincidan cuando el FIFO está vacío.

El código para el proceso de verificación se muestra a continuación.

PROC_VERIFY : process
begin
  wait until rising_edge(clk) and rst = '0';
  
  -- Check that DUT and TB FIFO are reporting empty simultaneously
  assert (empty = '1' and fifo.IsEmpty) or
         (empty = '0' and not fifo.IsEmpty)
    report "empty=" & std_logic'image(empty) 
      & " while fifo.IsEmpty=" & boolean'image(fifo.IsEmpty)
    severity failure;

  -- Check that the valid signals are matching
  assert rd_valid = fifo_out_valid
    report "rd_valid=" & std_logic'image(rd_valid) 
      & " while fifo_out_valid=" & std_logic'image(fifo_out_valid)
    severity failure;

  -- Check that the output from the DUT matches the TB FIFO
  if rd_valid then
    assert fifo_out = to_integer(unsigned(rd_data))
      report "rd_data=" & integer'image(to_integer(unsigned(rd_data)))
        & " while fifo_out=" & integer'image(fifo_out)
      severity failure;
      report "Pop " & integer'image(fifo_out);
  end if;

end process;

El proceso se desencadena por el flanco ascendente del reloj, como podemos ver en la primera línea de código. El DUT es un proceso cronometrado, y también se espera que la lógica descendente que está conectada al DUT esté sincronizada con la señal del reloj. Por lo tanto, tiene sentido verificar las salidas en el flanco ascendente del reloj.

El segundo bloque de código comprueba que el empty la señal que proviene del dispositivo bajo prueba se confirma solo cuando el FIFO del banco de pruebas está vacío. El DUT y el modelo de comportamiento tienen que estar de acuerdo en que FIFO está vacío o no para que pase esta prueba.

Luego sigue una comparación de las señales válidas de los datos leídos. El DUT y el modelo de comportamiento deberían estar emitiendo datos simultáneamente, de lo contrario, algo anda mal.

Finalmente, verificamos que los datos de salida del DUT coincidan con el siguiente elemento que extraemos del FIFO del banco de pruebas. Esto, por supuesto, solo sucede si el rd_valid se afirma la señal, lo que significa que el rd_data la señal se puede muestrear.

Recopilación de datos de cobertura

Para controlar el flujo principal del banco de pruebas, crearemos un proceso secuenciador. Este proceso inicializará los contenedores de cobertura, ejecutará las pruebas y detendrá el banco de pruebas cuando se hayan cumplido todos los objetivos de cobertura. El siguiente código muestra el proceso «PROC_SEQUENCER» completo.

PROC_SEQUENCER : process
begin

  -- Set up coverage bins
  bin1.AddBins("Write while empty", ONE_BIN);
  bin2.AddBins("Read while full", ONE_BIN);
  bin3.AddBins("Read and write while almost empty", ONE_BIN);
  bin4.AddBins("Read and write while almost full", ONE_BIN);
  bin5.AddBins("Read without write when almost empty", ONE_BIN);
  bin6.AddBins("Write without read when almost full", ONE_BIN);

  wait until rising_edge(clk);
  wait until rising_edge(clk);
  rst <= '0';
  wait until rising_edge(clk);

  loop
    wait until rising_edge(clk);

    -- Collect coverage data
    bin1.ICover(to_integer(wr_en = '1' and empty = '1'));
    bin2.ICover(to_integer(rd_en = '1' and full = '1'));
    bin3.ICover(to_integer(rd_en = '1' and wr_en = '1' and
                           empty = '0' and empty_next = '1'));
    bin4.ICover(to_integer(rd_en = '1' and wr_en = '1' and
                           full = '0' and full_next = '1'));
    bin5.ICover(to_integer(rd_en = '1' and wr_en = '0' and
                           empty = '0' and empty_next = '1'));
    bin6.ICover(to_integer(rd_en = '0' and wr_en = '1' and
                           full = '0' and full_next = '1'));

    -- Stop the test when all coverage goals have been met
    exit when
      bin1.IsCovered and
      bin2.IsCovered and
      bin3.IsCovered and
      bin4.IsCovered and
      bin5.IsCovered and
      bin6.IsCovered;
  end loop;
  
  report("Coverage goals met");

  -- Make sure that the DUT is empty before terminating the test
  wr_en <= force '0';
  rd_en <= force '1';
  loop
    wait until rising_edge(clk);
    exit when empty = '1';
  end loop;

  -- Print coverage data
  bin1.WriteBin;
  bin2.WriteBin;
  bin3.WriteBin;
  bin4.WriteBin;
  bin5.WriteBin;
  bin6.WriteBin;
  
  finish;
end process;

Primero, inicializamos los objetos del contenedor de cobertura llamando al AddBins procedimiento sobre ellos, como ya hemos discutido anteriormente en este artículo. Luego, después de que se libera el reinicio, pasamos a recopilar datos de cobertura. En cada flanco ascendente del reloj, se ejecutará el código dentro de la construcción del bucle.

El primer bloque de código dentro del bucle es para recopilar datos de cobertura. Podemos llamar al ICover procedimiento en el bin para registrar un hit en el punto de cobertura que representa. Si proporcionamos el parámetro entero 0 , la llamada no tendrá efecto. Si usamos el parámetro entero 1 , contará como un hit.

Solo hay un "contenedor" dentro de cada uno de los objetos del contenedor de cobertura, porque los inicializamos usando el ONE_BIN constante. Se puede acceder a este contenedor único llamando al ICover(1) . Podemos registrar un acierto o error en el punto de cobertura convirtiendo nuestras expresiones booleanas a los números enteros 1 o 0 usando el to_integer función

Una vez registrados los datos de cobertura, verificamos si se cumplieron todos los objetivos de cobertura llamando al IsCovered función en todos los contenedores. Luego, salimos del ciclo si se cumplieron todos los objetivos de cobertura.

Nos aseguraremos de que el DUT esté vacío antes de finalizar la prueba. Para lograr esto, tomamos el control de los procesos de escritura y lectura forzando el wr_en señal a '0' y el rd_en señal a '1' .

Finalmente, imprimimos estadísticas de cuántas veces se ha alcanzado cada objetivo de cobertura llamando al WriteBin función en cada uno de los contenedores de cobertura. El finish La palabra clave al final del proceso hará que el simulador detenga la simulación.

Ejecutar el banco de pruebas

Puede descargar todo el proyecto ModelSim con todos los archivos VHDL mediante el siguiente formulario.

Después de haber cargado el proyecto ejecutando el archivo do que se incluye en el Zip, podemos ejecutar el banco de pruebas simplemente escribiendo «runtb» en la consola de ModelSim. El tiempo de ejecución del banco de pruebas será aleatorio porque los objetivos de cobertura se alcanzan al azar. Sin embargo, los resultados de la prueba son reproducibles porque en realidad se utiliza una secuencia pseudoaleatoria.

No inicializamos una semilla en nuestro código, lo que significa que el valor inicial predeterminado se usará para el generador pseudoaleatorio. Es posible configurar una semilla diferente llamando al InitSeed procedimiento en el RandomPType objeto, esto producirá una secuencia aleatoria diferente.

La salida de la consola

La salida impresa en la consola de ModelSim después de dar el comando «runtb» se muestra a continuación. Habrá muchos empujes aleatorios hacia y desde el FIFO del banco de pruebas mientras se ejecuta la simulación.

VSIM 2> runtb
# ** Warning: Design size of 15929 statements or 2 leaf instances exceeds
#             ModelSim PE Student Edition recommended capacity.
# Expect performance to be quite adversely affected.
# ** Note: Push 34910
#    Time: 790 ns  Iteration: 0  Instance: /ring_buffer_tb
...
# ** Note: Pop 37937
#    Time: 83100 ns  Iteration: 0  Instance: /ring_buffer_tb
# ** Note: Pop 13898
#    Time: 83110 ns  Iteration: 0  Instance: /ring_buffer_tb
# %% WriteBin: 
# %% Write while empty  Bin:(1)   Count = 2  AtLeast = 1
# 
# %% WriteBin: 
# %% Read while full  Bin:(1)   Count = 3  AtLeast = 1
# 
# %% WriteBin: 
# %% Read and write while almost empty  Bin:(1)   Count = 106  AtLeast = 1
# 
# %% WriteBin: 
# %% Read and write while almost full  Bin:(1)   Count = 1  AtLeast = 1
# 
# %% WriteBin: 
# %% Read without write when almost empty  Bin:(1)   Count = 1  AtLeast = 1
# 
# %% WriteBin: 
# %% Write without read when almost full  Bin:(1)   Count = 3  AtLeast = 1
#
# Break in Process PROC_SEQUENCER at C:/crv/ring_buffer_tb.vhd line 127

Las estadísticas de todos los contenedores de cobertura se imprimen cuando se han cumplido todos los objetivos de cobertura. Algunos de los contenedores han sido golpeados solo una vez, mientras que uno ha sido golpeado 106 veces. Pero al final, cada contenedor ha sido golpeado al menos una vez. Así, podemos saber que todos los eventos para los que hemos definido bins de cobertura han sido probados y verificados.

La forma de onda

Examinemos la forma de onda para tener una idea de lo que ha estado haciendo el banco de pruebas. La siguiente imagen muestra la forma de onda con el fill_count señal representada como un valor analógico. El FIFO está lleno cuando la traza de esta señal está en la parte superior y vacío cuando está en la parte inferior.

Como podemos ver en la forma de onda, el búfer circular se llena y se vacía al azar. Sin embargo, no programamos explícitamente estas subidas y bajadas en el nivel de llenado. Sin embargo, estamos viendo un patrón de interacción de aspecto orgánico con el DUT.

Más información sobre la verificación aleatoria restringida

La verificación aleatoria restringida es una buena estrategia de banco de pruebas cuando el vector de prueba tiene demasiadas permutaciones para que una prueba exhaustiva sea práctica. Las interacciones aleatorias exhiben un comportamiento más natural que el que hubiera tenido una prueba de caso de esquina dirigida, sin sacrificar la precisión.

Podemos estar seguros de que se han cumplido todos los casos de esquina, siempre que hayamos configurado correctamente la recopilación de datos de cobertura. El beneficio adicional es que es más probable que las pruebas aleatorias expongan debilidades en el DUT para las que no está probando específicamente. Siempre que conozca todos los casos de esquina, puede crear pruebas dirigidas para ellos. Pero los casos de esquina se pasan por alto fácilmente, y ahí es cuando podría beneficiarse de la metodología de verificación aleatoria restringida.

Este artículo solo ha arañado la superficie de lo que puede hacer con la verificación aleatoria restringida. Recomiendo leer los documentos en la página OSVVM GitHub para profundizar en el tema.

También recomiendo el curso Advanced VHDL Testbenches and Verification de SynthWorks, al que no estoy afiliado. Sin embargo, he asistido a la versión de 5 días de este curso físico. El curso es impartido por Jim Lewis, presidente del Grupo de Estandarización y Análisis de VHDL (VASG). En general, una gran inversión para cualquier empresa que quiera llevar sus bancos de pruebas VHDL al siguiente nivel.


VHDL

  1. La cadencia acelera la verificación de SoC de mil millones de puertas
  2. Siemens agrega a Veloce para una verificación asistida por hardware sin problemas
  3. El proyecto explora un diseño confiable y un flujo de verificación para la seguridad de IoT
  4. Synopsys habilita diseños de múltiples matrices con HBM3 IP y verificación
  5. Control de acceso con QR, RFID y verificación de temperatura
  6. El lado incómodo, impredecible y aleatorio del mantenimiento
  7. Cómo generar números aleatorios en Java
  8. Java 8 - Flujos
  9. Control de funciones de torno de bancada inclinada con gráficos de verificación
  10. Procesamiento isométrico diferencial y verificación de simulación del diseño de PCB de alta velocidad
  11. Programa de verificación de rendimiento de CAGI para compresores rotativos