clk derive and proof

klee-examples/Cargo.toml

@@ -44,6 +44,10 @@ path = "src/register.rs"
 name = "peripheral"
 path = "src/peripheral.rs"
 
+[[bin]]
+name = "clk"
+path = "src/clk.rs"
+
 [profile.dev]
 incremental = false
 # lto = true
@@ -51,6 +55,7 @@ incremental = false
 [profile.release]
 debug = true
 panic = "abort"
+incremental = false
 lto = true
 
 [features]

klee-examples/src/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() -> Unknowns {
+    // pll input default to HSI
+
+    let pllsrcclk = 8_000_000;
+
+    // desired system clock, default to pll input
+    let sysclk = 96_000_000;
+
+    // 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 / sysclk) & !1);
+
+    // Input divisor from PLL source clock, must result to frequency in
+    // the range from 1 to 2 MHz
+    let mut pllm: u32 = 0;
+    ksymbol!(&mut pllm, "pllm");
+    kassume(pllm > 0);
+
+    // require multiples of 1 MHz
+    kassume(1_000_000 <= pllsrcclk / pllm && pllsrcclk / pllm <= 2_000_000);
+    // only 4Mz..=26Mz allowed
+    kassume(4 <= pllm && pllm <= 26);
+
+    // Main scaler,
+    let plln = sysclk * pllp / (pllsrcclk / pllm);
+    assert!(50 <= plln && plln <= 432); // constraint according to data sheet
+
+    let osc = (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
+    // 1-2MHz * plln / pllq = 48Mhz
+    let pllq = (pllsrcclk / pllm) * plln / 48_000_000;
+
+    // Calculate real system clock
+    let sysclk_real = (pllsrcclk / pllm) * plln / pllp;
+
+    kassume(sysclk_real == 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 u = pll_derive();
+    kassume(pllp == u.pllp);
+    // kassume(pll_in == u.pll_in);
+    kassume(pllm == u.pllm);
+    kassume(plln == u.plln);
+    kassume(pllq == u.pllq);
+}