\documentclass{amsart}
    \advance\textheight by 1.75in
    \advance\textwidth by 2in
    \advance\topmargin by -1in
    \advance\oddsidemargin by -1in
    \advance\evensidemargin by -1in
    \usepackage{amssymb}
    \parindent0pt
    \begin{document}
    \textbf{HWV001-1.ax} Half-adder.






$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{type}(\mbox{and}_1(x),\mbox{and})\qquad\mbox{cnf}(\mbox{halfadder\_and}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{type}(\mbox{and}_2(x),\mbox{and})\qquad\mbox{cnf}(\mbox{halfadder\_and}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{type}(\mbox{not}_1(x),\mbox{not})\qquad\mbox{cnf}(\mbox{halfadder\_not}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{type}(\mbox{or}_1(x),\mbox{or})\qquad\mbox{cnf}(\mbox{halfadder\_or}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{connection}(\mbox{in}(n_1,x),\mbox{in}(n_1,\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_in1\_in1or}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{connection}(\mbox{in}(n_2,x),\mbox{in}(n_2,\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_in2\_in2or}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{connection}(\mbox{in}(n_1,x),\mbox{in}(n_1,\mbox{and}_2(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_in1\_in1and}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{connection}(\mbox{in}(n_2,x),\mbox{in}(n_2,\mbox{and}_2(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_in2\_in2and}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(s,x),\mbox{out}(n_1,\mbox{and}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_outs\_out1and}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(c,x),\mbox{out}(n_1,\mbox{and}_2(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_outc\_out1and}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(n_1,\mbox{or}_1(x)),\mbox{in}(n_1,\mbox{and}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_out1or1\_in1\_and}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(n_1,\mbox{and}_2(x)),\mbox{in}(n_1,\mbox{not}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_out1and2\_in1not}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{halfadder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(n_1,\mbox{not}_1(x)),\mbox{in}(n_2,\mbox{and}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_out1not1\_in2and}_1,\mbox{axiom})$

\medskip\textbf{HWV002-1.ax} Half-adder.






$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{logic\_and}(\mbox{and}_1(x))\qquad\mbox{cnf}(\mbox{halfadder\_and}_1,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{logic\_and}(\mbox{and}_2(x))\qquad\mbox{cnf}(\mbox{halfadder\_and}_2,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{logic\_not}(\mbox{not}_1(x))\qquad\mbox{cnf}(\mbox{halfadder\_not}_1,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{logic\_or}(\mbox{or}_1(x))\qquad\mbox{cnf}(\mbox{halfadder\_or}_1,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{in}_1(x),\mbox{in}_1(\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_in1\_in1or}_1,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{in}_2(x),\mbox{in}_2(\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_in2\_in2or}_1,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{in}_1(x),\mbox{in}_1(\mbox{and}_2(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_in1\_in1and}_2,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{in}_2(x),\mbox{in}_2(\mbox{and}_2(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_in2\_in2and}_2,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{outs}(x),\mbox{out}_1(\mbox{and}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_outs\_out1and}_1,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{outc}(x),\mbox{out}_1(\mbox{and}_2(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_outc\_out1and}_2,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{out}_1(\mbox{or}_1(x)),\mbox{in}_1(\mbox{and}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_out1or1\_in1\_and}_1,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{out}_1(\mbox{and}_2(x)),\mbox{in}_1(\mbox{not}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_out1and2\_in1not}_1,\mbox{axiom})$

$\mbox{halfadder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{out}_1(\mbox{not}_1(x)),\mbox{in}_2(\mbox{and}_1(x)))\qquad\mbox{cnf}(\mbox{halfadder\_connection\_out1not1\_in2and}_1,\mbox{axiom})$

\medskip\textbf{HWV002-2.ax} Full-adder.






$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{halfadder}(h_1(x))\qquad\mbox{cnf}(\mbox{fulladder\_halfadder}_1,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{halfadder}(h_2(x))\qquad\mbox{cnf}(\mbox{fulladder\_halfadder}_2,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{logic\_or}(\mbox{or}_1(x))\qquad\mbox{cnf}(\mbox{fulladder\_or}_1,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{outs}(h_1(x)),\mbox{in}_2(h_2(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outsh1\_in2h}_2,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{outc}(h_1(x)),\mbox{in}_2(\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outch1\_in2or}_1,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{outc}(h_2(x)),\mbox{in}_1(\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outch2\_in1or}_1,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{in}_1(x),\mbox{in}_1(h_2(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_in1\_in1h}_2,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{in}_2(x),\mbox{in}_1(h_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_in2\_in1h}_1,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{inc}(x),\mbox{in}_2(h_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_inc\_in2h}_1,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{outs}(x),\mbox{outs}(h_2(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outs\_outsh}_2,\mbox{axiom})$

$\mbox{fulladder}(x) \ \Rightarrow \ \mbox{connection}(\mbox{outc}(x),\mbox{out}_1(\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outc\_out1or}_1,\mbox{axiom})$

\medskip\textbf{HWV002-0.ax} Connections, faults, and gates.






$( \mbox{connection}(p_1,p_2)\mbox{ and }0 ) \ \Rightarrow \ 0\qquad\mbox{cnf}(\mbox{value\_propagation\_zero}_1,\mbox{axiom})$

$( \mbox{connection}(p_1,p_2)\mbox{ and }1 ) \ \Rightarrow \ 1\qquad\mbox{cnf}(\mbox{value\_propagation\_one}_1,\mbox{axiom})$

$( \mbox{connection}(p_1,p_2)\mbox{ and }0 ) \ \Rightarrow \ 0\qquad\mbox{cnf}(\mbox{value\_propagation\_zero}_2,\mbox{axiom})$

$( \mbox{connection}(p_1,p_2)\mbox{ and }1 ) \ \Rightarrow \ 1\qquad\mbox{cnf}(\mbox{value\_propagation\_one}_2,\mbox{axiom})$

$0 \ \Rightarrow \ \neg\,1\qquad\mbox{cnf}(\mbox{unique\_value},\mbox{axiom})$

$( \mbox{and\_ok}(k)\mbox{ and }0 ) \ \Rightarrow \ 0\qquad\mbox{cnf}(\mbox{and\_0x}_0,\mbox{axiom})$

$( \mbox{and\_ok}(k)\mbox{ and }0 ) \ \Rightarrow \ 0\qquad\mbox{cnf}(\mbox{and\_x0}_0,\mbox{axiom})$

$( \mbox{and\_ok}(k)\mbox{ and }1\mbox{ and }1 ) \ \Rightarrow \ 1\qquad\mbox{cnf}(\mbox{and\_11}_1,\mbox{axiom})$

$( \mbox{and\_ok}(k)\mbox{ and }0 ) \ \Rightarrow \ ( 0\mbox{ or }0 )\qquad\mbox{cnf}(\mbox{and\_0}_{00},\mbox{axiom})$

$( \mbox{and\_ok}(k)\mbox{ and }1 ) \ \Rightarrow \ 1\qquad\mbox{cnf}(\mbox{and\_1\_1x},\mbox{axiom})$

$( \mbox{and\_ok}(k)\mbox{ and }1 ) \ \Rightarrow \ 1\qquad\mbox{cnf}(\mbox{and\_1\_x}_1,\mbox{axiom})$

$\mbox{and\_ok}(k) \ \Rightarrow \ \neg\,\mbox{abnormal}(k)\qquad\mbox{cnf}(\mbox{not\_and\_ok\_and\_abnormal},\mbox{axiom})$

$\mbox{logic\_and}(k) \ \Rightarrow \ ( \mbox{and\_ok}(k)\mbox{ or }\mbox{abnormal}(k) )\qquad\mbox{cnf}(\mbox{and\_ok\_or\_abnormal},\mbox{axiom})$

$( \mbox{or\_ok}(k)\mbox{ and }1 ) \ \Rightarrow \ 1\qquad\mbox{cnf}(\mbox{or\_1x}_1,\mbox{axiom})$

$( \mbox{or\_ok}(k)\mbox{ and }1 ) \ \Rightarrow \ 1\qquad\mbox{cnf}(\mbox{or\_x1}_1,\mbox{axiom})$

$( \mbox{or\_ok}(k)\mbox{ and }0\mbox{ and }0 ) \ \Rightarrow \ 0\qquad\mbox{cnf}(\mbox{or\_00}_0,\mbox{axiom})$

$( \mbox{or\_ok}(k)\mbox{ and }1 ) \ \Rightarrow \ ( 1\mbox{ or }1 )\qquad\mbox{cnf}(\mbox{or\_1}_{11},\mbox{axiom})$

$( \mbox{or\_ok}(k)\mbox{ and }0 ) \ \Rightarrow \ 0\qquad\mbox{cnf}(\mbox{or\_0\_0x},\mbox{axiom})$

$( \mbox{or\_ok}(k)\mbox{ and }0 ) \ \Rightarrow \ 0\qquad\mbox{cnf}(\mbox{or\_0}_{01},\mbox{axiom})$

$\mbox{or\_ok}(k) \ \Rightarrow \ \neg\,\mbox{abnormal}(k)\qquad\mbox{cnf}(\mbox{not\_or\_ok\_and\_abnormal},\mbox{axiom})$

$\mbox{logic\_or}(k) \ \Rightarrow \ ( \mbox{or\_ok}(k)\mbox{ or }\mbox{abnormal}(k) )\qquad\mbox{cnf}(\mbox{or\_ok\_or\_abnormal},\mbox{axiom})$

$( \mbox{not\_ok}(k)\mbox{ and }0 ) \ \Rightarrow \ 1\qquad\mbox{cnf}(\mbox{not\_0\_1\_fw},\mbox{axiom})$

$( \mbox{not\_ok}(k)\mbox{ and }1 ) \ \Rightarrow \ 0\qquad\mbox{cnf}(\mbox{not\_1\_0\_fw},\mbox{axiom})$

$( \mbox{not\_ok}(k)\mbox{ and }0 ) \ \Rightarrow \ 1\qquad\mbox{cnf}(\mbox{not\_0\_1\_bw},\mbox{axiom})$

$( \mbox{not\_ok}(k)\mbox{ and }1 ) \ \Rightarrow \ 0\qquad\mbox{cnf}(\mbox{not\_1\_0\_bw},\mbox{axiom})$

$\mbox{not\_ok}(k) \ \Rightarrow \ \neg\,\mbox{abnormal}(k)\qquad\mbox{cnf}(\mbox{not\_\_not\_ok\_and\_abnormal},\mbox{axiom})$

$\mbox{logic\_not}(k) \ \Rightarrow \ ( \mbox{not\_ok}(k)\mbox{ or }\mbox{abnormal}(k) )\qquad\mbox{cnf}(\mbox{not\_ok\_or\_abnormal},\mbox{axiom})$

\medskip\textbf{HWV001-0.ax} Connections, faults, and gates.






$( \mbox{connection}(p_1,p_2)\mbox{ and }\mbox{value}(p_1,v) ) \ \Rightarrow \ \mbox{value}(p_2,v)\qquad\mbox{cnf}(\mbox{value\_propagation}_1,\mbox{axiom})$

$( \mbox{connection}(p_1,p_2)\mbox{ and }\mbox{value}(p_2,v) ) \ \Rightarrow \ \mbox{value}(p_1,v)\qquad\mbox{cnf}(\mbox{value\_propagation}_2,\mbox{axiom})$

$( \mbox{value}(p,v_1)\mbox{ and }\mbox{value}(p,v_2) ) \ \Rightarrow \ \mbox{equal\_value}(v_1,v_2)\qquad\mbox{cnf}(\mbox{unique\_value},\mbox{axiom})$

$\neg\,\mbox{equal\_value}(n_0,n_1)\qquad\mbox{cnf}(\mbox{equal\_value}_1,\mbox{axiom})$

$\neg\,\mbox{equal\_value}(n_1,n_0)\qquad\mbox{cnf}(\mbox{equal\_value}_2,\mbox{axiom})$

$\mbox{mode}(k,\mbox{ok}) \ \Rightarrow \ \neg\,\mbox{mode}(k,\mbox{abnormal})\qquad\mbox{cnf}(\mbox{not\_ok\_and\_abnormal},\mbox{axiom})$

$\mbox{type}(k,\mbox{any}) \ \Rightarrow \ ( \mbox{mode}(k,\mbox{ok})\mbox{ or }\mbox{mode}(k,\mbox{abnormal}) )\qquad\mbox{cnf}(\mbox{ok\_or\_abnormal},\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{and})\mbox{ and }\mbox{value}(\mbox{in}(\mbox{any},k),n_0) ) \ \Rightarrow \ \mbox{value}(\mbox{out}(n_1,k),n_0)\qquad\mbox{cnf}(\mbox{and\_0x}_0,\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{and})\mbox{ and }\mbox{value}(\mbox{in}(n_1,k),n_1)\mbox{ and }\mbox{value}(\mbox{in}(n_2,k),n_1) ) \ \Rightarrow \ \mbox{value}(\mbox{out}(n_1,k),n_1)\qquad\mbox{cnf}(\mbox{and\_11}_1,\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{and})\mbox{ and }\mbox{value}(\mbox{out}(n_1,k),n_0) ) \ \Rightarrow \ ( \mbox{value}(\mbox{in}(n_1,k),n_0)\mbox{ or }\mbox{value}(\mbox{in}(n_2,k),n_0) )\qquad\mbox{cnf}(\mbox{and\_0}_{00},\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{and})\mbox{ and }\mbox{value}(\mbox{out}(n_1,k),n_1) ) \ \Rightarrow \ \mbox{value}(\mbox{in}(n_1,k),n_1)\qquad\mbox{cnf}(\mbox{and\_1\_1x},\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{and})\mbox{ and }\mbox{value}(\mbox{out}(n_1,k),n_1) ) \ \Rightarrow \ \mbox{value}(\mbox{in}(n_2,k),n_1)\qquad\mbox{cnf}(\mbox{and\_1\_x}_1,\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{or})\mbox{ and }\mbox{value}(\mbox{in}(\mbox{any},k),n_1) ) \ \Rightarrow \ \mbox{value}(\mbox{out}(n_1,k),n_1)\qquad\mbox{cnf}(\mbox{or\_1x}_1,\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{or})\mbox{ and }\mbox{value}(\mbox{in}(n_1,k),n_0)\mbox{ and }\mbox{value}(\mbox{in}(n_2,k),n_0) ) \ \Rightarrow \ \mbox{value}(\mbox{out}(n_1,k),n_0)\qquad\mbox{cnf}(\mbox{or\_00}_0,\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{or})\mbox{ and }\mbox{value}(\mbox{out}(n_1,k),n_1) ) \ \Rightarrow \ ( \mbox{value}(\mbox{in}(n_1,k),n_1)\mbox{ or }\mbox{value}(\mbox{in}(n_2,k),n_1) )\qquad\mbox{cnf}(\mbox{or\_1}_{11},\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{or})\mbox{ and }\mbox{value}(\mbox{out}(n_1,k),n_0) ) \ \Rightarrow \ \mbox{value}(\mbox{in}(n_1,k),n_0)\qquad\mbox{cnf}(\mbox{or\_0\_0x},\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{or})\mbox{ and }\mbox{value}(\mbox{out}(n_1,k),n_0) ) \ \Rightarrow \ \mbox{value}(\mbox{in}(n_2,k),n_0)\qquad\mbox{cnf}(\mbox{or\_0}_{01},\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{not})\mbox{ and }\mbox{value}(\mbox{in}(n_1,k),n_0) ) \ \Rightarrow \ \mbox{value}(\mbox{out}(n_1,k),n_1)\qquad\mbox{cnf}(\mbox{not\_0\_1\_fw},\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{not})\mbox{ and }\mbox{value}(\mbox{in}(n_1,k),n_1) ) \ \Rightarrow \ \mbox{value}(\mbox{out}(n_1,k),n_0)\qquad\mbox{cnf}(\mbox{not\_1\_0\_fw},\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{not})\mbox{ and }\mbox{value}(\mbox{out}(n_1,k),n_0) ) \ \Rightarrow \ \mbox{value}(\mbox{in}(n_1,k),n_1)\qquad\mbox{cnf}(\mbox{not\_0\_1\_bw},\mbox{axiom})$

$( \mbox{mode}(k,\mbox{ok})\mbox{ and }\mbox{type}(k,\mbox{not})\mbox{ and }\mbox{value}(\mbox{out}(n_1,k),n_1) ) \ \Rightarrow \ \mbox{value}(\mbox{in}(n_1,k),n_0)\qquad\mbox{cnf}(\mbox{not\_1\_0\_bw},\mbox{axiom})$

\medskip\textbf{HWV001-2.ax} Full-adder.






$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{type}(h_1(x),\mbox{halfadder})\qquad\mbox{cnf}(\mbox{fulladder\_halfadder}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{type}(h_2(x),\mbox{halfadder})\qquad\mbox{cnf}(\mbox{fulladder\_halfadder}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{type}(\mbox{or}_1(x),\mbox{or})\qquad\mbox{cnf}(\mbox{fulladder\_or}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(s,h_1(x)),\mbox{in}(n_2,h_2(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outsh1\_in2h}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(c,h_1(x)),\mbox{in}(n_2,\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outch1\_in2or}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(c,h_2(x)),\mbox{in}(n_1,\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outch2\_in1or}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{connection}(\mbox{in}(n_1,x),\mbox{in}(n_1,h_2(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_in1\_in1h}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{connection}(\mbox{in}(n_2,x),\mbox{in}(n_1,h_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_in2\_in1h}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{connection}(\mbox{in}(c,x),\mbox{in}(n_2,h_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_inc\_in2h}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(s,x),\mbox{out}(s,h_2(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outs\_outsh}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{fulladder}) \ \Rightarrow \ \mbox{connection}(\mbox{out}(c,x),\mbox{out}(n_1,\mbox{or}_1(x)))\qquad\mbox{cnf}(\mbox{fulladder\_connection\_outc\_out1or}_1,\mbox{axiom})$

\medskip\textbf{HWV011-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{p\_Full}(t_{139}) \ \Rightarrow \ \mbox{level}(t_{139})\ne \mbox{fifo\_length}\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Full}(t_{139})\mbox{ or }\mbox{level}(t_{139}) = \mbox{fifo\_length}\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV011-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206})\ne \mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_}\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfull\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV052-1.002.002.p} Faulty channel 2 2

The problem of sending N bits over a faulty channel that can
 mutilate any one bit. We can use K extra bits to help us do this.
 Satisfiable means that it is possible, unsatisfiable means that
 it is not possible.




$x = o\mbox{ or }x = i\qquad\mbox{cnf}(\mbox{bit\_domain},\mbox{axiom})$

$x^{-1}\ne x\qquad\mbox{cnf}(\mbox{bit\_inverse},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack}_1,\mbox{axiom})$

$\mbox{unpack}_1(x_1^{-1},x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{01},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2^{-1},\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{02},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,\mbox{pack}_1(x_1,x_2)^{-1},\mbox{pack}_2(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{03},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)^{-1}) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{04},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack}_2,\mbox{axiom})$

$\mbox{unpack}_2(x_1^{-1},x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{05},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2^{-1},\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{06},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,\mbox{pack}_1(x_1,x_2)^{-1},\mbox{pack}_2(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{07},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)^{-1}) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{08},\mbox{axiom})$

\medskip\textbf{HWV014-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}),n_0)\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(\mbox{f\_ADD\_}(t_{206},n_1))\ne \mbox{f\_SUB\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}),n_1)\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV011-3.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}) = \mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_}\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfull\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV017-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}),\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfull\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_0)\qquad\mbox{cnf}(\mbox{quest}_6,\mbox{negated\_conjecture})$

