soc.fu.logical.formal package

Submodules

soc.fu.logical.formal.proof_bpermd module

class soc.fu.logical.formal.proof_bpermd.Driver

Bases: nmigen.hdl.ir.Elaboratable

elaborate(platform)

class soc.fu.logical.formal.proof_bpermd.TestCase(methodName='runTest')

Bases: nmutil.formaltest.FHDLTestCase

test_formal()

test_ilang()

soc.fu.logical.formal.proof_input_stage module

class soc.fu.logical.formal.proof_input_stage.Driver

Bases: nmigen.hdl.ir.Elaboratable

elaborate(platform)

class soc.fu.logical.formal.proof_input_stage.GTCombinerTestCase(methodName='runTest')

Bases: nmutil.formaltest.FHDLTestCase

test_formal()

test_ilang()

soc.fu.logical.formal.proof_main_stage module

Links:

• https://bugs.libre-soc.org/show_bug.cgi?id=331
• https://libre-soc.org/openpower/isa/fixedlogical/

class soc.fu.logical.formal.proof_main_stage.Driver

Bases: nmigen.hdl.ir.Elaboratable

elaborate(platform)

class soc.fu.logical.formal.proof_main_stage.LogicalTestCase(methodName='runTest')

Bases: nmutil.formaltest.FHDLTestCase

test_formal()

test_ilang()

soc.fu.logical.formal.proof_main_stage.simple_popcount(sig, width)

simple, naive (and obvious) popcount. formal verification does not to be fast: it does have to be correct

Module contents