PV2 ⊧ FGLtransforms expressions into Boolean formulae

Application domain/field

• Hardware verification
• Microprocessors
• Microcode verification
• Symbolic simulation
• Term rewriting

Type of tool

Rewriter/Library for ACL2

Internals

FGL is described as a term rewriter that transforms expressions acting on fixed-size data into Boolean formulae. One can then use equivalence checking between two sets of Boolean formulae to show that the implementation result matches the specification. FGL is integrated into ACL2.