\medskip\textbf{HWV028-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{level}(t_{139} + n_1),\mbox{fifo\_length})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV005-2.p} A halfadder built from and, or and not gates






$\mbox{include}(\mbox{'Axioms/HWV002-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-1.ax'})$

$\mbox{halfadder}(h)\qquad\mbox{cnf}(\mbox{h\_isa\_halfadder},\mbox{hypothesis})$

$1\qquad\mbox{cnf}(\mbox{in1}_1,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{in2}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{outs}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{outc}_0,\mbox{hypothesis})$

$\neg\,\mbox{abnormal}(\mbox{and}_1(h))\qquad\mbox{cnf}(\mbox{diagnosis\_and}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{not}_1(h))\qquad\mbox{cnf}(\mbox{diagnosis\_not}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{or}_1(h))\qquad\mbox{cnf}(\mbox{diagnosis\_or}_1,\mbox{negated\_conjecture})$

\medskip\textbf{HWV017-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{gt}(\mbox{level}(t_{139}),\mbox{fifo\_length})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Rd}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{p\_Full}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},n_0)\qquad\mbox{cnf}(\mbox{quest}_6,\mbox{negated\_conjecture})$

\medskip\textbf{HWV008-1.002.p} 2 bit ripple carry adder






$\mbox{include}(\mbox{'Axioms/HWV001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-2.ax'})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{type}(f(n_1,x),\mbox{fulladder})\qquad\mbox{cnf}(\mbox{nbit\_adder\_fulladder}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{type}(f(n_2,x),\mbox{fulladder})\qquad\mbox{cnf}(\mbox{nbit\_adder\_fulladder}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{connection}(\mbox{out}(n_1,x),\mbox{out}(n_1,f(n_1,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_out1\_out1f}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{connection}(\mbox{out}(n_2,x),\mbox{out}(n_1,f(n_2,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_out2\_out1f}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{connection}(\mbox{out}(c,x),\mbox{out}(c,f(n_2,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_outc\_outcf}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{connection}(\mbox{in}(a_1,x),\mbox{in}(n_1,f(n_1,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_ina1\_in1f}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{connection}(\mbox{in}(b_1,x),\mbox{in}(n_2,f(n_1,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inb1\_in2f}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{connection}(\mbox{in}(a_2,x),\mbox{in}(n_1,f(n_2,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_ina2\_in1f}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{connection}(\mbox{in}(b_2,x),\mbox{in}(n_2,f(n_2,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inb2\_in2f}_2,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{connection}(\mbox{out}(c,f(n_1,x)),\mbox{in}(c,f(n_2,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inc\_incf}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_2)) \ \Rightarrow \ \mbox{connection}(\mbox{in}(c,x),\mbox{in}(c,f(n_1,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inc\_incf}_2,\mbox{axiom})$

$\mbox{type}(a,\mbox{nbit\_adder}(n_2))\qquad\mbox{cnf}(\mbox{a\_isa\_2bit\_adder},\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(a_1,a),n_0)\qquad\mbox{cnf}(\mbox{ina1}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(a_2,a),n_0)\qquad\mbox{cnf}(\mbox{ina2}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(b_1,a),n_0)\qquad\mbox{cnf}(\mbox{inb1}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(b_2,a),n_0)\qquad\mbox{cnf}(\mbox{inb2}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(c,a),n_0)\qquad\mbox{cnf}(\mbox{inc}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(n_1,a),n_0)\qquad\mbox{cnf}(\mbox{out1}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(n_2,a),n_0)\qquad\mbox{cnf}(\mbox{out2}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(c,a),n_1)\qquad\mbox{cnf}(\mbox{outc}_1,\mbox{hypothesis})$

$\neg\,\mbox{mode}(\mbox{or}_1(f(n_2,a)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or1f2a},\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{and}_2(h_1(f(n_2,a))),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_and2h2f2a},\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{and}_2(h_2(f(n_2,a))),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_and2h1f2a},\mbox{negated\_conjecture})$

\medskip\textbf{HWV020-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTempty\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTempty\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV010-3.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}) = n_0\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTempty\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV024-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{p\_Rd}(x_{140})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(x_{140})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_Data\_out}(x_{139},x_{140}) \ \Rightarrow \ \neg\,\mbox{p\_Data\_out}(x_{139},x_{140} + n_1)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_Data\_out}(x_{139},x_{140})\mbox{ or }\mbox{p\_Data\_out}(x_{139},x_{140} + n_1)\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV020-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{p\_Rd}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Empty}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{p\_Empty}(t_{139} + n_1) \ \Rightarrow \ \neg\,\mbox{p\_Rd\_error}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV052-1.002.001.p} Faulty channel 2 1

The problem of sending N bits over a faulty channel that can
 mutilate any one bit. We can use K extra bits to help us do this.
 Satisfiable means that it is possible, unsatisfiable means that
 it is not possible.




$x = o\mbox{ or }x = i\qquad\mbox{cnf}(\mbox{bit\_domain},\mbox{axiom})$

$x^{-1}\ne x\qquad\mbox{cnf}(\mbox{bit\_inverse},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,\mbox{pack}_1(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack}_1,\mbox{axiom})$

$\mbox{unpack}_1(x_1^{-1},x_2,\mbox{pack}_1(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{01},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2^{-1},\mbox{pack}_1(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{02},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,\mbox{pack}_1(x_1,x_2)^{-1}) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{03},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,\mbox{pack}_1(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack}_2,\mbox{axiom})$

$\mbox{unpack}_2(x_1^{-1},x_2,\mbox{pack}_1(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{04},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2^{-1},\mbox{pack}_1(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{05},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,\mbox{pack}_1(x_1,x_2)^{-1}) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{06},\mbox{axiom})$

\medskip\textbf{HWV025-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{p\_Rd}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_Rd\_error}(t_{139}) \ \Rightarrow \ \neg\,\mbox{p\_Rd\_error}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_Rd\_error}(t_{139})\mbox{ or }\mbox{p\_Rd\_error}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV001-1.p} Interchange inputs to outputs

This validates one of the circuit designs that will take x and
 y as input and output y and x without crossing any wires.




$\mbox{include}(\mbox{'Axioms/HWC002-0.ax'})$

$\mbox{and}(x,y) = \mbox{and}(y,x)\qquad\mbox{cnf}(\mbox{and\_commutativity},\mbox{axiom})$

$\mbox{or}(x,y) = \mbox{or}(y,x)\qquad\mbox{cnf}(\mbox{or\_commutativity},\mbox{axiom})$

$\mbox{and}(x,\mbox{and}(y,z)) = \mbox{and}(\mbox{and}(x,y),z)\qquad\mbox{cnf}(\mbox{and\_associativity},\mbox{axiom})$

$\mbox{or}(x,\mbox{or}(y,z)) = \mbox{or}(\mbox{or}(x,y),z)\qquad\mbox{cnf}(\mbox{or\_associativity},\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),z) = \mbox{or}(\mbox{or}(x,z),y)\qquad\mbox{cnf}(\mbox{or\_sorting},\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),z) = \mbox{and}(\mbox{and}(x,z),y)\qquad\mbox{cnf}(\mbox{and\_sorting},\mbox{axiom})$

$\mbox{not}(\mbox{and}(x,y)) = \mbox{or}(\mbox{not}(x),\mbox{not}(y))\qquad\mbox{cnf}(\mbox{not\_canonicalization}_1,\mbox{axiom})$

$\mbox{not}(\mbox{or}(x,y)) = \mbox{and}(\mbox{not}(x),\mbox{not}(y))\qquad\mbox{cnf}(\mbox{not\_canonicalization}_2,\mbox{axiom})$

$\mbox{and}(\mbox{or}(x,y),z) = \mbox{or}(\mbox{and}(x,z),\mbox{and}(y,z))\qquad\mbox{cnf}(\mbox{and\_or\_canonicalization},\mbox{axiom})$

$\mbox{and}(x,x) = x\qquad\mbox{cnf}(\mbox{and\_simplification}_1,\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),y) = \mbox{and}(x,y)\qquad\mbox{cnf}(\mbox{and\_simplification}_2,\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),x) = \mbox{and}(x,y)\qquad\mbox{cnf}(\mbox{and\_simplification}_3,\mbox{axiom})$

$\mbox{or}(x,x) = x\qquad\mbox{cnf}(\mbox{or\_simplification}_1,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),y) = \mbox{or}(x,y)\qquad\mbox{cnf}(\mbox{or\_simplification}_2,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),x) = \mbox{or}(x,y)\qquad\mbox{cnf}(\mbox{or\_simplification}_3,\mbox{axiom})$

$\mbox{and}(x,\mbox{not}(x)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_simplification}_1,\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),\mbox{not}(y)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_simplification}_2,\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),\mbox{not}(x)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_simplification}_3,\mbox{axiom})$

