diff --git a/common/Makefile.inc b/common/Makefile.inc
index 11ca2c3..ba48f85 100644
--- a/common/Makefile.inc
+++ b/common/Makefile.inc
@@ -51,8 +51,36 @@
 CONFIG_GFX_GMA_INTERNAL_PORT	:= $(call strip_quotes,$(CONFIG_GFX_GMA_INTERNAL_PORT))
 CONFIG_GFX_GMA_ANALOG_I2C_PORT	:= $(call strip_quotes,$(CONFIG_GFX_GMA_ANALOG_I2C_PORT))
 
+_GEN_NONCONST := $(strip \
+		 $(if $(filter Ironlake,$(CONFIG_GFX_GMA_GENERATION)),ilk, \
+		 $(if $(filter Haswell,$(CONFIG_GFX_GMA_GENERATION)),hsw,  \
+		 $(if $(filter Skylake,$(CONFIG_GFX_GMA_GENERATION)),skl))))
+# GNATprove (GPL 2017) doesn't realize when a boolean expression
+# that depends both on static values and variables can be evalu-
+# ated at compile time (e.g. `False and then Variable` is always
+# `False` and GNAT acts appropriately). So for now, we generate
+# functions instead of constant expressions for these mixed ex-
+# pressions.
+_GEN_CONST_TARGET := <cpufunc> # set to `constant` to generate constants.
+
 hw-gfx-gma-config-ads := $(subst //,/,$(call src-to-obj,,$(dir)/hw-gfx-gma-config).ads)
 
+ifeq ($(CONFIG_GFX_GMA_DYN_CPU),y)
+$(hw-gfx-gma-config-ads): $(dir)/hw-gfx-gma-config.ads.template $(cnf)
+	printf "    GENERATE   $(patsubst /%,%,$(subst $(obj)/,,$@))\n"
+	sed -e's/<<GEN>>/$(CONFIG_GFX_GMA_GENERATION)/' \
+	    -e's/<<INTERNAL_PORT>>/$(CONFIG_GFX_GMA_INTERNAL_PORT)/' \
+	    -e's/<<ANALOG_I2C_PORT>>/$(CONFIG_GFX_GMA_ANALOG_I2C_PORT)/' \
+	    -e's/<<DEFAULT_MMIO_BASE>>/$(CONFIG_GFX_GMA_DEFAULT_MMIO)/' \
+	    -e'/constant Gen_CPU\(_Var\)\?/d' \
+	    -e's/<genbool>/constant Boolean/' \
+	    -e's/<\(\(ilk\|hsw\|skl\)\(...\)\?\)bool>/<\1var> Boolean/' \
+	    $(if $(_GEN_NONCONST),-e's/<\(...\)\?$(_GEN_NONCONST)\(...\)\?var>/<cpufunc>/') \
+	    -e's/<\(ilk\|hsw\|skl\)\(...\)\?var>/$(_GEN_CONST_TARGET)/' \
+	    -e's/\(.*: *<cpufunc>.*:=\) *\(.*\);/\1\n     (\2);/' \
+	    -e's/\([^ ]\+\) *: *<cpufunc> \+\([^ ]*\) *:=/function \1 return \2 is/' \
+	    $< >$@
+else
 $(hw-gfx-gma-config-ads): $(dir)/hw-gfx-gma-config.ads.template $(cnf)
 	printf "    GENERATE   $(patsubst /%,%,$(subst $(obj)/,,$@))\n"
 	sed -e's/<<GEN>>/$(CONFIG_GFX_GMA_GENERATION)/' \
@@ -61,9 +89,12 @@
 	    -e's/<<INTERNAL_PORT>>/$(CONFIG_GFX_GMA_INTERNAL_PORT)/' \
 	    -e's/<<ANALOG_I2C_PORT>>/$(CONFIG_GFX_GMA_ANALOG_I2C_PORT)/' \
 	    -e's/<<DEFAULT_MMIO_BASE>>/$(CONFIG_GFX_GMA_DEFAULT_MMIO)/' \
+	    -e":s$$(printf '\n ')/,$$/{N;s/,\n.*Dyn_CPU\(_Var\)\?[^,)]*//;ts$$(printf '\n ')P;D;}" \
+	    -e'/Dyn_CPU\(_Var\)\?/d' \
 	    -e's/<\(gen\|\(ilk\|hsw\|skl\)\(...\)\?\)bool>/constant Boolean/' \
 	    -e's/<\(\(ilk\|hsw\|skl\)\(...\)\?\)var>/constant/' \
 	    $< >$@
+endif
 gfxinit-gen-y += $(hw-gfx-gma-config-ads)
 
 ifneq ($(filter G45,$(CONFIG_GFX_GMA_CPU)),)