Harmonic estende o Aristotle à verificação formal de software e hardware
A Harmonic estendeu o Aristotle à verificação formal de software em C e de hardware em Verilog, com provas matemáticas de que propriedades especificadas valem para todas as entradas possíveis de um sistema definido.
||
27/10 às 13:41, atualizado 14:10
Pontos principais
- A Harmonic afirma que, em C, o Aristotle verifica software contra requisitos especificados, incluindo corretude funcional e a ausência de certas classes de comportamento indefinido.
- Em Verilog, a Harmonic afirma que o Aristotle faz verificação lógica total de propriedades de caminho de controle, como liveness e safety, e de propriedades matemáticas de caminho de dados.
- Segundo a empresa, o Aristotle propõe propriedades a partir do código e informa quais provou, quais não provou e as premissas de cada prova.
- A Harmonic descreve um fluxo em que engenheiros revisam essas propriedades, as incluem no repositório e rodam o Aristotle em CI a cada commit, para que o que foi provado continue provado.
- A Harmonic informa que o Aristotle está disponível desde hoje, com preço por consumo no modo self-serve; os planos enterprise têm preço por volume, suporte dedicado e implantação on-prem ou em private cloud.
- A Harmonic não divulga métricas de desempenho nem clientes nomeados.
A Harmonic anunciou que o Aristotle, usado até então em matemática de pesquisa, passa a fazer verificação formal de software e hardware, começando por código em C e designs em Verilog. Segundo a empresa, o código gerado por IA já é escrito mais rápido do que as equipes conseguem revisar, e revisão e testes examinam só parte dos comportamentos possíveis. A verificação formal, ao contrário, prova se as propriedades especificadas valem para todas as entradas possíveis de um sistema definido.
