# SPA method for digital logic design and the Poage method

#### razvan23

Joined Mar 2, 2021
15
Hello, I am trying to learn the SPA method for digital logic design and i can't find anything ok on internet. For reference I am studing in my university right not electronic equipment testing and my professor didn't leave us some valid example. I have just one which I will post. Can someone please explain the steps for using the SPA ?

#### Attachments

• 1.3 MB Views: 7

#### dl324

Joined Mar 30, 2015
16,899
I am trying to learn the SPA method for digital logic design and i can't find anything ok on internet.
What the heck is SPA? Googling is pointless unless you want to filter through a lot of hits for a hot tubs and similar.

#### razvan23

Joined Mar 2, 2021
15
What the heck is SPA? Googling is pointless unless you want to filter through a lot of hits for a hot tubs and similar.
SPA stands for Single Path Activation method for Combinational Logic Circuits .

#### dl324

Joined Mar 30, 2015
16,899
SPA stands for Single Path Activation method for Combinational Logic Circuits .
Never heard of it. What's the benefit over the traditional method?

Is this school work?

#### razvan23

Joined Mar 2, 2021
15
Never heard of it. What's the benefit over the traditional method?

Is this school work?
Yes, it's school work and I can't find any information about it. The SPA is regarding of Principles of the test stimulus vectors’ generation.

#### WBahn

Joined Mar 31, 2012
30,034
Never heard of it, so unless you provide us with a pretty detailed description of what it is and how it is supposed to be used, it's going to be hard to get any assistance.

#### Danko

Joined Nov 22, 2017
1,834
One-Path Reachability Logic?

"VIII. Conclusion
We presented (one-path) reachability logic, a novel framework
for reasoning about reachability which unifies operational
and axiomatic semantics. Its sentences, the reachability rules,
can express both transitions between configurations, as needed
for operational semantics, and Hoare-style triples, as needed for
axiomatic semantics. A programming language is given as a set
of reachability rules defining its operational semantics, and a
sound and relatively complete language-independent seven-rule
proof system then can derive any reachability property of the
language. The soundness result was also mechanized in Coq,
which lets reachability logic proofs serve as proof certificates.
Until now, reachability rules were unconditional, so they
could only express a few styles of operational semantics. By
allowing conditional rules, reachability logic can now express
virtually all operational semantics styles, including the standard
small-step (by Plotkin) and big-step (by Kahn) semantics which
were excluded before.
We hope reachability logic may serve as a new foundation for
verifying programs. Also, since Hoare-style proof derivations
can be mechanically translated into reachability logic proof
derivations, reachability logic may also serve as a more elegant
means to establish soundness of axiomatic semantics."

#### Attachments

• 186.1 KB Views: 4
• 604.6 KB Views: 3
Last edited: