scientific article
From MaRDI portal
Publication:3753927
zbMath0612.94015MaRDI QIDQ3753927
Publication date: 1986
Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.
specificationhardware verificationHigher-order logichardware description languageCMOS full adderCMOS inverteredge-triggered Dtype registern-bit ripple-carry addersequential multiplier
Related Items (19)
ACKERMANN’S FUNCTION IN ITERATIVE FORM: A PROOF ASSISTANT EXPERIMENT ⋮ Rule-based induction ⋮ Accelerating tableaux proofs using compact representations ⋮ Indentification of inductive properties during verification of synchronous sequential circuits ⋮ Computational logic: its origins and applications ⋮ Computer assisted reasoning. A Festschrift for Michael J. C. Gordon ⋮ Proving and rewriting ⋮ Verification of asynchronous circuits by BDD-based model checking of Petri nets ⋮ A formalised theorem in the partition calculus ⋮ Automatic verification of a class of systolic circuits ⋮ Abstraction of hardware construction ⋮ Circuits as streams in Coq: Verification of a sequential multiplier ⋮ Universal algebra in higher types ⋮ A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL ⋮ Logic, sets, and mathematics ⋮ From LCF to Isabelle/HOL ⋮ Structuring and automating hardware proofs in a higher-order theorem- proving environment ⋮ Coquet: A Coq Library for Verifying Hardware ⋮ Set theory for verification. I: From foundations to functions
Uses Software
This page was built for publication:
