Skip to content
Snippets Groups Projects
Commit 37b47442 authored by Per Lindgren's avatar Per Lindgren
Browse files

clk derive and proof improved

parent 48de5c26
No related branches found
No related tags found
No related merge requests found
...@@ -30,34 +30,29 @@ pub struct Unknowns { ...@@ -30,34 +30,29 @@ pub struct Unknowns {
pllq: u32, pllq: u32,
} }
fn pll_derive() -> Unknowns { fn pll_derive(req: Requirements) -> Unknowns {
// pll input default to HSI // assertions on requirements
kassert!(req.pllsrcclk % 1_000_000 == 0); // Multiple of 1MHz
let pllsrcclk = 8_000_000; kassert!(4_000_000 <= req.pllsrcclk && req.pllsrcclk <= 26_000_000); // Multiple of 1MHz
kassert!(req.sysclk % 1_000_000 == 0); // Multiple of 1MHz
// desired system clock, default to pll input
let sysclk = 96_000_000;
// Sysclk output divisor must be one of 2, 4, 6 or 8 // Sysclk output divisor must be one of 2, 4, 6 or 8
// (&!1 implies even numbers) // (&!1 implies even numbers)
let pllp = core::cmp::min(8, (432_000_000 / sysclk) & !1); let pllp = core::cmp::min(8, (432_000_000 / req.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; let mut pllm: u32 = 0;
ksymbol!(&mut pllm, "pllm"); ksymbol!(&mut pllm, "pllm");
kassume(pllm > 0); kassume(1 < pllm && pllm < 64); // field constraint
// require multiples of 1 MHz // Oscillator input constraint in the range from 1 to 2 MHz
kassume(1_000_000 <= pllsrcclk / pllm && pllsrcclk / pllm <= 2_000_000); kassume(1_000_000 <= req.pllsrcclk / pllm && req.pllsrcclk / pllm <= 2_000_000);
// only 4Mz..=26Mz allowed
kassume(4 <= pllm && pllm <= 26);
// Main scaler, // Main scaler,
let plln = sysclk * pllp / (pllsrcclk / pllm); let plln = req.sysclk * pllp / (req.pllsrcclk / pllm);
assert!(50 <= plln && plln <= 432); // constraint according to data sheet assert!(50 <= plln && plln <= 432); // field constraint
let osc = (pllsrcclk / pllm) * plln; // Oscillator output constraint
let osc = (req.pllsrcclk / pllm) * plln;
// 100MHz <= OSC <= 432MHz // 100MHz <= OSC <= 432MHz
kassume(100_000_000 <= osc && osc <= 432_000_000); kassume(100_000_000 <= osc && osc <= 432_000_000);
...@@ -65,13 +60,20 @@ fn pll_derive() -> Unknowns { ...@@ -65,13 +60,20 @@ fn pll_derive() -> Unknowns {
// kassume(192_000_000 <= osc && osc <= 432_000_000); // kassume(192_000_000 <= osc && osc <= 432_000_000);
// compute USB clock // compute USB clock
// 1-2MHz * plln / pllq = 48Mhz // OSC / pllq = 48Mhz
let pllq = (pllsrcclk / pllm) * plln / 48_000_000; 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 // Calculate real system clock
let sysclk_real = (pllsrcclk / pllm) * plln / pllp; let sysclk_real = osc / pllp;
kassume(sysclk_real == sysclk); kassume(sysclk_real == req.sysclk);
Unknowns { Unknowns {
pllp, pllp,
...@@ -94,7 +96,13 @@ fn main() { ...@@ -94,7 +96,13 @@ fn main() {
ksymbol!(&mut plln, "plln"); ksymbol!(&mut plln, "plln");
ksymbol!(&mut pllq, "pllq"); ksymbol!(&mut pllq, "pllq");
let u = pll_derive(); let req = Requirements {
pllsrcclk: 8_000_000,
sysclk: 96_000_000,
usbclk: true,
};
let u = pll_derive(req);
kassume(pllp == u.pllp); kassume(pllp == u.pllp);
// kassume(pll_in == u.pll_in); // kassume(pll_in == u.pll_in);
kassume(pllm == u.pllm); kassume(pllm == u.pllm);
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment