clk.rs

#![no_std]
#![no_main]

#[macro_use]
extern crate klee;
extern crate panic_abort;

use klee::{kassert, kassume, ksymbol};

#[derive(Clone, Copy, Debug)]
pub struct CFGR {
    hse: Option<u32>,
    hclk: Option<u32>,
    pclk1: Option<u32>,
    pclk2: Option<u32>,
    sysclk: Option<u32>,
    usbclk: bool,
}

pub struct Requirements {
    pllsrcclk: u32,
    sysclk: u32,
    usbclk: bool,
}

pub struct Unknowns {
    pllp: u32,
    pllm: u32,
    plln: u32,
    pllq: u32,
}

fn pll_derive(req: Requirements) -> Unknowns {
    // assertions on requirements
    kassert!(req.pllsrcclk % 1_000_000 == 0); // Multiple of 1MHz
    kassert!(4_000_000 <= req.pllsrcclk && req.pllsrcclk <= 26_000_000); // Multiple of 1MHz
    kassert!(req.sysclk % 1_000_000 == 0); // Multiple of 1MHz

    // Sysclk output divisor must be one of 2, 4, 6 or 8
    // (&!1 implies even numbers)
    let pllp = core::cmp::min(8, (432_000_000 / req.sysclk) & !1);

    let mut pllm: u32 = 0;
    ksymbol!(&mut pllm, "pllm");
    kassume(1 < pllm && pllm < 64); // field constraint

    // Oscillator input constraint in the range from 1 to 2 MHz
    kassume(1_000_000 <= req.pllsrcclk / pllm && req.pllsrcclk / pllm <= 2_000_000);

    // Main scaler,
    let plln = req.sysclk * pllp / (req.pllsrcclk / pllm);
    assert!(50 <= plln && plln <= 432); // field constraint

    // Oscillator output constraint
    let osc = (req.pllsrcclk / pllm) * plln;
    // 100MHz <= OSC <= 432MHz
    kassume(100_000_000 <= osc && osc <= 432_000_000);

    // 192MHz  <= OSC <= 432MHz // for F401
    // kassume(192_000_000 <= osc && osc <= 432_000_000);

    // compute USB clock
    // OSC / pllq = 48Mhz
    let pllq = if req.usbclk {
        let pllq = osc / 48_000_000;
        kassume(osc / pllq == 48_000_000); // soundness
        kassume(1 < pllq && pllq < 16); // field constraint
        pllq
    } else {
        2 // set a valid value
    };

    // Calculate real system clock
    let sysclk_real = osc / pllp;

    kassume(sysclk_real == req.sysclk);

    Unknowns {
        pllp,
        pllm,
        plln,
        pllq,
    }
}

#[no_mangle]
fn main() {
    let mut pllp: u32 = 0;
    // let mut pll_in: u32 = 0;
    let mut pllm: u32 = 0;
    let mut plln: u32 = 0;
    let mut pllq: u32 = 0;
    ksymbol!(&mut pllp, "pllp");
    // ksymbol!(&mut pll_in, "pll_in");
    ksymbol!(&mut pllm, "pllm");
    ksymbol!(&mut plln, "plln");
    ksymbol!(&mut pllq, "pllq");

    let req = Requirements {
        pllsrcclk: 8_000_000,
        sysclk: 96_000_000,
        usbclk: true,
    };

    let u = pll_derive(req);
    kassume(pllp == u.pllp);
    // kassume(pll_in == u.pll_in);
    kassume(pllm == u.pllm);
    kassume(plln == u.plln);
    kassume(pllq == u.pllq);
}