In [30]:

    

from z3 import *

# Lets create a dictionary of all of our parameters.
# Where:
#    - f_in: Input Frequency
#    - f_out: Output Frequency
#    - d: PRDIV from datasheet. This is the division term
#    - m: VDIV from datasheet. This is the multiply term
params = {k: Int(k) for k in ['f_in', 'f_out', 'd', 'm']}

# Lets look at the datasheet and define some constraints on value ranges
# The range tuples are in the format (lower_bound, upper_bound) 
divide_range = (2e6, 4e6) # From K64F12 datasheet page 589 
d_range = (1, 25)         # From K64F12 datasheet page 589
m_range = (24, 55)        # From K64F12 datasheet page 590

# Get the input and output frequency as user inputs. 
# This is a quick and dirty handling of the inputs.
freq_in = 25e6
freq_out = 120e6

# Now we can constrain the equation with the "facts" we know
facts = [
    # define
    params['f_in'] == freq_in,
    params['f_out'] == freq_out,
    
    # Setup the equation which uses PRDIV (d) and VDIV (m)
    # This equation is set up from the K64 datasheet
    params['f_out'] == (params['f_in'] / params['d']) * params['m'],

    # From K64 datasheet page 589
    params['f_in'] / params['d'] >= divide_range[0],
    params['f_in'] / params['d'] <= divide_range[1],

    # From K64 datasheet page 589
    params['d'] >= d_range[0],  
    params['d'] <= d_range[1],

    # From K64 datasheet page 590
    params['m'] >= m_range[0],  
    params['m'] <= m_range[1]]

# To print out the results
model = solve(facts)

# But the model returns none
print model


    

    




[d = 10, m = 48, f_out = 120000000, f_in = 25000000]
None

In [31]:

    

#This method is defined in k64_pll_calculator/util.py
def solve_return_model(fact_list):
    """
    The default z3.solve() method prints to the screen. This uses the basis of
    that function to take a list of facts, add it to a solver and then return
    a z3 model with a solution.

    Relies on exceptions raised by calling s.mode() on an invalid model.

    @param a list of z3 facts and constraints
    @return A valid z3 model
    @raises Z3Exception
    """
    s = Solver()
    s.add(*fact_list)
    r = s.check()
    if r == unsat:
        print("no solution")
    elif r == unknown:
        print("failed to solve")

    return s.model()

model = solve_return_model(facts)

print(model)
print("Now we can play with the model: f_in == {}".format(model[params['f_in']]))


    

    




[d = 10, m = 48, f_out = 120000000, f_in = 25000000]
Now we can play with the model: f_in == 25000000