Package hardware-multiplier-thm: Properties of hardware multiplier devices

Information

Files

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

Theorems

⊦ ∀ld xb ys yc zb zs zc.
    Bus.multiplier ld xb ys yc zb zs zc ⇒
    ∃r.
      Bus.width ys = r + 1 ∧ Bus.width yc = r + 1 ∧ Bus.width zs = r + 1 ∧
      Bus.width zc = r + 1

⊦ ∀x y ld xb ys yc zb zs zc t k.
    (∀i.
       i ≤ k ⇒
       (signal ld (t + i) ⇔ i = 0) ∧ (signal xb (t + i) ⇔ Bits.bit x i) ∧
       (Bits.bit x i ⇒
        Bits.fromList (Bus.signal ys (t + i)) +
        2 * Bits.fromList (Bus.signal yc (t + i)) = y)) ∧
    Bus.multiplier ld xb ys yc zb zs zc ⇒
    Bits.cons (signal zb (t + k))
      (Bits.fromList (Bus.signal zs (t + k)) +
       2 * Bits.fromList (Bus.signal zc (t + k))) =
    Bits.shiftRight (Bits.bound x (k + 1) * y) k

⊦ ∀x y ld xs xc d ys yc zb zs zc t k.
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.fromList (Bus.signal xs t) + 2 * Bits.fromList (Bus.signal xc t) =
    x ∧
    (∀i.
       i ≤ d + k ∧ d ≤ i ∧ i ≤ Bus.width xs + (d + 1) ⇒
       Bits.fromList (Bus.signal ys (t + i)) +
       2 * Bits.fromList (Bus.signal yc (t + i)) = y) ∧
    SumCarry.multiplier ld xs xc d ys yc zb zs zc ⇒
    Bits.cons (signal zb (t + (d + k)))
      (Bits.fromList (Bus.signal zs (t + (d + k))) +
       2 * Bits.fromList (Bus.signal zc (t + (d + k)))) =
    Bits.shiftRight (Bits.bound x (k + 1) * y) k

External Type Operators

• →
• bool
• Data
  • List
    • list
• Hardware
  • bus
  • wire
• Number
  • Natural
    • natural

External Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ⇒
    • ∃
    • ¬
    • cond
    • ⊥
    • ⊤
  • List
    • ::
    • length
• Hardware
  • adder2
  • adder3
  • pipe
  • signal
  • Bus
    • Bus.adder3
    • Bus.append
    • Bus.case1
    • Bus.connect
    • Bus.delay
    • Bus.ground
    • Bus.multiplier
    • Bus.signal
    • Bus.single
    • Bus.sub
    • Bus.width
    • Bus.wire
  • SumCarry
    • SumCarry.multiplier
    • SumCarry.shiftRight
• Number
  • Natural
    • *
    • +
    • <
    • ≤
    • bit0
    • bit1
    • fromBool
    • max
    • suc
    • zero
    • Bits
      • Bits.bit
      • Bits.bound
      • Bits.cons
      • Bits.fromList
      • Bits.head
      • Bits.shiftLeft
      • Bits.shiftRight
      • Bits.tail
      • Bits.width

Assumptions

⊦ ⊤

⊦ bit0 0 = 0

⊦ fromBool ⊥ = 0

⊦ ∀t. t ⇒ t

⊦ ∀n. n ≤ n

⊦ ⊥ ⇔ ∀p. p

⊦ fromBool ⊤ = 1

⊦ ∀n. n ≤ suc n

⊦ (¬) = λp. p ⇒ ⊥

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

⊦ ∀t. (t ⇔ ⊤) ⇔ t

⊦ ∀t. ⊤ ∧ t ⇔ t

⊦ ∀t. t ∧ ⊤ ⇔ t

⊦ ∀t. ⊥ ⇒ t ⇔ ⊤

⊦ ∀t. ⊤ ⇒ t ⇔ t

⊦ ∀n. ¬(suc n = 0)

⊦ ∀n. 0 * n = 0

⊦ ∀m. m * 0 = 0

⊦ ∀n. 0 + n = n

⊦ ∀m. m + 0 = m

⊦ ∀k. Bits.shiftLeft 0 k = 0

⊦ ∀n. Bits.shiftRight n 0 = n

⊦ ∀t. (t ⇔ ⊥) ⇔ ¬t

⊦ ∀b. Bits.cons b 0 = fromBool b

⊦ ∀n. bit1 n = suc (bit0 n)

⊦ ∀n. Bits.bit n 0 ⇔ Bits.head n

⊦ ∀m. 1 * m = m

⊦ ∀l. Bits.width (Bits.fromList l) ≤ length l

⊦ ∀m n. m ≤ m + n

⊦ (⇒) = λp q. p ∧ q ⇔ p

⊦ ∀m. suc m = m + 1

⊦ ∀t₁ t₂. (if ⊥ then t₁ else t₂) = t₂

⊦ ∀t₁ t₂. (if ⊤ then t₁ else t₂) = t₁

⊦ ∀h t. Bits.tail (Bits.cons h t) = t

⊦ ∀n. Bits.bound n 1 = fromBool (Bits.head n)

⊦ ∀x t. length (Bus.signal x t) = Bus.width x

⊦ ∀m n. m * n = n * m

⊦ ∀m n. m + n = n + m

⊦ ∀n t. Bits.fromList (Bus.signal (Bus.ground n) t) = 0

⊦ ∀n. Bits.cons ⊥ n = 2 * n

⊦ ∀n i. Bits.bit n i ⇒ i < Bits.width n

⊦ ∀m n. m < suc n ⇔ m ≤ n

⊦ (∧) = λp q. (λf. f p q) = λf. f ⊤ ⊤

⊦ ∀n. Bits.shiftLeft n 1 = 2 * n

