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

Information

Files

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

Defined Constants

• Hardware
  • counter
  • counterPulse
  • eventCounter
  • pipe
  • Bus
    • Bus.pipe

Theorems

⊦ ∀ld nb dn. counterPulse ld nb dn ⇔ ∃ds. counter ld nb ds ∧ pulse ds dn

⊦ ∀w d wd.
    pipe w d wd ⇔
    ∃x x₀.
      Bus.width x = d + 1 ∧ Bus.wire x d x₀ ∧ Bus.pipe w x ∧ connect x₀ wd

⊦ ∀w x.
    Bus.pipe w x ⇔
    ∃r xp x₀ x₁ x₂.
      Bus.width x = r + 1 ∧ Bus.width xp = r ∧ Bus.wire x 0 x₀ ∧
      Bus.sub x 0 r x₁ ∧ Bus.sub x 1 r x₂ ∧ connect w x₀ ∧
      Bus.connect xp x₂ ∧ Bus.delay x₁ xp

⊦ ∀ld nb dn.
    counter ld nb dn ⇔
    ∃r sp cp sq cq sr cr dp dq dr nb₀ nb₁ cp₀ cp₁ cp₂ cq₀ cq₁ cr₀ cr₁.
      Bus.width nb = r + 1 ∧ Bus.width sp = r ∧ Bus.width cp = r + 1 ∧
      Bus.width sq = r ∧ Bus.width cq = r + 1 ∧ Bus.width sr = r ∧
      Bus.width cr = r + 1 ∧ Bus.wire nb 0 nb₀ ∧ Bus.sub nb 1 r nb₁ ∧
      Bus.wire cp 0 cp₀ ∧ Bus.sub cp 0 r cp₁ ∧ Bus.wire cp r cp₂ ∧
      Bus.wire cq 0 cq₀ ∧ Bus.sub cq 1 r cq₁ ∧ Bus.wire cr 0 cr₀ ∧
      Bus.sub cr 1 r cr₁ ∧ not cp₀ cq₀ ∧ Bus.adder2 sp cp₁ sq cq₁ ∧
      or2 dp cp₂ dq ∧ Bus.case1 ld nb₁ sq sr ∧ case1 ld nb₀ cq₀ cr₀ ∧
      Bus.case1 ld (Bus.ground r) cq₁ cr₁ ∧ case1 ld ground dq dr ∧
      connect dr dn ∧ Bus.delay sr sp ∧ Bus.delay cr cp ∧ delay dr dp

⊦ ∀ld nb inc dn.
    eventCounter ld nb inc dn ⇔
    ∃r sp cp sq cq sr cr dp dq dr sp₀ sp₁ cp₀ cp₁ cp₂ sq₀ sq₁ cq₀ cq₁.
      Bus.width nb = r + 1 ∧ Bus.width sp = r + 1 ∧ Bus.width cp = r + 1 ∧
      Bus.width sq = r + 1 ∧ Bus.width cq = r + 1 ∧ Bus.width sr = r + 1 ∧
      Bus.width cr = r + 1 ∧ Bus.wire sp 0 sp₀ ∧ Bus.sub sp 1 r sp₁ ∧
      Bus.wire sq 0 sq₀ ∧ Bus.sub sq 1 r sq₁ ∧ Bus.wire cp 0 cp₀ ∧
      Bus.sub cp 0 r cp₁ ∧ Bus.wire cp r cp₂ ∧ Bus.wire cq 0 cq₀ ∧
      Bus.sub cq 1 r cq₁ ∧ xor2 inc sp₀ sq₀ ∧ and2 inc sp₀ cq₀ ∧
      Bus.adder2 sp₁ cp₁ sq₁ cq₁ ∧ or2 dp cp₂ dq ∧ Bus.case1 ld nb sq sr ∧
      Bus.case1 ld (Bus.ground (r + 1)) cq cr ∧ case1 ld ground dq dr ∧
      connect dr dn ∧ Bus.delay sr sp ∧ Bus.delay cr cp ∧ delay dr dp

External Type Operators

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

External Constants

• =
• Data
  • Bool
    • ∀
    • ∧
    • ∃
    • ⊤
• Hardware
  • and2
  • case1
  • connect
  • delay
  • ground
  • not
  • or2
  • pulse
  • xor2
  • Bus
    • Bus.adder2
    • Bus.case1
    • Bus.connect
    • Bus.delay
    • Bus.ground
    • Bus.sub
    • Bus.width
    • Bus.wire
• Number
  • Natural
    • +
    • bit1
    • zero

Assumptions

⊦ ⊤

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

OpenTheory package document generated by opentheory 1.3 (release 20141105)