Use Z3 for solving placement constraints and layout optimization

[dvc94ch]

• [ ] Export placement constraints into an optimization problem in Z3's smt-lib format

[kasbah]

Could you go into a bit more detail of how this could work? Maybe a link to a research paper? I can sort of imagine it but it would be interesting read if someone has already done work like this.

I played a bit (mainly just thought about) using Z3 for code synthesis when I was working on an experimental footprint editor but I didn't fully realize that constraint programming could be used for layout tasks.

I found this paper (and Python implementations: 1 and 2) where they use an SMT solver for escape routing which is a bit different but also interesting.

[dvc94ch]

I looked was reading parts of Placement and Design Planning for 3D Integrated Circuits. Most literature seems to be focused on IC placement, I don't remember finding any which proposed using an SMT solver. This issue is more of a "explore idea further issue".

MonoSAT looks interesting, thanks for the link. I'd like to revive this project sometime. It's not very useful at the moment, since the graphviz export for example becomes a mess real quick. I was working on some improvements to that a while ago but development stalled...

My current area of interest are low cost inkjet printers for rapid electronics prototyping.

[kasbah]

It's an interesting topic that I'd like to explore more at some point. Thanks for the link.

Regarding the Graphviz output, I added some to SkiDL but it's just the most basic thing that wouldn't help much for complex circuits. Though for SkiDL I think if you treat sub-circuits as nodes as well, and can choose a "zoom level" it could actually become useful for more complex circuits as well.

Any links to read about your current projects?

[dvc94ch]

Yes, that was the approach I was taking too.

Recently I've been playing around with rust on the hifive board: https://github.com/dvc94ch/riscv-rust-toolchain Other than that I've not had too much time...

On the topic of inkjet printing I've mainly been reviewing literature, maybe find a project I could use as a bachelor thesis next year.

https://kitspace.org looks really nice, could be a nice source of real world placement/routing problems.

[kasbah]

Ah cool, sounds like fun. I dabbled in Rust a bit and Hifive is really cool. Does it have decent support for peripherals: ADC, SPI etc?

Thanks! Kitspace is where I spend most of my free time. I am trying to figure out how to get more people to put their projects up. Not needing to use Git/Github will be big when I get it done but other than that I am not sure. I am hoping the BOM tools I am developing will prove valuable enough to attract people.

Regarding real world placement/routing problems GitHub might be a better bet for now. I put this in a presentation recently; approximate data from a basic survey I repeated twice:

Open hardware is growing! Feb 2017:

• ~3000 KiCad projects on GitHub
• ~7000 Eagle projects on GitHub
• ~9000 shared projects on OshPark

Oct 2017:

• ~5500 KiCad projects on GitHub
• ~12000 Eagle projects on GitHub
• ~13000 shared projects on OshPark

By comparison we currently have 32 projects on Kitspace :)

[dvc94ch]

The hifive board doesn't have an ADC (or I2C, DMA), Watchdog and SPI support is still missing.

I'd put my projects up, but still have very limited design experience... Getting user attention is always the hard part, I'm sure there are many awesome dead projects on the internet. Have you tried writing guest blog posts for OSH, hackaday, EEVBlog etc..?

[kasbah]

I say, go for it! Even if it's just a really simple project. I wrote a post for Octopart a while back but not for the ones you mentioned. It's a good idea.

[dvc94ch]

Your (escape routing) paper revived my interest in the subject. I've found some time to continue researching SAT and it's applications.

The new experiment would be:

1. read a kicad netlist
2. annotate any information required (see [0])
3. generate constraints in a language like minizinc [1]
4. compile to flatzinc and translate to dimacs cnf with fzntini[3]
5. dimacs cnf + netlist graph information -> dimacs gnf
6. solve with monosat
7. translate result to kicad pcb
8. view result, update constraints cycle
9. postprocess with pykicad (add copper pours etc.)

First step would be to play with minizinc and monosat, solving standard problems like n-queens, sudoku, etc. and then moving on to graph problems.