$\mbox{or}(x,\mbox{not}(x)) = n_1\qquad\mbox{cnf}(\mbox{or\_not\_simplification}_1,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),\mbox{not}(y)) = n_1\qquad\mbox{cnf}(\mbox{or\_not\_simplification}_2,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),\mbox{not}(x)) = n_1\qquad\mbox{cnf}(\mbox{or\_not\_simplification}_3,\mbox{axiom})$

$\mbox{not}(\mbox{not}(x)) = x\qquad\mbox{cnf}(\mbox{not\_simplification},\mbox{axiom})$

$\mbox{or}(\mbox{and}(x,y),\mbox{and}(x,\mbox{not}(y))) = x\qquad\mbox{cnf}(\mbox{and\_or\_not\_simplification}_1,\mbox{axiom})$

$\mbox{or}(\mbox{and}(x,y),\mbox{and}(y,\mbox{not}(x))) = y\qquad\mbox{cnf}(\mbox{and\_or\_not\_simplification}_2,\mbox{axiom})$

$a_1 = \mbox{and}(b_1,b_3)\qquad\mbox{cnf}(\mbox{constructor}_1,\mbox{negated\_conjecture})$

$a_2 = \mbox{and}(b_2,b_3)\qquad\mbox{cnf}(\mbox{constructor}_2,\mbox{negated\_conjecture})$

$b_1 = \mbox{not}(d_1)\qquad\mbox{cnf}(\mbox{constructor}_3,\mbox{negated\_conjecture})$

$b_2 = \mbox{not}(d_2)\qquad\mbox{cnf}(\mbox{constructor}_4,\mbox{negated\_conjecture})$

$b_3 = \mbox{or}(c_1,c_2)\qquad\mbox{cnf}(\mbox{constructor}_5,\mbox{negated\_conjecture})$

