Demo - NTU-ALComLab/LSV-PA GitHub Wiki

Outline

In this demo, we will show:

  • how to read a circuit by command read
  • print its statistics by command print_stats
  • visualize the circuit by command show
  • transform the circuit into an and-inverter graph (AIG) by command strash
  • simplify the AIG by command fraig
  • check the equivalence of two circuits by command cec

Note: Use -h option to see the usage of a command. For example:

abc 01> cec -h
usage: cec [-T num] [-C num] [-I num] [-P num] [-psnvh] <file1> <file2>
	         performs combinational equivalence checking
	-T num : approximate runtime limit in seconds [default = 20]
	-C num : limit on the number of conflicts [default = 10000]
	-I num : limit on the number of clause inspections [default = 0]
	-P num : partition size for multi-output networks [default = unused]
	-p     : toggle automatic partitioning [default = no]
	-s     : toggle "SAT only" and "FRAIG + SAT" [default = FRAIG + SAT]
	-n     : toggle how CIs/COs are matched (by name or by order) [default = by name]
	-v     : toggle verbose output [default = no]
	-h     : print the command usage
	file1  : (optional) the file with the first network
	file2  : (optional) the file with the second network
	         if no files are given, uses the current network and its spec
	         if one file is given, uses the current network and the file

Demonstration

Consider an one-bit full adder in the blif format:

.model full_adder
.inputs a b c-in
.outputs sum c-out
.names a b c-in sum #sum=XOR(a,b,c-in)
100 1
010 1
001 1
111 1
.names a b c-in c-out #c-out=MAJ(a,b,c-in)
11- 1
1-1 1
-11 1
.end

We can read the circuit into ABC and print its basic statistics:

abc 01> read lsv/example/full_adder.blif 
abc 02> print_stats
full_adder                    : i/o =    3/    2  lat =    0  nd =     2  edge =      6  cube =     7  lev = 1

We can also visualize the circuit by command show (packages graphviz and gv required):

full adder

We can strash the full adder into an and-inverter graph (AIG), and simplify it by fraig:

abc 01> read lsv/example/full_adder.blif 
abc 02> strash
abc 03> print_stats
full_adder                    : i/o =    3/    2  lat =    0  and =     11  lev =  4
abc 03> fraig
abc 04> print_stats
full_adder                    : i/o =    3/    2  lat =    0  and =      8  lev =  4

Observe that the number of AND gates is reduced by 3.

The AIG after strash:

strash

The simplified AIG after fraig:

fraig

We could check the equivalence between the simplified full adder and the original one by command cec:

abc 01> read archive/example/full_adder.blif 
abc 02> strash
abc 03> print_stats
full_adder                    : i/o =    3/    2  lat =    0  and =     11  lev =  4
abc 03> fraig
abc 04> print_stats
full_adder                    : i/o =    3/    2  lat =    0  and =      8  lev =  4
abc 04> cec archive/example/full_adder.blif 
Networks are equivalent.  Time =     0.02 sec
⚠️ **GitHub.com Fallback** ⚠️