From 37b474428f09e125d8515cf33e03e6d629d67a3a Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Sat, 16 Feb 2019 23:24:21 +0100
Subject: [PATCH] clk derive and proof improved
---
klee-examples/src/clk.rs | 54 +++++++++++++++++++++++-----------------
1 file changed, 31 insertions(+), 23 deletions(-)
diff --git a/klee-examples/src/clk.rs b/klee-examples/src/clk.rs
index e17bff0..d8b689d 100644
--- a/klee-examples/src/clk.rs
+++ b/klee-examples/src/clk.rs
@@ -30,34 +30,29 @@ pub struct Unknowns {
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;
+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 / 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;
ksymbol!(&mut pllm, "pllm");
- kassume(pllm > 0);
+ kassume(1 < pllm && pllm < 64); // field constraint
- // 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);
+ // 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 = sysclk * pllp / (pllsrcclk / pllm);
- assert!(50 <= plln && plln <= 432); // constraint according to data sheet
+ let plln = req.sysclk * pllp / (req.pllsrcclk / pllm);
+ assert!(50 <= plln && plln <= 432); // field constraint
- let osc = (pllsrcclk / pllm) * plln;
+ // Oscillator output constraint
+ let osc = (req.pllsrcclk / pllm) * plln;
// 100MHz <= OSC <= 432MHz
kassume(100_000_000 <= osc && osc <= 432_000_000);
@@ -65,13 +60,20 @@ fn pll_derive() -> Unknowns {
// 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;
+ // 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 = (pllsrcclk / pllm) * plln / pllp;
+ let sysclk_real = osc / pllp;
- kassume(sysclk_real == sysclk);
+ kassume(sysclk_real == req.sysclk);
Unknowns {
pllp,
@@ -94,7 +96,13 @@ fn main() {
ksymbol!(&mut plln, "plln");
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(pll_in == u.pll_in);
kassume(pllm == u.pllm);
--
GitLab