Template-based circuit understanding
Contribuinte(s) |
Claessen, Koen Kuncak, Viktor |
---|---|
Data(s) |
2014
|
Resumo |
When verifying or reverse-engineering digital circuits, one often wants to identify and understand small components in a larger system. A possible approach is to show that the sub-circuit under investigation is functionally equivalent to a reference implementation. In many cases, this task is difficult as one may not have full information about the mapping between input and output of the two circuits, or because the equivalence depends on settings of control inputs. We propose a template-based approach that automates this process. It extracts a functional description for a low-level combinational circuit by showing it to be equivalent to a reference implementation, while synthesizing an appropriate mapping of input and output signals and setting of control signals. The method relies on solving an exists/forall problem using an SMT solver, and on a pruning technique based on signature computation. |
Formato |
application/pdf |
Identificador | |
Publicador |
FMCAD Inc |
Relação |
http://eprints.qut.edu.au/83100/1/__staffhome.qut.edu.au_staffgroupm%24_meaton_Desktop_Published%20paper_Jovanovic.pdf http://csl.sri.com/users/dejan/papers/gascon-fmcad2014.pdf Gascón, Adrià, Subramanyan, Pramod, Dutertre, Bruno, Tiwari, Ashish, Jovanović, Dejan, & Malik, Sharad (2014) Template-based circuit understanding. In Claessen, Koen & Kuncak, Viktor (Eds.) Proceedings of the 14th Conference on Formal Methods in Computer-Aided Design (FMCAD '14), FMCAD Inc, Lausanne, Switzerland, pp. 83-90. |
Direitos |
Copyright 2014 owned jointly by the authors and FMCAD Inc. |
Fonte |
School of Electrical Engineering & Computer Science; Science & Engineering Faculty |
Tipo |
Conference Paper |