|
|
|---|
|
|
|
|---|
Summary of a system to specify the treatments of different primary outputs by AIG transformations
As an
This is fine when all we want to do with a transform is have it run fully automatically and e.g. preserve combinational equivalence among the outputs. But some transforms benefit from more user direction, and can be configured such that certain nodes are identified for certain purposes. For example, the FRAIG transform can find candidate equivalence classes, but it can benefit from a configuration which says that only certain nodes are to be treated as candidate equivalences. In a usage such as sv::svex-focused-equivalence-checking, these potentially equivalent nodes are known before any transforms are done, but other transforms may need to be run before the fraig transform. Therefore these candidate equivalence nodes are added as primary outputs (generally after the "real" primary outputs of the AIG). We then need to tell the FRAIG transform which outputs are regular primary outputs and which are the candidate equivalence classes. As this is just one example of the special purpose use of primary output nodes for a transform, there may be several different ranges of outputs that are to be used for different purposes across different transforms. We need a mapping, therefore, between ranges of outputs and their special purposes in various transforms.
To allow this sort of thing to work with minimal user hassle, we add one layer of indirection: we instead keep a mapping from output ranges to names (symbols), and separately in each transform's configuration, map names to objects describing their special purposes (which vary by transform).
Typically the