-
Notifications
You must be signed in to change notification settings - Fork 30
RE Literature Survey
Formal Methods for Reverse Engineering Gate Level Netlists - Wenchao LI
Presents close to a complete flow (assuming you start from a gate-level netlist, so no frontend stuff). My takeaways that didn't sound like anything I'd heard in the channel:
- Solve max. common subgraph problem by solving max. clique problem (see reference 8)
- QPF > SAT for model checking because it can deal with "side signals" better
- Signature analysis based on simulation can provide input/output correspondence
FROSTY: A Fast Hierarchy Extractor for Industrial CMOS Circuits - Lei Yang and C.J Richard Shi
This paper begins with a transistor-level netlist, first extracts gates, then extracts "pseudo-gates" (flip flops, latches, anything not static CMOS) and user-defined blocks. The block extraction is done using directed graph traversal and what they call "node properties" - the algorithm is "gradual matching".
Verification of Gate-level Arithmetic Circuits by Function Extraction
An interesting approach to verification of arithmetic/combinatorial circuits. Obviously intended for verification, but potentially useful for extraction as well. Claims to be very fast.
Simulation Graphs for Reverse Engineering
The key idea of this paper is using simulation graphs to identify candidate subgraphs for extraction. Basically the full SAT-based equivalence checking is not performed, instead the graph is transformed into a simulation graph which is much smaller and easier to run subgraph isomorphism testing on. Then once candidates are identified the full checking is run.
A very recent paper from the family of "simplify the isomorphism problem by finding candidate higher level structures and matching on those" algorithms, this graph uses a heuristic which basically says "assume that highly-connected regions are functional blocks" (or, looked at inversely, "choose your functional blocks so that a minimum number of connections between them are required). There's also a genetic algorithm component to attempt to bootstrap further and further up the functional hierarchy.
Very relevant paper. Describes a set of three tools designed to do essentially what you're talking about doing. Also describes a nice GUI used for manual supervision of the process. The three tools are described below.
RELIC: identifies control registers by identifying datapath registers. Datapath registers are assumed to be highly similar while control registers tend to be more unique. Thus RELIC computes a kind of "how similar is this wire to other wires" score which enables it to classify a wire as datapath or control.
REBUS: Uses the same technique along with forward propagation to identify datapaths.
REFSM: Uses the control registers extracted by RELIC to recover the high-level chip FSM using a breadth-first search. Then uses a tensor product decomposition technique to extract FSMs for submodules from the higher-level FSM.
Reverse Engineering Digital Circuits Using Functional Analysis
This is also a pretty complete automated flow which seems to produce good results. The algorithm for this paper goes like this:
a) Cut-based Boolean matching used to find replicated "bitslices" (1 output, small number of inputs). "Find some circuits that appear a lot in the netlist". b) Topological analysis to group bitslices into multi-bit components (adders, multiplexers, etc). "Find some places where several bitslices are used in the same way". c) Propagate these words to find other circuits. d) Boolean matching for larger submodules e) Topological analysis and SAT checking to look for counters and shift registers 7) Find register files and RAM arrays with BDD-based functional analysis.
A highly efficient method for extracting FSMs from flattened gate-level netlist
Detailed algorithm(s) for extracting FSMs. Finds potential state registers (basically registers that feed back to themselves), downselects them, finds register groups based on enable signals, groups state registers according to those groups, identifies the combinatorial circuits in the feedback paths, then partition state registers based on how strongly connected they are.