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 ?

 

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.

 

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 .

 

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?

 

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.

 

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.

 

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."