| -- |
| -- Copyright (C) 2022 Google, LLC |
| -- |
| -- This program is free software; you can redistribute it and/or modify |
| -- it under the terms of the GNU General Public License as published by |
| -- the Free Software Foundation; either version 2 of the License, or |
| -- (at your option) any later version. |
| -- |
| -- This program is distributed in the hope that it will be useful, |
| -- but WITHOUT ANY WARRANTY; without even the implied warranty of |
| -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the |
| -- GNU General Public License for more details. |
| -- |
| |
| private package HW.GFX.GMA.PLLs |
| with |
| Abstract_State => (State with Part_Of => GMA.State) |
| is |
| |
| -- XXX: Types should be private (but that triggers a bug in SPARK GPL 2016) |
| type T is (Invalid_PLL, DPLL0, DPLL1, DPLL4, DPLL2); |
| subtype Configurable_DPLLs is T range DPLL0 .. DPLL4; |
| Invalid : constant T := Invalid_PLL; |
| |
| procedure Initialize |
| with |
| Global => (Output => State); |
| |
| pragma Warnings (Off, "unused variable ""Port_Cfg""", |
| Reason => "Not yet implemented."); |
| procedure Alloc |
| (Port_Cfg : in Port_Config; |
| PLL : out T; |
| Success : out Boolean); |
| pragma Warnings (On, "unused variable ""Port_Cfg"""); |
| |
| |
| pragma Warnings (Off, "subprogram ""Free"" has no effect", |
| Reason => "Not yet implemented."); |
| procedure Free (PLL : T); |
| pragma Warnings (On, "subprogram ""Free"" has no effect"); |
| |
| pragma Warnings (Off, "subprogram ""All_Off"" has no effect", |
| Reason => "Not yet implemented."); |
| procedure All_Off; |
| pragma Warnings (On, "subprogram ""All_Off"" has no effect"); |
| |
| pragma Warnings (Off, "unused variable ""PLL""", |
| Reason => "Not yet implemented."); |
| function Register_Value (PLL : T) return Word32; |
| pragma Warnings (On, "unused variable ""PLL"""); |
| |
| end HW.GFX.GMA.PLLs; |