⊦ (∃) = λp. ∀q. (∀x. p x ⇒ q) ⇒ q

⊦ ∀h t. Bits.fromList (h :: t) = Bits.cons h (Bits.fromList t)

⊦ ∀m n. m + suc n = suc (m + n)

⊦ ∀n k. Bits.shiftRight n (suc k) = Bits.tail (Bits.shiftRight n k)

⊦ ∀n k. Bits.width (Bits.shiftLeft n k) ≤ Bits.width n + k

⊦ ∀m n. suc m ≤ suc n ⇔ m ≤ n

⊦ ∀x y. Bus.sub x 0 (Bus.width x) y ⇔ y = x

⊦ ∀w t. Bits.fromList (Bus.signal (Bus.single w) t) = fromBool (signal w t)

⊦ ∀n k. Bits.shiftLeft n (suc k) = Bits.cons ⊥ (Bits.shiftLeft n k)

⊦ ∀n k. Bits.shiftLeft n (suc k) = Bits.shiftLeft (Bits.cons ⊥ n) k

⊦ ∀h t. Bits.cons h t = fromBool h + 2 * t

⊦ ∀x y t. Bus.connect x y ⇒ Bus.signal y t = Bus.signal x t

⊦ ∀m n p. m + (n + p) = m + n + p

⊦ ∀k n₁ n₂. Bits.shiftLeft (n₁ * n₂) k = n₁ * Bits.shiftLeft n₂ k

⊦ ∀m n p. m + n = m + p ⇔ n = p

⊦ ∀p m n. m + p = n + p ⇔ m = n

⊦ ∀m n p. m + n ≤ m + p ⇔ n ≤ p

⊦ ∀m n p. n + m ≤ p + m ⇔ n ≤ p

⊦ ∀m n p. m < n ∧ n ≤ p ⇒ m < p

⊦ ∀m n p. m ≤ n ∧ n ≤ p ⇒ m ≤ p

⊦ ∀x k n y. Bus.sub x k n y ⇒ Bus.width y = n

⊦ ∀m n. Bits.width (m + n) ≤ max (Bits.width m) (Bits.width n) + 1

⊦ ∀x i w. Bus.wire x i w ⇔ Bus.sub x i 1 (Bus.single w)

⊦ ∀p. p 0 ∧ (∀n. p n ⇒ p (suc n)) ⇒ ∀n. p n

⊦ ∀m n p. max n p ≤ m ⇔ n ≤ m ∧ p ≤ m

⊦ ∀m n p. m * (n + p) = m * n + m * p

⊦ ∀m n p. (m + n) * p = m * p + n * p

⊦ ∀k n₁ n₂.
    Bits.shiftLeft (n₁ + n₂) k = Bits.shiftLeft n₁ k + Bits.shiftLeft n₂ k

⊦ ∀n₁ n₂ k.
    Bits.shiftRight (n₁ + Bits.shiftLeft n₂ k) k =
    Bits.shiftRight n₁ k + n₂

⊦ ∀n k.
    Bits.bound n (suc k) =
    Bits.bound n k + Bits.shiftLeft (fromBool (Bits.bit n k)) k

⊦ ∀x y t. Bus.delay x y ⇒ Bus.signal y (t + 1) = Bus.signal x t

⊦ ∀w x t.
    Bus.signal (Bus.append (Bus.single w) x) t =
    signal w t :: Bus.signal x t

⊦ ∀w d wd t. pipe w d wd ⇒ (signal wd (t + d) ⇔ signal w t)

⊦ ∀p c x y. p (if c then x else y) ⇔ (c ⇒ p x) ∧ (¬c ⇒ p y)

⊦ ∀x y t.
    Bits.fromList (Bus.signal (Bus.append x y) t) =
    Bits.fromList (Bus.signal x t) +
    Bits.shiftLeft (Bits.fromList (Bus.signal y t)) (Bus.width x)

⊦ ∀s x y z t.
    Bus.case1 s x y z ⇒
    Bus.signal z t = if signal s t then Bus.signal x t else Bus.signal y t

⊦ ∀ld xs xc xb.
    SumCarry.shiftRight ld xs xc xb ⇒
    ∃r. Bus.width xs = r + 1 ∧ Bus.width xc = r + 1

⊦ ∀x y z k m n.
    Bus.sub x k m y ∧ Bus.sub x (k + m) n z ⇒
    Bus.sub x k (m + n) (Bus.append y z)

⊦ ∀x y s c t.
    adder2 x y s c ⇒
    fromBool (signal x t) + fromBool (signal y t) =
    fromBool (signal s t) + 2 * fromBool (signal c t)

⊦ ∀x y z s c t.
    Bus.adder3 x y z s c ⇒
    Bits.fromList (Bus.signal x t) +
    (Bits.fromList (Bus.signal y t) + Bits.fromList (Bus.signal z t)) =
    Bits.fromList (Bus.signal s t) + 2 * Bits.fromList (Bus.signal c t)

⊦ ∀x y z s c t.
    adder3 x y z s c ⇒
    fromBool (signal x t) +
    (fromBool (signal y t) + fromBool (signal z t)) =
    fromBool (signal s t) + 2 * fromBool (signal c t)

⊦ ∀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

⊦ ∀x ld xs xc xb t k.
    (∀i. i ≤ k ⇒ (signal ld (t + i) ⇔ i = 0)) ∧
    Bits.fromList (Bus.signal xs t) + 2 * Bits.fromList (Bus.signal xc t) =
    x ∧ SumCarry.shiftRight ld xs xc xb ⇒
    (signal xb (t + k) ⇔ Bits.bit x k)

⊦ ∀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

OpenTheory package document generated by opentheory 1.3 (release 20151018)