- Threshold logic collapse operation and verification within ABC
- Primary developer: Nian-Ze Lee from National Taiwan University
- C implementation of algorithms proposed in Analytic Approaches to the Collapse Operation and Equivalence Verification of Threshold Logic Circuits
- Algorithms and codes for threshold logic technology mapping proposed in Threshold Logic Synthesis Based on Cut Pruning by Augusto Neutzling et al.
- Reference: Nian-Ze Lee, Hao-Yuan Kuo, Yi-Hsiang Lai, Jie-Hong R. Jiang: Analytic approaches to the collapse operation and equivalence verification of threshold logic circuits. ICCAD 2016: 5
Type make
to complie and the executable file is bin/abc
make
The source code has been compiled successfully with GCC_VERSION=8.2.0 under CentOS 7.3.1611/Ubuntu 18.04 LTS
read_th
(aliasrt
): read a TL circuit (TLC) file in the.th
format (POs must be buffered)write_th
(aliaswt
): write the current TLC out in the.th
formatprint_th
(aliaspt
): print the network statistics of the current TLC
aig2th
(aliasa2t
): convert an AIG circuit to a TLC by replacing AIG nodes with TL gates (TLGs)merge_th
(aliasmt
): the proposed collapsing-based TLC synthesis
th2mux
(aliast2m
): convert a TLC to an AIG circuit by expanding a TLG to a MUX treethverify
(aliastvr
): write a CNF/PB file for the equivalence checking of two TLCsthpg
(aliastp
): write a PB file for the output satisfiability of a TLC with PG encoding
- Collapse an AIG circuit iteratively with a fanout bound = 100 (
aig_syn
is defined in file abc.rc)
abc 01> r exp_TCAD/collapse/benchmark/iscas_itc/s38417.blif
abc 02> aig_syn
abc 03> mt -B 100
abc 04> pt
abc 05> q
- Collapse a synthesized TLC iteratively with a fanout bound = 100 (
tl_syn
is defined in file abc.rc)
abc 01> r exp_TCAD/collapse/benchmark/iscas_itc/s38417.blif
abc 02> tl_syn
abc 03> wt s38417_before_clp.th
abc 04> mt -B 100
abc 05> pt
abc 06> wt s38417_after_clp.th
abc 07> q
- Verify equivalence using the TL-to-MUX translation and ABC command
cec
(continued from the above example)
abc 01> rt s38417_before_clp.th
abc 02> t2m
abc 03> w s38417_before_clp.aig
abc 04> rt s38417_after_clp.th
abc 05> t2m
abc 06> w s38417_after_clp.aig
abc 07> cec s38417_before_clp.aig s38417_after_clp.aig
abc 08> q
- Verify equivalence using the TL-to-PB translation and
minisat+
(continued from the above example)
abc 01> tvr s38417_before_clp.th s38417_after_clp.th
abc 02> q
$ bin/minisat+ compTH.opb
- Verify equivalence using the TL-to-CNF translation and
minisat
(continued from the above example)
abc 01> tvr -V 1 s38417_before_clp.th s38417_after_clp.th
abc 02> q
$ bin/minisat compTH.dimacs
- Check the output satisfiability of a TLC using the PB-based method with PG encoding (
pg_and
is defined in file abc.rc)
abc 01> r exp_TCAD/pg_encoding/benchmark/b14.blif
abc 02> pg_and
abc 03> q
$ bin/minisat+ no_pg.opb
$ bin/minisat+ pg.opb
Directory exp_TCAD
contains all benchmarks, scripts, log files, and data in the experiments. Specifically:
- Sub-directory
collapse
is for the collapsing-based synthesis experiments - Sub-directory
eqcheck
is for the verification experiments between TLCs before and after collapsing - Sub-directory
pg_encoding
is for the PG encoding experiments - Sub-directory
high_fanin
is for the translation scalability experiments - Sub-directory
dnn_mnist
is for the activation-binarized neural networks experiments
Please send an email to Nian-Ze Lee (nian-ze.lee@sosy.ifi.lmu.de) if there is any problem.