$c_1 = \mbox{or}(d_1,d_3)\qquad\mbox{cnf}(\mbox{constructor}_6,\mbox{negated\_conjecture})$

$c_2 = \mbox{or}(d_2,d_3)\qquad\mbox{cnf}(\mbox{constructor}_7,\mbox{negated\_conjecture})$

$d_3 = f_3\qquad\mbox{cnf}(\mbox{constructor}_8,\mbox{negated\_conjecture})$

$d_1 = \mbox{not}(e_1)\qquad\mbox{cnf}(\mbox{constructor}_9,\mbox{negated\_conjecture})$

$d_2 = \mbox{not}(e_2)\qquad\mbox{cnf}(\mbox{constructor}_{10},\mbox{negated\_conjecture})$

$e_1 = \mbox{or}(f_1,f_3)\qquad\mbox{cnf}(\mbox{constructor}_{11},\mbox{negated\_conjecture})$

$e_2 = \mbox{or}(f_2,f_3)\qquad\mbox{cnf}(\mbox{constructor}_{12},\mbox{negated\_conjecture})$

$f_1 = \mbox{not}(i_1)\qquad\mbox{cnf}(\mbox{constructor}_{13},\mbox{negated\_conjecture})$

$f_2 = \mbox{not}(i_2)\qquad\mbox{cnf}(\mbox{constructor}_{14},\mbox{negated\_conjecture})$

$f_3 = \mbox{and}(i_1,i_2)\qquad\mbox{cnf}(\mbox{constructor}_{15},\mbox{negated\_conjecture})$

$\mbox{circuit}(\mbox{input}(i_1,i_2),\mbox{output}(a_1,a_2))\qquad\mbox{cnf}(\mbox{circuit\_description},\mbox{negated\_conjecture})$

$\neg\,\mbox{circuit}(\mbox{input}(i_1,i_2),\mbox{output}(i_2,i_1))\qquad\mbox{cnf}(\mbox{prove\_interchange},\mbox{negated\_conjecture})$

\medskip\textbf{HWV036-2.p} Full-adder.






$\mbox{include}(\mbox{'Axioms/HWV002-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-2.ax'})$

\medskip\textbf{HWV012-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{gt}(\mbox{fifo\_length},\mbox{level}(t_{139}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_Wr\_error}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV008-2.002.p} 2 bit ripple carry adder






$\mbox{include}(\mbox{'Axioms/HWV002-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-2.ax'})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{fulladder}(f_1(x))\qquad\mbox{cnf}(\mbox{nbit\_adder\_fulladder}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{fulladder}(f_2(x))\qquad\mbox{cnf}(\mbox{nbit\_adder\_fulladder}_2,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{connection}(\mbox{out}_1(x),\mbox{out}_1(f_1(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_out1\_out1f}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{connection}(\mbox{out}_2(x),\mbox{out}_1(f_2(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_out2\_out1f}_2,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{connection}(\mbox{outc}(x),\mbox{outc}(f_2(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_outc\_outcf}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{connection}(\mbox{ina}_1(x),\mbox{in}_1(f_1(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_ina1\_in1f}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{connection}(\mbox{inb}_1(x),\mbox{in}_2(f_1(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inb1\_in2f}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{connection}(\mbox{ina}_2(x),\mbox{in}_1(f_2(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_ina2\_in1f}_2,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{connection}(\mbox{inb}_2(x),\mbox{in}_2(f_2(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inb2\_in2f}_2,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{connection}(\mbox{outc}(f_1(x)),\mbox{inc}(f_2(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inc\_incf}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_2(x) \ \Rightarrow \ \mbox{connection}(\mbox{inc}(x),\mbox{inc}(f_1(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inc\_incf}_2,\mbox{axiom})$

$\mbox{nbit\_adder}_2(a)\qquad\mbox{cnf}(\mbox{a\_isa\_2bit\_adder},\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{ina1}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{ina2}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{inb1}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{inb2}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{inc}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{out1}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{out2}_0,\mbox{hypothesis})$

$1\qquad\mbox{cnf}(\mbox{outc}_1,\mbox{hypothesis})$

$\neg\,\mbox{abnormal}(\mbox{or}_1(f_2(a)))\qquad\mbox{cnf}(\mbox{diagnosis\_or1f2a},\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{and}_2(h_1(f_2(a))))\qquad\mbox{cnf}(\mbox{diagnosis\_and2h1f2a},\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{and}_2(h_2(f_2(a))))\qquad\mbox{cnf}(\mbox{diagnosis\_and2h2f2a},\mbox{negated\_conjecture})$

\medskip\textbf{HWV035-2.p} Half-adder.






$\mbox{include}(\mbox{'Axioms/HWV002-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-1.ax'})$

\medskip\textbf{HWV010-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206})\ne n_0\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTempty\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV052-1.001.001.p} Faulty channel 1 1

The problem of sending N bits over a faulty channel that can 
 mutilate any one bit. We can use K extra bits to help us do this.
 Satisfiable means that it is possible, unsatisfiable means that 
 it is not possible.




$x = o\mbox{ or }x = i\qquad\mbox{cnf}(\mbox{bit\_domain},\mbox{axiom})$

$x^{-1}\ne x\qquad\mbox{cnf}(\mbox{bit\_inverse},\mbox{axiom})$

$\mbox{unpack}_1(x_1,\mbox{pack}_1(x_1)) = x_1\qquad\mbox{cnf}(\mbox{unpack}_1,\mbox{axiom})$

$\mbox{unpack}_1(x_1^{-1},\mbox{pack}_1(x_1)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{01},\mbox{axiom})$

$\mbox{unpack}_1(x_1,\mbox{pack}_1(x_1)^{-1}) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{02},\mbox{axiom})$

\medskip\textbf{HWV014-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{gt}(\mbox{level}(x_{139}),n_0)\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Rd}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Wr}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{level}(x_{139} + n_1)\ne -\mbox{level}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV009-4.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV026-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_error\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV019-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{p\_Wr\_error}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},\mbox{level}(t_{139}))\mbox{ or }\mbox{p\_Rd}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV021-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{p\_Rd\_error}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Rd}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Empty}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV019-3.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV010-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{p\_Empty}(t_{139}) \ \Rightarrow \ \mbox{level}(t_{139})\ne n_0\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Empty}(t_{139})\mbox{ or }\mbox{level}(t_{139}) = n_0\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV016-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_LES\_EQU\_}(n_0,\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTempty\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_0)\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV009-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{level}(t_{139} + n_1) = n_0 \ \Rightarrow \ ( \mbox{p\_Wr\_error}(t_{139} + n_1)\mbox{ or }\mbox{p\_Rd\_error}(t_{139} + n_1) )\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV031-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_LES\_EQU\_}(\mbox{f\_ADD\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_level\_}(t_{206}),n_1),\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{f\_ADD\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_level\_}(\mbox{f\_ADD\_}(t_{206},n_1)),n_1),\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV006-2.p} A fulladder built from two halfadders and an or gate






$\mbox{include}(\mbox{'Axioms/HWV002-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-2.ax'})$

$\mbox{fulladder}(f)\qquad\mbox{cnf}(\mbox{f\_isa\_fulladder},\mbox{hypothesis})$

$1\qquad\mbox{cnf}(\mbox{in1}_1,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{in2}_0,\mbox{hypothesis})$

$1\qquad\mbox{cnf}(\mbox{inc}_1,\mbox{hypothesis})$

$1\qquad\mbox{cnf}(\mbox{outs}_1,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{outc}_0,\mbox{hypothesis})$

$\mbox{abnormal}(\mbox{or}_1(f)) \ \Rightarrow \ \neg\,\mbox{abnormal}(\mbox{not}_1(h_2(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_not1h}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{and}_2(h_2(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_and}_2,\mbox{negated\_conjecture})$

$\mbox{abnormal}(\mbox{or}_1(f)) \ \Rightarrow \ \neg\,\mbox{abnormal}(\mbox{and}_1(h_2(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_and1h}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{or}_1(h_1(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_or1h}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{not}_1(h_1(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_not1h}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{and}_2(h_1(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_and2h}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{and}_1(h_1(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_and1h}_1,\mbox{negated\_conjecture})$

\medskip\textbf{HWV015-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{gt}(\mbox{level}(x_{139}),n_0)\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Rd}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_Wr}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{level}(x_{139} + n_1)\ne \mbox{level}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV021-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTempty\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV003-1.p} One bit Full Adder






$\mbox{include}(\mbox{'Axioms/HWC002-0.ax'})$

$\mbox{not}(\mbox{and}(x,y)) = \mbox{or}(\mbox{not}(x),\mbox{not}(y))\qquad\mbox{cnf}(\mbox{demorgan}_1,\mbox{axiom})$

$\mbox{not}(\mbox{or}(x,y)) = \mbox{and}(\mbox{not}(x),\mbox{not}(y))\qquad\mbox{cnf}(\mbox{demorgan}_2,\mbox{axiom})$

$\mbox{not}(\mbox{not}(x)) = x\qquad\mbox{cnf}(\mbox{not\_involution},\mbox{axiom})$

$\mbox{and}(x,y) = \mbox{and}(y,x)\qquad\mbox{cnf}(\mbox{and\_symmetry},\mbox{negated\_conjecture})$

$\mbox{or}(x,y) = \mbox{or}(y,x)\qquad\mbox{cnf}(\mbox{or\_symmetry},\mbox{negated\_conjecture})$

$\mbox{and}(\mbox{or}(x,y),z) = \mbox{or}(\mbox{and}(x,z),\mbox{and}(y,z))\qquad\mbox{cnf}(\mbox{and\_or\_simplification},\mbox{negated\_conjecture})$

$\mbox{and}(\mbox{and}(x,y),z) = \mbox{and}(\mbox{and}(x,z),y)\qquad\mbox{cnf}(\mbox{and\_commutativity},\mbox{negated\_conjecture})$

$\mbox{or}(\mbox{or}(x,y),z) = \mbox{or}(\mbox{or}(x,z),y)\qquad\mbox{cnf}(\mbox{or\_commutativity},\mbox{negated\_conjecture})$

$\mbox{and}(x,\mbox{not}(x)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_1,\mbox{axiom})$

$\mbox{or}(x,\mbox{not}(x)) = n_1\qquad\mbox{cnf}(\mbox{or\_not\_evaluation}_1,\mbox{axiom})$

$\mbox{and}(x,x) = x\qquad\mbox{cnf}(\mbox{and\_idempotency},\mbox{axiom})$

$\mbox{or}(x,x) = x\qquad\mbox{cnf}(\mbox{or\_idempotency},\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),\mbox{not}(y)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_2,\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),\mbox{not}(x)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_3,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),\mbox{not}(y)) = n_1\qquad\mbox{cnf}(\mbox{or\_not\_evaluation}_2,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),\mbox{not}(x)) = n_1\qquad\mbox{cnf}(\mbox{or\_not\_evaluation}_3,\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),y) = \mbox{and}(x,y)\qquad\mbox{cnf}(\mbox{and\_evaluation}_1,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),y) = \mbox{or}(x,y)\qquad\mbox{cnf}(\mbox{or\_evaluation}_1,\mbox{axiom})$

$\mbox{and}(\mbox{and}(\mbox{and}(x_1,x_2),x_3),\mbox{not}(x_1)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_4,\mbox{axiom})$

$\mbox{and}(\mbox{and}(\mbox{and}(x_1,x_2),x_3),\mbox{not}(x_2)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_5,\mbox{axiom})$

$\mbox{or}(\mbox{and}(x,y),y) = y\qquad\mbox{cnf}(\mbox{and\_or\_subsumption}_1,\mbox{axiom})$

$\mbox{or}(\mbox{and}(x,y),x) = x\qquad\mbox{cnf}(\mbox{and\_or\_subsumption}_2,\mbox{axiom})$

$\mbox{or}(\mbox{or}(\mbox{and}(x,y),z),y) = \mbox{or}(z,y)\qquad\mbox{cnf}(\mbox{and\_or\_subsumption}_3,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,\mbox{and}(y,z)),z) = \mbox{or}(x,z)\qquad\mbox{cnf}(\mbox{and\_or\_subsumption}_4,\mbox{axiom})$

$\mbox{or}(\mbox{and}(x,\mbox{not}(y)),y) = \mbox{or}(x,y)\qquad\mbox{cnf}(\mbox{karnaugh}_1,\mbox{axiom})$

$\mbox{or}(\mbox{and}(\mbox{not}(x),\mbox{not}(y)),y) = \mbox{or}(y,\mbox{not}(x))\qquad\mbox{cnf}(\mbox{karnaugh}_2,\mbox{axiom})$

$\mbox{or}(\mbox{and}(\mbox{and}(x,y),\mbox{not}(z)),\mbox{and}(x,z)) = \mbox{or}(\mbox{and}(x,y),\mbox{and}(x,z))\qquad\mbox{cnf}(\mbox{karnaugh}_3,\mbox{axiom})$

$\mbox{xor}(x,y) = \mbox{or}(\mbox{and}(x,\mbox{not}(y)),\mbox{and}(y,\mbox{not}(x)))\qquad\mbox{cnf}(\mbox{xor\_definition},\mbox{axiom})$

$\mbox{carryout}(x,y,z) = \mbox{or}(\mbox{and}(x,\mbox{or}(y,z)),\mbox{and}(\mbox{not}(x),\mbox{and}(y,z)))\qquad\mbox{cnf}(\mbox{carryout\_definition},\mbox{negated\_conjecture})$

$x + y{=}z = \mbox{xor}(\mbox{xor}(x,y),z)\qquad\mbox{cnf}(\mbox{sum\_definition},\mbox{negated\_conjecture})$

$a_{11} = \mbox{not}(\mbox{and}(a,b))\qquad\mbox{cnf}(\mbox{circuit}_1,\mbox{negated\_conjecture})$

$a_{12} = \mbox{not}(\mbox{and}(a_{11},a))\qquad\mbox{cnf}(\mbox{circuit}_2,\mbox{negated\_conjecture})$

$a_{13} = \mbox{not}(\mbox{and}(a_{11},b))\qquad\mbox{cnf}(\mbox{circuit}_3,\mbox{negated\_conjecture})$

$a_{14} = \mbox{not}(\mbox{and}(a_{12},a_{13}))\qquad\mbox{cnf}(\mbox{circuit}_4,\mbox{negated\_conjecture})$

$a_{15} = \mbox{not}(\mbox{and}(a_{14},\mbox{carryin}))\qquad\mbox{cnf}(\mbox{circuit}_5,\mbox{negated\_conjecture})$

$a_{16} = \mbox{not}(\mbox{and}(a_{14},a_{15}))\qquad\mbox{cnf}(\mbox{circuit}_6,\mbox{negated\_conjecture})$

$a_{17} = \mbox{not}(\mbox{and}(a_{15},\mbox{carryin}))\qquad\mbox{cnf}(\mbox{circuit}_7,\mbox{negated\_conjecture})$

$s_1 = \mbox{not}(\mbox{and}(a_{16},a_{17}))\qquad\mbox{cnf}(\mbox{circuit}_8,\mbox{negated\_conjecture})$

$c_1 = \mbox{not}(\mbox{and}(a_{11},a_{15}))\qquad\mbox{cnf}(\mbox{circuit}_9,\mbox{negated\_conjecture})$

$\mbox{circuit}(s_1,c_1)\qquad\mbox{cnf}(\mbox{the\_output\_circuit},\mbox{negated\_conjecture})$

$\neg\,\mbox{circuit}(a + b{=}\mbox{carryin},\mbox{carryout}(a,b,\mbox{carryin}))\qquad\mbox{cnf}(\mbox{prove\_circuit},\mbox{negated\_conjecture})$

\medskip\textbf{HWV029-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{gt}(\mbox{level}(x_{139}),\mbox{fifo\_length})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{level}(x_{139} + n_1),\mbox{fifo\_length})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV022-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{level}(t_{139}) + n_1 = \mbox{fifo\_length}\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Rd}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{level}(t_{139} + n_1)\ne \mbox{fifo\_length}\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV012-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV052-1.001.002.p} Faulty channel 1 2

The problem of sending N bits over a faulty channel that can
 mutilate any one bit. We can use K extra bits to help us do this.
 Satisfiable means that it is possible, unsatisfiable means that
 it is not possible.




$x = o\mbox{ or }x = i\qquad\mbox{cnf}(\mbox{bit\_domain},\mbox{axiom})$

$x^{-1}\ne x\qquad\mbox{cnf}(\mbox{bit\_inverse},\mbox{axiom})$

$\mbox{unpack}_1(x_1,\mbox{pack}_1(x_1),\mbox{pack}_2(x_1)) = x_1\qquad\mbox{cnf}(\mbox{unpack}_1,\mbox{axiom})$

$\mbox{unpack}_1(x_1^{-1},\mbox{pack}_1(x_1),\mbox{pack}_2(x_1)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{01},\mbox{axiom})$

$\mbox{unpack}_1(x_1,\mbox{pack}_1(x_1)^{-1},\mbox{pack}_2(x_1)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{02},\mbox{axiom})$

$\mbox{unpack}_1(x_1,\mbox{pack}_1(x_1),\mbox{pack}_2(x_1)^{-1}) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{03},\mbox{axiom})$

\medskip\textbf{HWV033-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{gt}(\mbox{rd\_level}(t_{139}),-\mbox{fifo\_length})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{rd\_level}(t_{139} + n_1),-\mbox{fifo\_length})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV033-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_level\_}(t_{206}),\mbox{f\_SUB\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_1))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_level\_}(\mbox{f\_ADD\_}(t_{206},n_1)),\mbox{f\_SUB\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_1))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV034-2.p} Connections, faults, and gates.






