Using CAQE to synthesize Verilog code

expected_output.v

/* Generated by Yosys 0.7+528 (git sha1 3f007024, gcc 7.3.0 -fPIC -Os) */

(* top =  1  *)
module \7controller.aig (bit_control_0, bit_mode_0, bit_control_16, bit_control_15, bit_control_14, bit_control_13, bit_control_12, bit_control_11, bit_control_10, bit_control_9, bit_control_8, bit_control_7, bit_control_6, bit_control_5, bit_control_4, bit_control_3, bit_control_2, bit_control_1);
  output bit_control_0;
  output bit_control_1;
  output bit_control_10;
  output bit_control_11;
  output bit_control_12;
  output bit_control_13;
  output bit_control_14;
  output bit_control_15;
  output bit_control_16;
  output bit_control_2;
  output bit_control_3;
  output bit_control_4;
  output bit_control_5;
  output bit_control_6;
  output bit_control_7;
  output bit_control_8;
  output bit_control_9;
  input bit_mode_0;
  assign bit_control_1 = ~bit_mode_0;
  assign bit_control_0 = bit_mode_0;
  assign bit_control_10 = bit_control_1;
  assign bit_control_11 = 1'h1;
  assign bit_control_12 = 1'h0;
  assign bit_control_13 = bit_mode_0;
  assign bit_control_14 = 1'h0;
  assign bit_control_15 = bit_control_1;
  assign bit_control_16 = bit_mode_0;
  assign bit_control_2 = bit_control_1;
  assign bit_control_3 = bit_mode_0;
  assign bit_control_4 = bit_control_1;
  assign bit_control_5 = bit_mode_0;
  assign bit_control_6 = bit_mode_0;
  assign bit_control_7 = bit_control_1;
  assign bit_control_8 = bit_mode_0;
  assign bit_control_9 = 1'h1;
endmodule

gencontrol.sv

`define N 3

module top (
	input mode,
	input [`N:0] A,
	input [`N:0] B,
	input [16:0] control,

	output ok
);
	wire [`N:0] O1;
	wire [`N:0] O2;

	simple_alu    s_alu (mode,    A, B, O1);
	lut_based_alu l_alu (control, A, B, O2);

	assign ok = O1 == O2;
endmodule

module simple_alu(
	input mode,
	input [`N:0] A,
	input [`N:0] B,
	output [`N:0] O
);

	assign O = mode ? A+B : A-B;

endmodule

