|
|
|---|
|
|
|
|---|
Does a FAIG always evaluate to a purely Boolean value, i.e., is it never X or Z?
When an FAIG is known to be purely Boolean, then there is not much reason to represent it as an FAIG—we might as well throw its offset away and just work with its onset as an AIG.
When you are dealing with nice, well-behaved, RTL-level circuits that don't use any fancy low-level, four-valued sorts of things like tri-state buffers, this can be a useful optimization. For instance, it may reduce the complexity of SAT queries, or carry out other kinds of analysis where you don't have to think about four-valuedness.
(faig-purebool-p x) is a logically nice, but non-executable way to express pure Boolean-ness. See also faig-purebool-check, which can be executed; it uses a SAT solver to answer the question.
Function:
(defun faig-purebool-p (x) (declare (xargs :non-executable t)) (declare (xargs :guard t)) (prog2$ (throw-nonexec-error 'faig-purebool-p (list x)) (let ((env (faig-purebool-p-witness x))) (or (equal (faig-eval x env) (faig-t)) (equal (faig-eval x env) (faig-f))))))
Theorem:
(defthm faig-purebool-p-necc (implies (not (or (equal (faig-eval x env) (faig-t)) (equal (faig-eval x env) (faig-f)))) (not (faig-purebool-p x))))