Fraig-config
Configuration object for the fraig aignet transform.
This is a product type introduced by fty::defprod.
Fields
- initial-sim-words — posp
- Number of 32-bit simulation words per node for initial simulation
- initial-sim-rounds — posp
- Number of times to simulate initially
- sim-words — posp
- Number of 32-bit simulation words per node for simulation during fraiging
- ipasir-limit — ACL2::maybe-natp
- Ipasir effort limit
- ipasir-recycle-count — ACL2::maybe-natp
- Number of callbacks after which to recycle the solver
- ctrex-queue-limit — ACL2::maybe-natp
- Limit to number of counterexamples that may be queued before resimulation
- ctrex-force-resim — booleanp
- Force resimulation of a counterexample before checking another node in the same equivalence class
- random-seed-name — symbolp
- Name to use for seed-random, or NIL to not reseed the random number generator
- outs-only — booleanp
- Only check the combinational outputs of the network
- miters-only — booleanp
- Instead of starting with all nodes in a single equivalence
class and refining them with random simulation, start with equivalence classes
consisting of the mitered outputs of the network. That is, whenever an output contains
an XOR under a top-level conjunction, put the inputs of that XOR into an
equivalence class. This is useful for checking equivalences when you know
exactly which nodes in a network are supposed to be equivalent, because it
avoids checking false equivalences.
- delete-class-on-fail — natp
- If set greater than 0, then if a SAT check fails, don't try to prove any
of the other equivalences in that node's equiv class (delete the class), unless
it was the constant class. If set greater than 1, delete the class even if
it's the constant class (drastic!).
- gatesimp — gatesimp
- Gate simplification parameters. Warning: This transform will do
nothing good if hashing is turned off.
- level-limit — natp
- If set greater than 0, we'll only try to check the current
node's candidatae equivalence if its level (see aignet-record-levels) is
less than or equal to the level limit.
- n-outputs-are-initial-equiv-classes — ACL2::maybe-natp
- If set to a natural number N, then the initial equiv classes will be built
by joining pairs of outputs (i, i+N). The range of i depends on the
setting of initial-equiv-classes-last. If nonnil, then i ranges from
numOuts-2N to numOuts-N-1; if nil, then it ranges from 0 to
N-1. Larger equivalence classes may be built by pairing the same node
more than once. Combinational equivalence is preserved for all outputs. Not
compatible with :miters-only.
- initial-equiv-classes-last — booleanp
- See the n-outputs-are-initial-equiv-classes option.
Subtopics
- Make-fraig-config
- Basic constructor macro for fraig-config structures.
- Fraig-config-fix
- Fixing function for fraig-config structures.
- Fraig-config-p
- Recognizer for fraig-config structures.
- Fraig-config->n-outputs-are-initial-equiv-classes
- Get the n-outputs-are-initial-equiv-classes field from a fraig-config.
- Fraig-config-equiv
- Basic equivalence relation for fraig-config structures.
- Change-fraig-config
- Modifying constructor for fraig-config structures.
- Fraig-config->initial-equiv-classes-last
- Get the initial-equiv-classes-last field from a fraig-config.
- Fraig-config->ipasir-recycle-count
- Get the ipasir-recycle-count field from a fraig-config.
- Fraig-config->delete-class-on-fail
- Get the delete-class-on-fail field from a fraig-config.
- Fraig-config->ctrex-queue-limit
- Get the ctrex-queue-limit field from a fraig-config.
- Fraig-config->random-seed-name
- Get the random-seed-name field from a fraig-config.
- Fraig-config->initial-sim-words
- Get the initial-sim-words field from a fraig-config.
- Fraig-config->initial-sim-rounds
- Get the initial-sim-rounds field from a fraig-config.
- Fraig-config->ctrex-force-resim
- Get the ctrex-force-resim field from a fraig-config.
- Fraig-config->miters-only
- Get the miters-only field from a fraig-config.
- Fraig-config->level-limit
- Get the level-limit field from a fraig-config.
- Fraig-config->ipasir-limit
- Get the ipasir-limit field from a fraig-config.
- Fraig-config->sim-words
- Get the sim-words field from a fraig-config.
- Fraig-config->outs-only
- Get the outs-only field from a fraig-config.
- Fraig-config->gatesimp
- Get the gatesimp field from a fraig-config.