EDIT: Another idea to reduce problem size is to use the sat solver for computing a rubber band sketch, instead of using a grid.

[0] Optimization of electronics component placement design on PCB using self organizing genetic algorithm (SOGA) [1] minizinc [2] overview sat/smt/cp/asp [3] fzntini

[kasbah]

Very interesting! Might be a good idea to optimize for minimal trace length (or area of PCB?) to start off with (rather than "temperature of components, area of PCB, high power component placement and high potential critical components distance" as they do in the linked paper).

What do you mean by "rubber band sketch"?

[dvc94ch]

Routing is expressed as a topological problem, which uses less nodes in a graph (n = number of pads) than a grid representation (n = x y z). It is then converted into an extended rubber band sketch and finally into a geometric routing.

[0] Introduction: SURF: Rubber-band Routing System for Multichip Modules [1] Topological routing: RUBBER-BAND BASED TOPOLOGICAL ROUTER [2] Spoke insertion: Fast and Incremental Routability Check of A Topological Routing Using a Cut-based Encoding [3] Geometric routing: Geometric Transformations for a Rubber-band Sketch

[dvc94ch]

So Z3 isn't going to be a magic bullet. Instead of using Z3 to optimize an objective function (optimization only works for linear cost functions, minimizing area is nonlinear)

The thing that can work is adding constraints until the solution that is found is good enough, and use Z3 to simply find a solution instead of the optimal solution.

The constraints I added for the simple example where an area constraint, and positioning the mcu at the center.

# Project constraints:
# Minimize manually
s.add(area < 120)
s.add(boxes[0].x == pcb[0] / 2)
s.add(boxes[0].y == pcb[1] / 2)

Here's a prototype for placing a simple circuit:

from z3 import *
import math

class Box(object):
    counter = 0

    def __init__(self, width, height):
        self.id = str(Box.counter)
        Box.counter += 1

        self.x = Int('x%s' % self.id)
        self.y = Int('y%s' % self.id)
        self.width = int(math.ceil(width))
        self.height = int(math.ceil(height))
        self.rx = int(math.ceil(width / 2))
        self.ry = int(math.ceil(height / 2))

    def overlap(self, other):
        c1 = self.x - other.x >= self.rx + other.rx
        c2 = other.x - self.x >= self.rx + other.rx
        c3 = self.y - other.y >= self.ry + other.ry
        c4 = other.y - self.y >= self.ry + other.ry
        return Or(c1, c2, c3, c4)

    def __str__(self):
        return "w=%s h=%s rx=%s ry=%s" % (self.width, self.height,
                                          self.rx, self.ry)

    def eval(self, model):
        return "x=%s y=%s %s" % (model[self.x], model[self.y], str(self))

# Input
packages = [
    # count, width, height
    (1, 5, 5), # 5.3, 5.3
    (8, 4, 2),
]

s = Solver()
#s = Optimize()

pcb = (Int('pcb_x'), Int('pcb_y'))
area = Int('area')
boxes = []

s.add(pcb[0] >= 0)
s.add(pcb[1] >= 0)
s.add(area == pcb[0] * pcb[1])

for i, p in enumerate(packages):
    for j in range(p[0]):
        box = Box(p[1], p[2])
        # Constrain position to be on the pcb
        s.add(box.x >= box.rx)
        s.add(box.x <= pcb[0] - box.rx)
        s.add(box.y >= box.ry)
        s.add(box.y <= pcb[1] - box.ry)

        for b in boxes:
            # Add non overlapping constraint
            s.add(box.overlap(b))

        boxes.append(box)

# Project constraints:
# Minimize manually
s.add(area < 120)
s.add(boxes[0].x == pcb[0] / 2)
s.add(boxes[0].y == pcb[1] / 2)

print(s.check())
model = s.model()

pcb_a = model[area].as_long()
pcb_x = model[pcb[0]].as_long()
pcb_y = model[pcb[1]].as_long()
print('area: %s, %s x %s' % (str(pcb_a), str(pcb_x), str(pcb_y)))

