Package hardware-multiplier-def: Definition of hardware multiplier devices

Information

Files

• Package tarball hardware-multiplier-def-1.12.tgz
• Theory source file hardware-multiplier-def.thy (included in the package tarball)

Defined Constants

• Hardware
  • Bus
    • Bus.multiplier
  • SumCarry
    • SumCarry.multiplier

Theorems

⊦ ∀ld xs xc d ys yc zb zs zc.
    SumCarry.multiplier ld xs xc d ys yc zb zs zc ⇔
    ∃xb ldd xbd.
      SumCarry.shiftRight ld xs xc xb ∧ pipe ld d ldd ∧ pipe xb d xbd ∧
      Bus.multiplier ldd xbd ys yc zb zs zc

⊦ ∀ld xb ys yc zb zs zc.
    Bus.multiplier ld xb ys yc zb zs zc ⇔
    ∃r sp sq sr cp cq cr yos yoc ps pc sq₀ sq₁ sr₀ sr₁ cq₀ cq₁ cr₀ cr₁ yos₀
      yos₁ yoc₀ yoc₁ pc₀ pc₁ pc₂ pc₃.
      Bus.width ys = r + 1 ∧ Bus.width yc = r + 1 ∧ Bus.width zs = r + 1 ∧
      Bus.width zc = r + 1 ∧ Bus.width sp = r + 1 ∧ Bus.width sq = r + 1 ∧
      Bus.width sr = r + 1 ∧ Bus.width cp = r + 1 ∧ Bus.width cq = r + 1 ∧
      Bus.width cr = r + 1 ∧ Bus.width yos = r + 1 ∧
      Bus.width yoc = r + 1 ∧ Bus.width ps = r ∧ Bus.width pc = r + 1 ∧
      Bus.wire sq 0 sq₀ ∧ Bus.sub sq 1 r sq₁ ∧ Bus.sub sr 0 r sr₀ ∧
      Bus.wire sr r sr₁ ∧ Bus.sub cq 0 r cq₀ ∧ Bus.wire cq r cq₁ ∧
      Bus.sub cr 0 r cr₀ ∧ Bus.wire cr r cr₁ ∧ Bus.wire yos 0 yos₀ ∧
      Bus.sub yos 1 r yos₁ ∧ Bus.sub yoc 0 r yoc₀ ∧ Bus.wire yoc r yoc₁ ∧
      Bus.wire pc 0 pc₀ ∧ Bus.sub pc 0 r pc₁ ∧ Bus.sub pc 1 r pc₂ ∧
      Bus.wire pc r pc₃ ∧ Bus.case1 ld (Bus.ground (r + 1)) sp sq ∧
      Bus.case1 ld (Bus.ground (r + 1)) cp cq ∧
      Bus.case1 xb ys (Bus.ground (r + 1)) yos ∧
      Bus.case1 xb yc (Bus.ground (r + 1)) yoc ∧ adder2 sq₀ yos₀ zb pc₀ ∧
      Bus.adder3 sq₁ cq₀ yos₁ ps pc₂ ∧ Bus.adder3 yoc₀ ps pc₁ sr₀ cr₀ ∧
      adder3 yoc₁ cq₁ pc₃ sr₁ cr₁ ∧ Bus.connect sr zs ∧ Bus.connect cr zc ∧
      Bus.delay sr sp ∧ Bus.delay cr cp

External Type Operators

• →
• bool
• Hardware
  • bus
  • wire
• Number
  • Natural
    • natural

External Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ∃
    • ⊤
• Hardware
  • adder2
  • adder3
  • pipe
  • Bus
    • Bus.adder3
    • Bus.case1
    • Bus.connect
    • Bus.delay
    • Bus.ground
    • Bus.sub
    • Bus.width
    • Bus.wire
  • SumCarry
    • SumCarry.shiftRight
• Number
  • Natural
    • +
    • bit1
    • zero

Assumptions

⊦ ⊤

⊦ (∀) = λp. p = λx. ⊤

OpenTheory package document generated by opentheory 1.3 (release 20151018)