module lut_based_alu(
	input [16:0] lutdata,
	input [`N:0] A,
	input [`N:0] B,
	output [`N:0] O
);
	wire [`N:0] C;
	wire C__1 = lutdata[16];

	lut lo0(lutdata[ 7:0], {A[0], B[0], C__1}, O[0]);
	lut lc0(lutdata[15:8], {A[0], B[0], C__1}, C[0]);
	lut lo1(lutdata[ 7:0], {A[1], B[1], C[0]}, O[1]);
	lut lc1(lutdata[15:8], {A[1], B[1], C[0]}, C[1]);
	lut lo2(lutdata[ 7:0], {A[2], B[2], C[1]}, O[2]);
	lut lc2(lutdata[15:8], {A[2], B[2], C[1]}, C[2]);
	lut lo3(lutdata[ 7:0], {A[3], B[3], C[2]}, O[3]);
	lut lc3(lutdata[15:8], {A[3], B[3], C[2]}, C[3]);

endmodule

module lut(
	input [7:0] lutdata,
	input [2:0] I,
	output O
);
	assign O = lutdata[I];
endmodule

gencontrol.ys

read_verilog -sv gencontrol.sv
synth -flatten
abc -g AND
write_aiger -map 2out.aim -ascii 1out.aig

!../aiger/aigtocnf -m 1out.aig 3out.dimacs
!python script1.py
!../caqe-2/caqem -c 4out.qdimacs > 5controller.aig || true
!python script2.py
!../aiger/aigtoblif 7controller.aig > 8controller.blif

design -reset
read_blif 8controller.blif
synth -flatten
opt_clean -purge
write_verilog 9controller.v

script1.py

import scriptx

uncontrollable = ["mode"]
controllable   = ["control"]
unobservable   = ["A", "B"]

aim = scriptx.readaim("2out.aim")

forall1bits = []
existsbits = []
forall2bits = []

for ty, aignum, srcbit, srcname in aim:
	if ty == "input":
		if srcname in uncontrollable:
			forall1bits.append(aignum)
		elif srcname in controllable:
			existsbits.append(aignum)
		elif srcname in unobservable:
			forall2bits.append(aignum)
		else:
			assert False, ("unconsidered input", srcname)

dimacslines, i, mapping, dimnums = scriptx.readdimacs("3out.dimacs")
mapping = {k: v for k, v in mapping}

forall1dim = [mapping[n*2+2] for n in forall1bits if n*2+2 in mapping]
exists1dim = [mapping[n*2+2] for n in existsbits  if n*2+2 in mapping]
forall2dim = [mapping[n*2+2] for n in forall2bits if n*2+2 in mapping]
#with open("interfacewidth.txt", "w") as f: f.write("{} {}".format(len(forall1dim), len(exists1dim)))

exists2dim = list(dimnums - set(forall1dim) - set(forall2dim) - set(exists1dim))

quantifierlines = [
	"a {} 0".format(" ".join(str(n) for n in forall1dim)),
	"e {} 0".format(" ".join(str(n) for n in exists1dim)),
	"a {} 0".format(" ".join(str(n) for n in forall2dim)),
	"e {} 0".format(" ".join(str(n) for n in exists2dim))
]

qdimacs = "\n".join([dimacslines[i]] + quantifierlines + dimacslines[i+1:])

with open("4out.qdimacs", "w") as f: f.write(qdimacs)

script2.py

import scriptx

def parsequantifier(ql):
	p = ql.split(" ")
	assert p[0] in "ae"
	assert p[-1] == "0"
	return p[0], [int(n) for n in p[1:-1]]

def parsegate(gate):
	o, a, b = gate.split(" ")
	return int(o), int(a), int(b)

def parsegate2(gate):
	o, a, b = gate.split(" ")
	return int(o)//2, int(a)//2, int(b)//2

def mapint(ns): return [int(n) for n in ns]

def readquantifiers(fname):
	with open(fname) as f:
		qdimacslines = f.read().split("\n")[1:]
	for i, line in enumerate(qdimacslines):
		if line[0] not in "ae":
			break
	return [parsequantifier(ql) for ql in qdimacslines[:i]]

##

def edges_build(ln):
	edges = []
	for gate in ln:
		o, a, b = parsegate2(gate)
		if a!=0: edges.append([a, o])
		if b!=0: edges.append([b, o])
	return edges

def edges_into(fname, edgess):
	inputs = mapint(li)
	with open(fname, "w") as f:
		f.write("digraph {\n")

		attrs = {}

		for v in range(nm):
			v = v+1
			#attrs[v] = "[ fillcolor={}; style=filled; label=\"{}\" ];\n".format(["red", "orange", "green", "purple", "gray"][hqefi.get(v, -1)], v//2)
			attrs[v] = "[ label=\"{}\" ];\n".format(v//2)

		for i, (q, vs) in enumerate(quantifiers):
			f.write(" subgraph cluster_{}{} {{\n".format(q, i))
			for v in vs:
				v = qtm[v]//2
				f.write("  n{} {}".format(v, attrs[v]))
				del attrs[v]
			f.write(" }\n")

		for v, attr in attrs.items():
			f.write(" n{} {}".format(v, attr))

		#for num, l in hqefi.items():
		#	f.write("  n{} [ fillcolor={}; style=filled ];\n".format(num, ["red", "organe", "green", "purple", "gray"][l]))
		for color, edges in zip(["red", "blue"], edgess):
			for edge in edges:
				f.write(" n{} -> n{} [color={}];\n".format(edge[0], edge[1], color))
		f.write("}\n")

##

with open("5controller.aig") as f: lines = f.read()
lines = lines.split("\n")
aag, m, i, l, o, n = lines[0].split(" ")
nm = int(m)
ni = int(i)
nl = int(l)
no = int(o)
nn = int(n)

li = lines[1:1+ni]
ll = lines[1+ni:1+ni+nl]
lo = lines[1+ni+nl:1+ni+nl+no]
ln = lines[1+ni+nl+no:1+ni+nl+no+nn]
ci = lines[1+ni+nl+no+nn:1+ni+nl+no+nn+ni]
co = lines[1+ni+nl+no+nn+ni:1+ni+nl+no+nn+ni+no]
zz = lines[1+ni+nl+no+nn+ni+no:]

ili = mapint(li)
ill = mapint(ll)
ilo = mapint(lo)

assert zz[0] == "c"
assert zz[1] in ("SAT", "UNSAT")
assert (lo[-1], zz[1]) in (("1", "SAT"), ("0", "UNSAT")), (lo[-1], zz[1])

qtm = {}
for cil in ci:
	a, b = cil.split(" ")
	qtm[int(b)] = int(li[int(a[1:])])
for col in co[:-1]:
	a, b = col.split(" ")
	qtm[int(b)] = int(lo[int(a[1:])])

qti = [int(l.split(" ")[1]) for l in ci]
qto = [int(l.split(" ")[1]) for l in co[:-1]]

##

quantifiers = readquantifiers("4out.qdimacs")

assert quantifiers[0][0] == "a"
assert quantifiers[1][0] == "e"
assert quantifiers[2][0] == "a"
assert quantifiers[3][0] == "e"

##

def readmappings():
	_, _, dimmapping, _ = scriptx.readdimacs("3out.dimacs")
	dimmapping = {v: k for k, v in dimmapping}

	aimmapping = {}
	aim = scriptx.readaim("2out.aim")
	for ty, aignum, srcbit, srcname in aim:
		aimmapping[ty, aignum] = (srcname, srcbit)

	aigputmapping = {}
	with open("1out.aig") as f:
		sub_lines = f.read()
	sub_lines = sub_lines.split("\n")
	_, _, sub_i, sub_l, sub_o, _ = sub_lines[0].split(" ")
	sub_ni = int(sub_i)
	sub_nl = int(sub_l)
	sub_no = int(sub_o)
	assert sub_nl == 0
	sub_li = sub_lines[1:1+sub_ni]
	sub_lo = sub_lines[1+sub_ni:1+sub_ni+sub_no]
	for i, n in enumerate(mapint(sub_li)):
		assert (n&1) == 0
		aigputmapping[n] = ("input", i)
	for i, n in enumerate(mapint(sub_lo)):
		aigputmapping[n] = ("output", i)

	def dimnumtoname(dimnum):
		if dimnum not in dimmapping:
			return (0, "const0", 0)
		aig1num = dimmapping[dimnum]
		if aig1num in aigputmapping: 
			inv, aig1putnum = 0, aigputmapping[aig1num]
		else:
			inv, aig1putnum = 1, aigputmapping[aig1num^1]
		#print(aig2num, dimnum, aig1num, aig1putnum)
		srcname, srcbit = aimmapping[aig1putnum]
		return inv, srcname, srcbit

	return dimmapping, aigputmapping, aimmapping, dimnumtoname

##

if zz[1] == "SAT":

	mi = [q in quantifiers[0][1] for q in qti]
	mo = [q in quantifiers[1][1] for q in qto]

	dead = [n for n, m in zip(ili, mi) if not m]
	ili  = [n for n, m in zip(ili, mi) if     m]
	ilo  = [n for n, m in zip(ilo, mo) if     m]
	ci   = [c for c, m in zip( ci, mi) if     m]
	co   = [c for c, m in zip( co, mo) if     m]

	quant_index = {"a": {}, "e": {}}
	for i, (q, vs) in enumerate(quantifiers):
		n = quant_index[q]
		for v in vs:
			v = qtm[v]//2
			if v in n:
				assert q == "e" # every forall quantified var should be unique, and not be in 'n' already
				n[v] = max(n[v], i)
			else:
				n[v] = i

	cache = {}
	remap = {}
	optd = set()
	dead = {int(n)//2 for n in dead}
	deadpath = {origin: [] for origin in dead}

	ln2 = []
	for gate in ln:
		# caqe generates extremely redundant gates
		# deduplicating using 'cache' and 'remap'
		o, a, b = parsegate(gate)

		if o//2 in dead:
			continue

		if a//2 in dead or b//2 in dead:
			if a//2 in dead:
				deadpath[o//2] = [a] + deadpath[a//2]
			else:
				deadpath[o//2] = [b] + deadpath[b//2]
			dead.add(o//2)
			continue

		a = remap.get(a//2, a&~1) ^ (a&1)
		b = remap.get(b//2, b&~1) ^ (b&1)
		if (a, b) in cache:
			remap[o//2] = cache[a, b]
		else:
			cache[a, b] = o
			ln2.append("{} {} {}".format(o, a, b))
			optd.add(o)

	for o in ilo:
		if o//2 in dead:
			print("desired output", o, "was removed because it is affected by removed input", deadpath[o//2][-1], "through", deadpath[o//2])
		if o&~1 not in optd:
			if o//2 in remap:
				ln2.append("{} {} {}".format(o, remap[o//2], 1))
			else:
				pass # can only hope that o is an input bit

	li = list(map(str, ili))
	lo = list(map(str, ilo))
	ln = ln2

	if False:
		# fix up comment lines
		ci = ["i{} {}".format(i, c.split(" ")[1]) for i, c in enumerate(ci)]
		co = ["o{} {}".format(i, c.split(" ")[1]) for i, c in enumerate(co)]
	else:
		# enhance comment lines
		dimmapping, aigputmapping, aimmapping, dimnumtoname = readmappings()

		def h(c):
			inv, n, b = dimnumtoname(int(c.split(" ")[1]))
			if inv: return "not_{}_{}".format(n, b)
			else:   return "bit_{}_{}".format(n, b)

		ci = ["i{} {}".format(i, h(c)) for i, c in enumerate(ci)]
		co = ["o{} {}".format(i, h(c)) for i, c in enumerate(co)]


	newheader = "{} {} {} {} {} {}".format(aag, nm, len(li), nl, len(lo), len(ln))
	lines = [newheader] + li + ll + lo + ln + ci + co + zz

	#edges_into("6controller.dot", [edges_build(ln)])
	with open("7controller.aig", "w") as f: f.write("\n".join(lines))

else:

	numforall = sum(len(indices) for kind, indices in quantifiers if kind == "a")
	numexists = sum(len(indices) for kind, indices in quantifiers if kind == "e")

	import sys, subprocess
	cmd = ["../aiger/aigsim", "-r", "1", "5controller.aig"]
	print(" ".join(cmd))
	aigsimlines = subprocess.check_output(cmd).split(b"\n")
	pairs = [line.split(b" ")[1:3] for line in aigsimlines if line and line[0] == 32]

	dimmapping, aigputmapping, aimmapping, dimnumtoname = readmappings()

	for inp, outp in pairs:
		for aig2num, col in enumerate(co[:-1]):
			a, b = col.split(" ")
			assert aig2num == int(a[1:])
			dimnum = int(b)
			inv, srcname, srcbit = dimnumtoname(dimnum)
			print("{}[{}]".format(srcname, srcbit), "=", inv^int(chr(outp[aig2num])))

	sys.exit(1)

scriptx.py

def readdimacs(fname):
	with open("3out.dimacs") as f: dimacs = f.read()
	dimacslines = dimacs.split("\n")
	mapping = []
	dimnums = set()
	for i, line in enumerate(dimacslines):
		if line[0] == "p": break
		c, aignum, arrow, dimnum = line.split(" ")
		aignum = int(aignum)
		dimnum = int(dimnum)
		mapping.append((aignum, dimnum))
		dimnums.add(dimnum)
	return dimacslines, i, mapping, dimnums

def readaim(fname):
	with open(fname) as f: amap = f.read()
	m = []
	for line in amap.split("\n"):
		if not line.strip(): continue
		ty, aignum, srcbit, srcname = line.split(" ")
		aignum = int(aignum)
		srcbit = int(srcbit)
		m.append([ty, aignum, srcbit, srcname])
	return m