grid = [[' ' for i in range(pcb_x)] for i in range(pcb_y)]
symbols = '*$%@+-%~&'

for i, b in enumerate(boxes):
    print(b.eval(model))
    for y in range(b.height):
        for x in range(b.width):
            pos_y = model[b.y].as_long() - b.ry + y
            pos_x = model[b.x].as_long() - b.rx + x
            grid[pos_y][pos_x] = symbols[i]

result = '_' * (pcb_x + 2) + '\n'
for line in grid:
    result += '|'
    for char in line:
        result += char
    result += '|\n'
result += '_' * (pcb_x + 2) + '\n'
print(result)

time python3 place.py
sat
area: 112, 14 x 8
x=7 y=4 w=5 h=5 rx=3 ry=3
x=12 y=7 w=4 h=2 rx=2 ry=1
x=2 y=3 w=4 h=2 rx=2 ry=1
x=2 y=7 w=4 h=2 rx=2 ry=1
x=12 y=1 w=4 h=2 rx=2 ry=1
x=12 y=3 w=4 h=2 rx=2 ry=1
x=2 y=1 w=4 h=2 rx=2 ry=1
x=2 y=5 w=4 h=2 rx=2 ry=1
x=12 y=5 w=4 h=2 rx=2 ry=1
________________
|%%%%      ++++|
|%%%%***** ++++|
|%%%%***** ----|
|%%%%***** ----|
|~~~~***** &&&&|
|~~~~***** &&&&|
|@@@@      $$$$|
|@@@@      $$$$|
________________

python3 place.py  2.82s user 0.03s system 99% cpu 2.863 total

[dvc94ch]

Modeling the pin assignment problem in Z3 prototype:

from z3 import *
import itertools

## Device
class Pin(object):
    counter = 0

    def __init__(self, *funs):
        self.id = Pin.counter
        Pin.counter += 1

        self.device = None
        self.funs = funs

        # Solution
        self.v_assign = Int('assign' + str(self.id))
        self.v_busassign = Int('busassign' + str(self.id))

        # Pin properties
        self.v_fun = Int('func' + str(self.id))
        self.v_bus = Int('bus' + str(self.id))

    def get_fun_by_name(self, name):
        for fun in self.funs:
            if fun.fun_name == name:
                return fun

    def pin_constraints(self):
        '''Pin constraints.'''

        _and = BoolVal(True)
        _or = BoolVal(False)
        for fun in self.funs:
            funid = self.device.funs_map[fun.fun_name]
            # Pin function can only be one of
            _or = Or(_or, self.v_fun == funid)
            if hasattr(fun, 'bus_name'):
                busid = self.device.buss_map[fun.bus_name]
                # If a pin has a function assigned it also has a bus assigned
                _and = And(_and, Implies(self.v_fun == funid,
                                         self.v_bus == busid))
                _and = And(_and, Implies(self.v_fun != funid,
                                         self.v_bus != busid))

        return And(_and, _or)

    def debug(self, model):
        return 'pin: %s assign: %s busassign: %s bus: %s func: %s\n' % \
            (self.id,
             str(model[self.v_assign]), str(model[self.v_busassign]),
             str(model[self.v_bus]), str(model[self.v_fun]))

    def eval(self, model):
        fun = model[self.v_fun].as_long()
        assign = model[self.v_assign].as_long()
        fun_name = self.device.funs[fun].fun_name
        return 'pin: %s func: %s assign: %s\n' % \
            (self.id, str(self.get_fun_by_name(fun_name)), str(assign))

