|
Abstract:
|
O escopo tradicional da veri¯ca»c~ao funcional foi ampliado com o surgimento dos °uxos de projeto em n¶³vel de sistema eletr^onico (ESL). Nesses °u-xos, logo ap¶os o particionamento hardware-software, a veri¯ca»c~ao precisa lidar com tipos abstratos de dados, com artefatos de implementa»c~ao e com a poss¶³vel n~ao-preserva»c~ao, no dispositivo sob veri¯ca»c~ao (DUV), da ordem dos comportamentos no modelo de refer^encia (golden model ). As t¶ecnicas existentes para veri¯ca»c~ao p¶os-particionamento est~ao limitadas pelo uso de heur¶³sticas (que colocam em risco as garantias de veri¯ca»c~ao) ou por abordagens black-box (que restringem a observabilidade). Este trabalho adota uma abordagem white-box e prop~oe uma nova t¶ecnica que opera sobre amostras de dados capturadas por monitores e armazenadas na forma dos assim-chamados logs. Para cada ponto a ser veri¯cado, inserem-se monitores espelhados: um no modelo de refer^encia, outro no DUV. A veri¯ca»c~ao autom¶atica dos logs ¶e formulada com um problema de casamento (matching) em um grafo bipartido. O problema cl¶assico foi modi¯cado para capturar n~ao apenas a compatibilidade de valores monitorados, mas tamb¶em a preced^encia de eventos, de forma a viabilizar o tratamento da n~ao-preserva»c~ao da ordem no DUV. A formula»c~ao adotada permitiu provar v¶arias propriedades, as quais foram utilizadas como base te¶orica para determinar as garantias de veri¯ca»c~ao da t¶ecnica proposta. A implementa»c~ao dos monitores utilizou infra-estrutura pr¶e-existente baseada em re°ex~ao computacional. S~ao apresentados resultados experimentais que validam a formula»c~ao e os algoritmos propostos. The traditional scope of functional veri¯cation has been extended with the rise of electronic-system-level (ESL) design °ows. In those °ows, immediately after hardware-software partitioning, veri¯cation has to deal with abstract data, with implementation artifacts, and, possibly, with the non-preservation, by the device under veri¯cation (DUV), of the the order of behaviors at the golden model. Existing approaches are limited either by the use of greedy heuristics (jeopardizing veri¯cation guarantees) or by black-box approaches (impairing observability). This work adopts a white-box approach and proposes a new technique that operates on data samples captured by monitors and stored in the form of so-called logs. For each point to be veri¯ed, mirrored monitors are inserted: one at the golden model, another at the DUV. The automatic veri¯cation of the logs of a pair of mirrored monitors is cast as a bipartite graph matching problem. The classical problem was modi¯ed to capture not only value compatibility, but also event precedence, so as to allow the treatment of the non-preserved event order at the DUV. The adopted formulation allowed us to prove several properties, which were used as stepping stones for determining the veri¯cation guarantees of the proposed technique. The implementation of monitors relied on pre-existing infrastructure based upon computational re°ection. Experimental results validate the formulation and the proposed algorithms. |
