Template-based circuit understanding

Adrià Gascón, Pramod Subramanyan, Bruno Dutertre, Ashish Tiwari, Dejan Jovanović, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

41 Scopus citations


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.

Original languageEnglish (US)
Title of host publication2014 Formal Methods in Computer-Aided Design, FMCAD 2014
EditorsKoen Claessen, Viktor Kuncak
PublisherInstitute of Electrical and Electronics Engineers Inc.
Number of pages8
ISBN (Electronic)9780983567844
StatePublished - Dec 16 2014
Event14th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2014 - Lausanne, Switzerland
Duration: Oct 21 2014Oct 24 2014

Publication series

Name2014 Formal Methods in Computer-Aided Design, FMCAD 2014


Other14th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2014

All Science Journal Classification (ASJC) codes

  • Computational Theory and Mathematics
  • Computer Graphics and Computer-Aided Design


Dive into the research topics of 'Template-based circuit understanding'. Together they form a unique fingerprint.

Cite this