class Device(object):
    def __init__(self, pins):
        self.pins = []
        self.buss = []
        self.buss_map = {}
        self.funs = []
        self.funs_map = {}

        for pin in pins:
            self.add_pin(pin)

    def add_pin(self, pin):
        pin.device = self
        self.pins.append(pin)
        for fun in pin.funs:
            if not fun.fun_name in self.funs_map:
                self.funs.append(fun)
                self.funs_map[fun.fun_name] = len(self.funs) - 1
            if hasattr(fun, 'bus_name'):
                if not fun.bus_name in self.buss_map:
                    self.buss.append(fun.bus_name)
                    self.buss_map[fun.bus_name] = len(self.buss) - 1

    def device_constraints(self):
        '''Device constraints.'''

        # Identity
        _and = BoolVal(True)

        # Each pin can only have one assignment.
        _and = And(_and, Distinct([p.v_assign for p in self.pins]))

        for p in self.pins:
            # Add pin constraints
            _and = And(_and, p.pin_constraints())

        # Each unique busassignment needs to be to a different busid.
        for p1, p2 in itertools.combinations(self.pins, 2):
            _and = And(_and, Implies(p1.v_busassign != p2.v_busassign,
                                     p1.v_bus != p2.v_bus))

        return _and

    def assignment_constraints(self, assign):
        '''Assignment constraints.'''

        # Identities
        _and = BoolVal(True)
        _or = BoolVal(False)

        for i, pin in enumerate(self.pins):
            # Each assignment can have only one pin.
            _or = Or(_or, pin.v_assign == assign.id)
            # An assignment to a pin implies that the pin's function
            # is the same as the assignments function.
            _and = And(_and, Implies(pin.v_assign == assign.id,
                       pin.v_fun == self.funs_map[assign.fun_name]))
            # An assignment implies the busassignment.
            _and = And(_and, Implies(pin.v_assign == assign.id,
                                     pin.v_busassign == assign.busassignid))

        return And(_and, _or)

    def debug(self, model):
        result = ''
        for pin in self.pins:
            result += pin.debug(model)
        return result

    def eval(self, model):
        result = ''
        for pin in self.pins:
            result += pin.eval(model)
        return result

class Fun(object):
    def __init__(self, name):
        self.fun_name = name

    def __str__(self):
        return self.fun_name

class BusFun(object):
    def __init__(self, bus_name, fun_name):
        self.fun_name = fun_name
        self.bus_name = bus_name

    def __str__(self):
        return '%s %s' % (self.bus_name, self.fun_name)

class Assign(object):
    counter = 1

    def __init__(self, fun_name):
        self.id = Assign.counter
        Assign.counter += 1

        self.busassignid = -self.id
        self.fun_name = fun_name

    def __iter__(self):
        yield self

class BusAssign(object):
    counter = 0

    def __init__(self, *assignments):
        self.id = BusAssign.counter
        BusAssign.counter += 1

        self.assignments = []
        for assig in assignments:
            self.add_assign(assig)

    def add_assign(self, assign):
        assign.busassignid = self.id
        self.assignments.append(assign)

    def __iter__(self):
        for assig in self.assignments:
            yield assig

## Problem
device = Device([
    Pin(Fun('GPIO'), BusFun('UART0', 'UART_TX')), # 0
    Pin(Fun('GPIO'), BusFun('UART0', 'UART_RX')), # 1
    Pin(Fun('GPIO'), BusFun('UART1', 'UART_TX')), # 2
    Pin(Fun('GPIO'), BusFun('UART1', 'UART_RX'))  # 3
])

assignments = [
    Assign('GPIO'), # 1
    Assign('GPIO'), # 2
    #BusAssign(
        Assign('UART_TX'), # 3
        Assign('UART_RX') # 4
    #)
]

s = Solver()
# Add constraints from device
s.add(device.device_constraints())

# Add constraints from assignments
for assign in assignments:
    for assign in assign:
        s.add(device.assignment_constraints(assign))

# Force a specific pin
# s.add(device.pins[0].v_assign == 3)

print(s.check())

model = s.model()

# print(device.debug(model))
print(device.eval(model))

time python3 pinassign.py
sat
pin: 0 func: GPIO assign: 2
pin: 1 func: UART0 UART_RX assign: 4
pin: 2 func: UART1 UART_TX assign: 3
pin: 3 func: GPIO assign: 1

python3 pinassign.py  0.46s user 0.02s system 99% cpu 0.488 total