$\mbox{include}(\mbox{'Axioms/HWV002-0.ax'})$

\medskip\textbf{HWV018-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{p\_Rd}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_Full}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{p\_Full}(t_{139} + n_1) \ \Rightarrow \ \neg\,\mbox{p\_Wr\_error}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV003-2.p} One bit Full Adder

Prove that the given implementation of a one-bit full adder
 using only NAND gates is correct




$\mbox{or}(x,y) = \mbox{or}(y,x)\qquad\mbox{cnf}(\mbox{or\_commutative},\mbox{axiom})$

$\mbox{and}(x,y) = \mbox{and}(y,x)\qquad\mbox{cnf}(\mbox{and\_commutative},\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),z) = \mbox{or}(x,\mbox{or}(y,z))\qquad\mbox{cnf}(\mbox{or\_associative},\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),z) = \mbox{and}(x,\mbox{and}(y,z))\qquad\mbox{cnf}(\mbox{and\_associative},\mbox{axiom})$

$\mbox{or}(x,\mbox{ll}_0) = x\qquad\mbox{cnf}(\mbox{or\_identity},\mbox{axiom})$

$\mbox{and}(x,\mbox{ll}_1) = x\qquad\mbox{cnf}(\mbox{and\_identity},\mbox{axiom})$

$\mbox{and}(x,\mbox{or}(y,z)) = \mbox{or}(\mbox{and}(x,y),\mbox{and}(x,z))\qquad\mbox{cnf}(\mbox{or\_distributive},\mbox{axiom})$

$\mbox{or}(x,\mbox{and}(y,z)) = \mbox{and}(\mbox{or}(x,y),\mbox{or}(x,z))\qquad\mbox{cnf}(\mbox{and\_distributive},\mbox{axiom})$

$\mbox{or}(x,\mbox{not}(x)) = \mbox{ll}_1\qquad\mbox{cnf}(\mbox{or\_complement},\mbox{axiom})$

$\mbox{and}(x,\mbox{not}(x)) = \mbox{ll}_0\qquad\mbox{cnf}(\mbox{and\_complement},\mbox{axiom})$

$\mbox{or}(x,x) = x\qquad\mbox{cnf}(\mbox{or\_idempotent},\mbox{axiom})$

$\mbox{and}(x,x) = x\qquad\mbox{cnf}(\mbox{and\_idempotent},\mbox{axiom})$

$\mbox{not}(\mbox{not}(x)) = x\qquad\mbox{cnf}(\mbox{not\_involution},\mbox{axiom})$

