Skip to content

Latest commit

 

History

History
88 lines (76 loc) · 4.93 KB

DATASETS.md

File metadata and controls

88 lines (76 loc) · 4.93 KB

Dataset setup

NOTE: Will update this document soon.

Random circuits

We generate large synthetic combinatorial circuits using BONY. We did slightly modification to the code and hold the code in Ironprop-Stone/Bony.

Prepare the raw benchmarks

  • Generate the raw data by yourself
  • Setup from the generated dataset
    • The data directory structure is shown as follows. 
      ${deepgate}/data_raw/random_circuits
└── bench
│   ├── 600.bench
│   ├── 601.bench
│   ├── ...
├── circuit_figs
│   ├── 600_0.png
│   ├── 601_0.png
│   └── ...
├── labels
│   ├── 600_0.txt
│   ├── 601_0.txt
│   └── ...
├── sub_circuits
│   ├── 600_0.txt
│   ├── 601_0.txt
│   └── ...
    • The bench contains the raw benchmark files generated by Bony. The circuit_figs constains the C1 predictions vs. simulated probability. The labels constains the simulated probability labels for every circuit. The sub_circuits contains the extracted sub-circuits from bench.
    • We only need the bench for the data generation.
    cd data/random_circuits
python prepare_random_circuits.py
cd ../..

After this step, you should end up with two files in the data\random_circuits directory: random_circuits_graphs.npz for the circuit graphs, and random_circuits_labels.npz for the semi ground-truth probability labels, which will look like

${PoseAug}
├── data/random_circuits
│  ├── random_circuits_graphs.npz
│  ├── random_circuits_labels.npz

Benchmarks

  1. ISCAS'85
  2. ITC'99
  3. EPFL

Random satisfiability problems (SAT)

Here are 3 methods to generate the dataset for SAT problem.

Random SAT dataset

The source of SAT problems all follows the generation algorithm described in NeuroSAT. Here, we have different way to pre-process the generated SAT problems:

  1. CNF format. The raw format from SAT generator.
  2. Conventional Circuit format (AND, OR, NOT). Three types of gates are considered here. The expansion from CNF to conventional circuits follows the procedure in CircuitSAT.
  3. AIG format (AND, NOT).

The details of AIG conversion is shown as follow:

Libraries

The libraries we need:

  1. abc: System for sequential logic system and formal verification;
  2. AIGER: A format, library and sets of utilities for And-Inverter Graphs (AIGs);
  3. CNFtoAIG: A converter extracts an AIG in AIGER format from a CNF in DIMACS format;
  4. PyMiniSolvers: a Python API for the MiniSat and MiniCard constraint solvers.

Workflow

  • Step1: PyMiniSovlers to generate SAT and UNSAT pairs in dimacs format, which representing the propositional equations as CNF;
  • Step2: CNFtoAIG to convert the CNF circuits into AIG circuits;
  • Step3: ABC to optimize AIG and output optimized AIG, which is usually be done for synthesis. The optimization process follows the demo example: 1, (Balancing) balance; 2, (Synthesis) balance; rewrite -l; rewrite -lz; balance; rewrite -lz; balance; 3, (Verification) ces; 4, Save AIG write *.aig. I assume the networks before and after synthesis are equivalent.
  • Step4: aigtoaig (utilities in AIGER) to convert binary AIGER format (*.aig) into ASCII AIGER (*.aag) format.
  • Step5: Parse and construct graphs in PyGeometric format with generated AIG circuits.

CNF synthesized dataset

  1. The generation of random CNF formula follows the procedure described in NeuroSAT. The outputs are a few pairs of SAT and UNSAT CNFs. In each pair, SAT and UNSAT CNFs only have difference on the final clauses.
  2. Convert the CNF formula to flat circuit in verilog format. The depth of circuit is only 3 (literal -> clause -> primary output).
  3. Use Yosys synthesis the flat circuits.
  4. Convert the post-synthesize circuit to bench format.

Extract SAT and UNSAT subcircuits

  1. Generate the random non-CNF circuits with specific parameters.
  2. Maintain the fan-in list and verify satisfiability of each gate in circuits.
  3. Extract the SAT and UNSAT gates as subcircuits, the primary inputs of the subcircuit are the original PIs in fan-in list, the only primary output is the corresponding SAT or UNSAT gate.