$\mbox{not}(\mbox{ll}_0) = \mbox{ll}_1\qquad\mbox{cnf}(\mbox{ll0\_inverse},\mbox{axiom})$

$\mbox{not}(\mbox{ll}_1) = \mbox{ll}_0\qquad\mbox{cnf}(\mbox{ll1\_inverse},\mbox{axiom})$

$\mbox{or}(x,\mbox{ll}_1) = \mbox{ll}_1\qquad\mbox{cnf}(\mbox{or\_boundedness},\mbox{axiom})$

$\mbox{and}(x,\mbox{ll}_0) = \mbox{ll}_0\qquad\mbox{cnf}(\mbox{and\_boundedness},\mbox{axiom})$

$\mbox{or}(x,\mbox{and}(x,y)) = x\qquad\mbox{cnf}(\mbox{or\_absorption},\mbox{axiom})$

$\mbox{and}(x,\mbox{or}(x,y)) = x\qquad\mbox{cnf}(\mbox{and\_absorption},\mbox{axiom})$

$\mbox{not}(\mbox{or}(x,y)) = \mbox{and}(\mbox{not}(x),\mbox{not}(y))\qquad\mbox{cnf}(\mbox{or\_demorgan},\mbox{axiom})$

$\mbox{not}(\mbox{and}(x,y)) = \mbox{or}(\mbox{not}(x),\mbox{not}(y))\qquad\mbox{cnf}(\mbox{and\_demorgan},\mbox{axiom})$

$\mbox{or}(\mbox{and}(\mbox{not}(x),y),\mbox{and}(x,\mbox{not}(y))) = \mbox{xor}(x,y)\qquad\mbox{cnf}(\mbox{xor\_definition},\mbox{axiom})$

$\mbox{xor}(x,y) = \mbox{xor}(y,x)\qquad\mbox{cnf}(\mbox{xor\_commutative},\mbox{axiom})$

$\mbox{xor}(x,\mbox{xor}(y,z)) = \mbox{xor}(\mbox{xor}(x,y),z)\qquad\mbox{cnf}(\mbox{xor\_associative},\mbox{axiom})$

$\mbox{xor}(\mbox{xor}(a,b),\mbox{cin}) = \mbox{sum\_def}\qquad\mbox{cnf}(\mbox{sum\_def},\mbox{negated\_conjecture})$

$\mbox{or}(\mbox{and}(\mbox{cin},\mbox{or}(a,b)),\mbox{and}(\mbox{not}(\mbox{cin}),\mbox{and}(a,b))) = \mbox{carry\_def}\qquad\mbox{cnf}(\mbox{carry\_def},\mbox{negated\_conjecture})$

$\mbox{not}(\mbox{and}(a,b)) = t_1\qquad\mbox{cnf}(t_1,\mbox{negated\_conjecture})$

$\mbox{not}(\mbox{and}(a,t_1)) = t_2\qquad\mbox{cnf}(t_2,\mbox{negated\_conjecture})$

$\mbox{not}(\mbox{and}(b,t_1)) = t_3\qquad\mbox{cnf}(t_3,\mbox{negated\_conjecture})$

$\mbox{not}(\mbox{and}(t_2,t_3)) = t_4\qquad\mbox{cnf}(t_4,\mbox{negated\_conjecture})$

$\mbox{not}(\mbox{and}(t_4,\mbox{cin})) = t_5\qquad\mbox{cnf}(t_5,\mbox{negated\_conjecture})$

$\mbox{not}(\mbox{and}(t_4,t_5)) = t_6\qquad\mbox{cnf}(t_6,\mbox{negated\_conjecture})$

$\mbox{not}(\mbox{and}(t_5,\mbox{cin})) = t_7\qquad\mbox{cnf}(t_7,\mbox{negated\_conjecture})$

$\mbox{not}(\mbox{and}(t_6,t_7)) =  + \qquad\mbox{cnf}(\mbox{sum},\mbox{negated\_conjecture})$

$\mbox{not}(\mbox{and}(t_1,t_5)) = \mbox{carry}\qquad\mbox{cnf}(\mbox{carry},\mbox{negated\_conjecture})$

$ +  = \mbox{sum\_def} \ \Rightarrow \ \mbox{carry}\ne \mbox{carry\_def}\qquad\mbox{cnf}(\mbox{prove\_circuit},\mbox{negated\_conjecture})$

\medskip\textbf{HWV019-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV023-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{level}(t_{139}) = n_1\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_Rd}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Empty}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV026-3.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_error\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV032-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_level\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV026-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_Wr\_error}(t_{139}) \ \Rightarrow \ \neg\,\mbox{p\_Wr\_error}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_Wr\_error}(t_{139})\mbox{ or }\mbox{p\_Wr\_error}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV030-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{gt}(\mbox{fifo\_length},\mbox{wr\_level}(t_{139} + n_1))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV008-2.001.p} 1 bit ripple carry adder






$\mbox{include}(\mbox{'Axioms/HWV002-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-2.ax'})$

$\mbox{nbit\_adder}_1(x) \ \Rightarrow \ \mbox{fulladder}(f_1(x))\qquad\mbox{cnf}(\mbox{nbit\_adder\_fulladder}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_1(x) \ \Rightarrow \ \mbox{connection}(\mbox{out}_1(x),\mbox{outs}(f_1(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_out1\_out1f}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_1(x) \ \Rightarrow \ \mbox{connection}(\mbox{outc}(x),\mbox{outc}(f_1(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_outc\_outcf}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_1(x) \ \Rightarrow \ \mbox{connection}(\mbox{ina}_1(x),\mbox{in}_1(f_1(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_ina1\_in1f}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_1(x) \ \Rightarrow \ \mbox{connection}(\mbox{inb}_1(x),\mbox{in}_2(f_1(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inb1\_in2f}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_1(x) \ \Rightarrow \ \mbox{connection}(\mbox{inc}(x),\mbox{inc}(f_1(x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inc\_incf}_1,\mbox{axiom})$

$\mbox{nbit\_adder}_1(a)\qquad\mbox{cnf}(\mbox{a\_isa\_1bit\_adder},\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{ina1}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{inb1}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{inc}_0,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{out1}_0,\mbox{hypothesis})$

$1\qquad\mbox{cnf}(\mbox{outc}_0,\mbox{hypothesis})$

$\neg\,\mbox{abnormal}(\mbox{or}_1(f_1(a)))\qquad\mbox{cnf}(\mbox{diagnosis\_or1f}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{and}_2(h_1(f_1(a))))\qquad\mbox{cnf}(\mbox{diagnosis\_and2h1f}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{abnormal}(\mbox{and}_2(h_2(f_1(a))))\qquad\mbox{cnf}(\mbox{diagnosis\_and2h2f}_1,\mbox{negated\_conjecture})$

\medskip\textbf{HWV052-1.003.003.p} Faulty channel 3 3

The problem of sending N bits over a faulty channel that can
 mutilate any one bit. We can use K extra bits to help us do this.
 Satisfiable means that it is possible, unsatisfiable means that
 it is not possible.




$x = o\mbox{ or }x = i\qquad\mbox{cnf}(\mbox{bit\_domain},\mbox{axiom})$

$x^{-1}\ne x\qquad\mbox{cnf}(\mbox{bit\_inverse},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_1\qquad\mbox{cnf}(\mbox{unpack}_1,\mbox{axiom})$

$\mbox{unpack}_1(x_1^{-1},x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{01},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2^{-1},x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{02},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,x_3^{-1},\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{03},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3)^{-1},\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{04},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3)^{-1},\mbox{pack}_3(x_1,x_2,x_3)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{05},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)^{-1}) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{06},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_2\qquad\mbox{cnf}(\mbox{unpack}_2,\mbox{axiom})$

$\mbox{unpack}_2(x_1^{-1},x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{07},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2^{-1},x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{08},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,x_3^{-1},\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{09},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3)^{-1},\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{10},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3)^{-1},\mbox{pack}_3(x_1,x_2,x_3)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{11},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)^{-1}) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{12},\mbox{axiom})$

$\mbox{unpack}_3(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_3\qquad\mbox{cnf}(\mbox{unpack}_3,\mbox{axiom})$

$\mbox{unpack}_3(x_1^{-1},x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_3\qquad\mbox{cnf}(\mbox{unpack3}_{13},\mbox{axiom})$

$\mbox{unpack}_3(x_1,x_2^{-1},x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_3\qquad\mbox{cnf}(\mbox{unpack3}_{14},\mbox{axiom})$

$\mbox{unpack}_3(x_1,x_2,x_3^{-1},\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_3\qquad\mbox{cnf}(\mbox{unpack3}_{15},\mbox{axiom})$

$\mbox{unpack}_3(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3)^{-1},\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)) = x_3\qquad\mbox{cnf}(\mbox{unpack3}_{16},\mbox{axiom})$

$\mbox{unpack}_3(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3)^{-1},\mbox{pack}_3(x_1,x_2,x_3)) = x_3\qquad\mbox{cnf}(\mbox{unpack3}_{17},\mbox{axiom})$

$\mbox{unpack}_3(x_1,x_2,x_3,\mbox{pack}_1(x_1,x_2,x_3),\mbox{pack}_2(x_1,x_2,x_3),\mbox{pack}_3(x_1,x_2,x_3)^{-1}) = x_3\qquad\mbox{cnf}(\mbox{unpack3}_{18},\mbox{axiom})$

\medskip\textbf{HWV006-1.p} A fulladder built from two halfadders and an or gate






$\mbox{include}(\mbox{'Axioms/HWV001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-2.ax'})$

$\mbox{type}(f,\mbox{fulladder})\qquad\mbox{cnf}(\mbox{f\_isa\_fulladder},\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(n_1,f),n_1)\qquad\mbox{cnf}(\mbox{in1}_1,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(n_2,f),n_0)\qquad\mbox{cnf}(\mbox{in2}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(c,f),n_1)\qquad\mbox{cnf}(\mbox{inc}_1,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(s,f),n_1)\qquad\mbox{cnf}(\mbox{outs}_1,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(c,f),n_0)\qquad\mbox{cnf}(\mbox{outc}_0,\mbox{hypothesis})$

$\mbox{mode}(\mbox{or}_1(f),\mbox{abnormal}) \ \Rightarrow \ \neg\,\mbox{mode}(\mbox{not}_1(h_2(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_not1h}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{and}_2(h_2(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_and}_2,\mbox{negated\_conjecture})$

$\mbox{mode}(\mbox{or}_1(f),\mbox{abnormal}) \ \Rightarrow \ \neg\,\mbox{mode}(\mbox{and}_1(h_2(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_and1h}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{or}_1(h_1(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or1h}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{not}_1(h_1(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_not1h}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{and}_2(h_1(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_and2h}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{and}_1(h_1(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_and1h}_1,\mbox{negated\_conjecture})$

\medskip\textbf{HWV025-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_error\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV037-1.p} Axioms from a VHDL design description






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

\medskip\textbf{HWV025-3.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_error\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV005-1.p} A halfadder built from and, or and not gates






$\mbox{include}(\mbox{'Axioms/HWV001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-1.ax'})$

$\mbox{type}(h,\mbox{halfadder})\qquad\mbox{cnf}(\mbox{h\_isa\_halfadder},\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(n_1,h),n_1)\qquad\mbox{cnf}(\mbox{in1}_1,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(n_2,h),n_0)\qquad\mbox{cnf}(\mbox{in2}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(s,h),n_0)\qquad\mbox{cnf}(\mbox{outs}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(c,h),n_0)\qquad\mbox{cnf}(\mbox{outc}_0,\mbox{hypothesis})$

$\neg\,\mbox{mode}(\mbox{and}_1(h),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_and}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{not}_1(h),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_not}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{or}_1(h),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or}_1,\mbox{negated\_conjecture})$

\medskip\textbf{HWV028-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(\mbox{f\_ADD\_}(t_{206},n_1)),\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV018-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfull\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfull\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV052-1.002.003.p} Faulty channel 2 3

The problem of sending N bits over a faulty channel that can
 mutilate any one bit. We can use K extra bits to help us do this.
 Satisfiable means that it is possible, unsatisfiable means that
 it is not possible.




$x = o\mbox{ or }x = i\qquad\mbox{cnf}(\mbox{bit\_domain},\mbox{axiom})$

$x^{-1}\ne x\qquad\mbox{cnf}(\mbox{bit\_inverse},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack}_1,\mbox{axiom})$

$\mbox{unpack}_1(x_1^{-1},x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{01},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2^{-1},\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{02},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,\mbox{pack}_1(x_1,x_2)^{-1},\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{03},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)^{-1},\mbox{pack}_3(x_1,x_2)) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{04},\mbox{axiom})$

$\mbox{unpack}_1(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)^{-1}) = x_1\qquad\mbox{cnf}(\mbox{unpack1}_{05},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack}_2,\mbox{axiom})$

$\mbox{unpack}_2(x_1^{-1},x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{06},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2^{-1},\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{07},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,\mbox{pack}_1(x_1,x_2)^{-1},\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{08},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2)^{-1},\mbox{pack}_3(x_1,x_2)) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{09},\mbox{axiom})$

$\mbox{unpack}_2(x_1,x_2,\mbox{pack}_1(x_1,x_2),\mbox{pack}_2(x_1,x_2),\mbox{pack}_3(x_1,x_2)^{-1}) = x_2\qquad\mbox{cnf}(\mbox{unpack2}_{10},\mbox{axiom})$

\medskip\textbf{HWV034-1.p} Connections, faults, and gates.






$\mbox{include}(\mbox{'Axioms/HWV001-0.ax'})$

\medskip\textbf{HWV009-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(\mbox{f\_ADD\_}(t_{206},n_1))\ne n_0\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV018-3.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfull\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV007-2.p} A fulladder built from two halfadders and an or gate






$\mbox{include}(\mbox{'Axioms/HWV002-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV002-2.ax'})$

$\mbox{fulladder}(f)\qquad\mbox{cnf}(\mbox{f\_isa\_fulladder},\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{in1}_1,\mbox{hypothesis})$

$1\qquad\mbox{cnf}(\mbox{in2}_0,\mbox{hypothesis})$

$1\qquad\mbox{cnf}(\mbox{inc}_1,\mbox{hypothesis})$

$1\qquad\mbox{cnf}(\mbox{outs}_1,\mbox{hypothesis})$

$0\qquad\mbox{cnf}(\mbox{outc}_0,\mbox{hypothesis})$

$\neg\,\mbox{abnormal}(\mbox{and}_2(h_1(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_and2h}_1,\mbox{negated\_conjecture})$

$\mbox{abnormal}(\mbox{or}_1(f)) \ \Rightarrow \ \neg\,\mbox{abnormal}(\mbox{and}_1(h_1(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_and1h}_1,\mbox{negated\_conjecture})$

$\mbox{abnormal}(\mbox{or}_1(f)) \ \Rightarrow \ \neg\,\mbox{abnormal}(\mbox{not}_1(h_1(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_not1h}_1,\mbox{negated\_conjecture})$

$\mbox{abnormal}(\mbox{or}_1(f)) \ \Rightarrow \ \neg\,\mbox{abnormal}(\mbox{and}_1(h_2(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_and1h}_2,\mbox{negated\_conjecture})$

$\mbox{abnormal}(\mbox{or}_1(f)) \ \Rightarrow \ \neg\,\mbox{abnormal}(\mbox{or}_1(h_2(f)))\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_or1h}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV031-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{gt}(\mbox{wr\_level}(x_{139}) + n_1,\mbox{fifo\_length})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{wr\_level}(x_{139} + n_1) + n_1,\mbox{fifo\_length})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV030-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_level\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV020-3.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTempty\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV015-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}),n_0)\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(\mbox{f\_ADD\_}(t_{206},n_1))\ne \mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206})\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV027-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206})\ne \mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(\mbox{f\_ADD\_}(t_{206},n_1))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV023-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}) = n_1\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTempty\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV029-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}),\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(\mbox{f\_ADD\_}(t_{206},n_1)),\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV032-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{gt}(\mbox{fifo\_length},\mbox{rd\_level}(t_{139} + n_1))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},n_0)\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

\medskip\textbf{HWV004-1.p} Two bit Full Adder






$\mbox{include}(\mbox{'Axioms/HWC002-0.ax'})$

$\mbox{not}(\mbox{and}(x,y)) = \mbox{or}(\mbox{not}(x),\mbox{not}(y))\qquad\mbox{cnf}(\mbox{demorgan}_1,\mbox{axiom})$

$\mbox{not}(\mbox{or}(x,y)) = \mbox{and}(\mbox{not}(x),\mbox{not}(y))\qquad\mbox{cnf}(\mbox{demorgan}_2,\mbox{axiom})$

$\mbox{not}(\mbox{not}(x)) = x\qquad\mbox{cnf}(\mbox{not\_involution},\mbox{axiom})$

$\mbox{and}(x,y) = \mbox{and}(y,x)\qquad\mbox{cnf}(\mbox{and\_symmetry},\mbox{negated\_conjecture})$

$\mbox{or}(x,y) = \mbox{or}(y,x)\qquad\mbox{cnf}(\mbox{or\_symmetry},\mbox{negated\_conjecture})$

$\mbox{and}(\mbox{or}(x,y),z) = \mbox{or}(\mbox{and}(x,z),\mbox{and}(y,z))\qquad\mbox{cnf}(\mbox{and\_or\_simplification},\mbox{negated\_conjecture})$

$\mbox{and}(\mbox{and}(x,y),z) = \mbox{and}(\mbox{and}(x,z),y)\qquad\mbox{cnf}(\mbox{and\_commutativity},\mbox{negated\_conjecture})$

$\mbox{or}(\mbox{or}(x,y),z) = \mbox{or}(\mbox{or}(x,z),y)\qquad\mbox{cnf}(\mbox{or\_commutativity},\mbox{negated\_conjecture})$

$\mbox{and}(x,\mbox{not}(x)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_1,\mbox{axiom})$

$\mbox{or}(x,\mbox{not}(x)) = n_1\qquad\mbox{cnf}(\mbox{or\_not\_evaluation}_1,\mbox{axiom})$

$\mbox{and}(x,x) = x\qquad\mbox{cnf}(\mbox{and\_idempotency},\mbox{axiom})$

$\mbox{or}(x,x) = x\qquad\mbox{cnf}(\mbox{or\_idempotency},\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),\mbox{not}(y)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_2,\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),\mbox{not}(x)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_3,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),\mbox{not}(y)) = n_1\qquad\mbox{cnf}(\mbox{or\_not\_evaluation}_2,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),\mbox{not}(x)) = n_1\qquad\mbox{cnf}(\mbox{or\_not\_evaluation}_3,\mbox{axiom})$

$\mbox{and}(\mbox{and}(x,y),y) = \mbox{and}(x,y)\qquad\mbox{cnf}(\mbox{and\_evaluation}_1,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,y),y) = \mbox{or}(x,y)\qquad\mbox{cnf}(\mbox{or\_evaluation}_1,\mbox{axiom})$

$\mbox{and}(\mbox{and}(\mbox{and}(x_1,x_2),x_3),\mbox{not}(x_1)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_4,\mbox{axiom})$

$\mbox{and}(\mbox{and}(\mbox{and}(x_1,x_2),x_3),\mbox{not}(x_2)) = n_0\qquad\mbox{cnf}(\mbox{and\_not\_evaluation}_5,\mbox{axiom})$

$\mbox{or}(\mbox{and}(x,y),y) = y\qquad\mbox{cnf}(\mbox{and\_or\_subsumption}_1,\mbox{axiom})$

$\mbox{or}(\mbox{and}(x,y),x) = x\qquad\mbox{cnf}(\mbox{and\_or\_subsumption}_2,\mbox{axiom})$

$\mbox{or}(\mbox{or}(\mbox{and}(x,y),z),y) = \mbox{or}(z,y)\qquad\mbox{cnf}(\mbox{and\_or\_subsumption}_3,\mbox{axiom})$

$\mbox{or}(\mbox{or}(x,\mbox{and}(y,z)),z) = \mbox{or}(x,z)\qquad\mbox{cnf}(\mbox{and\_or\_subsumption}_4,\mbox{axiom})$

$\mbox{or}(\mbox{and}(x,\mbox{not}(y)),y) = \mbox{or}(x,y)\qquad\mbox{cnf}(\mbox{karnaugh}_1,\mbox{axiom})$

$\mbox{or}(\mbox{and}(\mbox{not}(x),\mbox{not}(y)),y) = \mbox{or}(y,\mbox{not}(x))\qquad\mbox{cnf}(\mbox{karnaugh}_2,\mbox{axiom})$

$\mbox{or}(\mbox{and}(\mbox{and}(x,y),\mbox{not}(z)),\mbox{and}(x,z)) = \mbox{or}(\mbox{and}(x,y),\mbox{and}(x,z))\qquad\mbox{cnf}(\mbox{karnaugh}_3,\mbox{axiom})$

$\mbox{xor}(x,y) = \mbox{or}(\mbox{and}(x,\mbox{not}(y)),\mbox{and}(y,\mbox{not}(x)))\qquad\mbox{cnf}(\mbox{xor\_definition},\mbox{axiom})$

$\mbox{carryout}(x,y,z) = \mbox{or}(\mbox{and}(x,\mbox{or}(y,z)),\mbox{and}(\mbox{not}(x),\mbox{and}(y,z)))\qquad\mbox{cnf}(\mbox{carryout\_definition},\mbox{negated\_conjecture})$

$x + y{=}z = \mbox{xor}(\mbox{xor}(x,y),z)\qquad\mbox{cnf}(\mbox{sum\_definition},\mbox{negated\_conjecture})$

$s_0 = a_0 + b_0{=}n_0\qquad\mbox{cnf}(\mbox{s0\_definition},\mbox{negated\_conjecture})$

$s_1 = a_1 + b_1{=}\mbox{carryout}(a_0,b_0,n_0)\qquad\mbox{cnf}(\mbox{s1\_definition},\mbox{negated\_conjecture})$

$\mbox{overflow} = \mbox{carryout}(a_1,b_1,\mbox{carryout}(a_0,b_0,n_0))\qquad\mbox{cnf}(\mbox{overflow\_definition},\mbox{negated\_conjecture})$

$\mbox{circuit}(s_0,s_1,\mbox{overflow})\qquad\mbox{cnf}(\mbox{the\_output\_circuit},\mbox{negated\_conjecture})$

$\neg\,\mbox{circuit}(\mbox{xor}(a_0,b_0),\mbox{xor}(\mbox{xor}(a_1,b_1),\mbox{carryout}(a_0,b_0,n_0)),\mbox{or}(\mbox{and}(a_1,b_1),\mbox{and}(\mbox{and}(a_0,b_0),\mbox{or}(a_1,b_1))))\qquad\mbox{cnf}(\mbox{prove\_circuit},\mbox{negated\_conjecture})$

\medskip\textbf{HWV022-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{f\_ADD\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}),n_1) = \mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_}\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(\mbox{f\_ADD\_}(t_{206},n_1))\ne \mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_}\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV013-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{p\_Reset}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},\mbox{level}(x_{139}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Rd}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_Wr}(x_{139})\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{level}(x_{139} + n_1)\ne \mbox{level}(x_{139}) + n_1\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV027-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Rd}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{level}(t_{139})\ne \mbox{level}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

\medskip\textbf{HWV008-1.001.p} 1 bit ripple carry adder






$\mbox{include}(\mbox{'Axioms/HWV001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-2.ax'})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_1)) \ \Rightarrow \ \mbox{type}(v(n_1,x),\mbox{fulladder})\qquad\mbox{cnf}(\mbox{nbit\_adder\_fulladder}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_1)) \ \Rightarrow \ \mbox{connection}(\mbox{out}(n_1,x),\mbox{out}(s,v(n_1,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_out1\_out1v}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_1)) \ \Rightarrow \ \mbox{connection}(\mbox{out}(c,x),\mbox{out}(c,v(n_1,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_outc\_outcv}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_1)) \ \Rightarrow \ \mbox{connection}(\mbox{in}(a_1,x),\mbox{in}(n_1,v(n_1,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_ina1\_in1v}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_1)) \ \Rightarrow \ \mbox{connection}(\mbox{in}(b_1,x),\mbox{in}(n_2,v(n_1,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inb1\_in2v}_1,\mbox{axiom})$

$\mbox{type}(x,\mbox{nbit\_adder}(n_1)) \ \Rightarrow \ \mbox{connection}(\mbox{in}(c,x),\mbox{in}(c,v(n_1,x)))\qquad\mbox{cnf}(\mbox{nbit\_adder\_connection\_inc\_incv}_1,\mbox{axiom})$

$\mbox{type}(a,\mbox{nbit\_adder}(n_1))\qquad\mbox{cnf}(\mbox{a\_isa\_1bit\_adder},\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(a_1,a),n_0)\qquad\mbox{cnf}(\mbox{ina1}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(b_1,a),n_0)\qquad\mbox{cnf}(\mbox{inb1}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(c,a),n_0)\qquad\mbox{cnf}(\mbox{inc}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(n_1,a),n_0)\qquad\mbox{cnf}(\mbox{out1}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(c,a),n_1)\qquad\mbox{cnf}(\mbox{outc}_0,\mbox{hypothesis})$

$\neg\,\mbox{mode}(\mbox{or}_1(v(n_1,a)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or1v}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{and}_2(h_1(v(n_1,a))),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_and2h1v}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{mode}(\mbox{and}_2(h_2(v(n_1,a))),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_and2h2v}_1,\mbox{negated\_conjecture})$

\medskip\textbf{HWV036-1.p} Full-adder.






$\mbox{include}(\mbox{'Axioms/HWV001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-2.ax'})$

\medskip\textbf{HWV024-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_LES\_EQU\_}(n_0,x_{207})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_LES\_EQU\_}(x_{207},\mbox{f\_SUB\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_width\_},n_1))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{f\_\_index\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTdata\_\_out\_}(\mbox{f\_ADD\_}(t_{206},n_1)),\mbox{f\_SUB\_}(\mbox{f\_SUB\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_width\_},n_1),x_{207}))\ne \mbox{f\_\_index\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTdata\_\_out\_}(t_{206}),\mbox{f\_SUB\_}(\mbox{f\_SUB\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_width\_},n_1),x_{207}))\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV013-2.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTrd\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_LES\_EQU\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTfifo\_\_length\_},\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(\mbox{f\_ADD\_}(t_{206},n_1))\ne \mbox{f\_ADD\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTlevel\_}(t_{206}),n_1)\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV038-1.p} Axioms from a VHDL design description






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

\medskip\textbf{HWV035-1.p} Half-adder.






$\mbox{include}(\mbox{'Axioms/HWV001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-1.ax'})$

\medskip\textbf{HWV016-1.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV003-0.ax'})$

$\neg\,\mbox{gt}(n_0,\mbox{level}(t_{139}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_Wr}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

$\neg\,\mbox{p\_Reset}(t_{139})\qquad\mbox{cnf}(\mbox{quest}_3,\mbox{negated\_conjecture})$

$\mbox{p\_Empty}(t_{139} + n_1)\qquad\mbox{cnf}(\mbox{quest}_4,\mbox{negated\_conjecture})$

$\mbox{gt}(\mbox{fifo\_length},n_0)\qquad\mbox{cnf}(\mbox{quest}_5,\mbox{negated\_conjecture})$

\medskip\textbf{HWV007-1.p} A fulladder built from two halfadders and an or gate






$\mbox{include}(\mbox{'Axioms/HWV001-0.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-1.ax'})$

$\mbox{include}(\mbox{'Axioms/HWV001-2.ax'})$

$\mbox{type}(f,\mbox{fulladder})\qquad\mbox{cnf}(\mbox{f\_isa\_fulladder},\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(n_1,f),n_0)\qquad\mbox{cnf}(\mbox{in1}_1,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(n_2,f),n_1)\qquad\mbox{cnf}(\mbox{in2}_0,\mbox{hypothesis})$

$\mbox{value}(\mbox{in}(c,f),n_1)\qquad\mbox{cnf}(\mbox{inc}_1,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(s,f),n_1)\qquad\mbox{cnf}(\mbox{outs}_1,\mbox{hypothesis})$

$\mbox{value}(\mbox{out}(c,f),n_0)\qquad\mbox{cnf}(\mbox{outc}_0,\mbox{hypothesis})$

$\neg\,\mbox{mode}(\mbox{and}_2(h_1(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_and2h}_1,\mbox{negated\_conjecture})$

$\mbox{mode}(\mbox{or}_1(f),\mbox{abnormal}) \ \Rightarrow \ \neg\,\mbox{mode}(\mbox{and}_1(h_1(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_and1h}_1,\mbox{negated\_conjecture})$

$\mbox{mode}(\mbox{or}_1(f),\mbox{abnormal}) \ \Rightarrow \ \neg\,\mbox{mode}(\mbox{not}_1(h_1(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_not1h}_1,\mbox{negated\_conjecture})$

$\mbox{mode}(\mbox{or}_1(f),\mbox{abnormal}) \ \Rightarrow \ \neg\,\mbox{mode}(\mbox{and}_1(h_2(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_and1h}_2,\mbox{negated\_conjecture})$

$\mbox{mode}(\mbox{or}_1(f),\mbox{abnormal}) \ \Rightarrow \ \neg\,\mbox{mode}(\mbox{or}_1(h_2(f)),\mbox{abnormal})\qquad\mbox{cnf}(\mbox{diagnosis\_or1\_or1h}_2,\mbox{negated\_conjecture})$

\medskip\textbf{HWV009-3.p} Safelogic VHDL design verification obligation






$\mbox{include}(\mbox{'Axioms/HWV004-0.ax'})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTreset\_}(t_{206}))\qquad\mbox{cnf}(\mbox{quest}_1,\mbox{negated\_conjecture})$

$\mbox{p\_\_pred\_}(\mbox{fwork\_DOTfifo\_DOTrtl\_DOTwr\_\_error\_}(\mbox{f\_ADD\_}(t_{206},n_1)))\qquad\mbox{cnf}(\mbox{quest}_2,\mbox{negated\_conjecture})$

\medskip
\end{document}