A comparative study of modelling at different levels of abstraction in system on chip designs: a case study

2004 ◽  
Author(s):  
S. Jayadevappa ◽  
R. Shankar ◽  
I. Mahgoub
Keyword(s):  
Comparative Study ◽  
System On Chip ◽  
Levels Of Abstraction ◽  
On Chip ◽  
Different Levels

scholarly journals Cryptographic Protocol Verification via Supercompilation (A Case Study)

10.29007/gpsh ◽  
2018 ◽  
Author(s):  
Abdulbasit Ahmed ◽  
Alexei Lisitsa ◽  
Andrei Nemytykh
Keyword(s):  
Program Transformation ◽  
Cache Coherence ◽  
Protocol Verification ◽  
Cryptographic Protocol ◽  
Levels Of Abstraction ◽  
Transformation Techniques ◽  
Program Specialization ◽  
Coherence Protocols ◽  
Different Levels

It has been known for a while that program transformation techniques, in particular, program specialization, can be used to prove the properties of programs automatically. For example, if a program actually implements (in a given context of use) a constant function, sufficiently powerful and semantics preserving program transformation may reduce the program to a syntactically trivial ``constant'' program, pruning unreachable branches and proving thereby the property. Viability of such an approach to verification has been demonstrated in previous works where it was applied to the verification of parameterized cache coherence protocols and Petri Nets models.In this paper we further extend the method and present a case study on its appication to the verification of a cryptographic protocol. The protocol is modeled by functional programs at different levels of abstraction and verification via program specialization is done by using Turchin's supercompilation method.

A case study on logic diagnosis for System-on-Chip

2009 ◽  
Author(s):  
Y. Benabboud ◽  
A. Bosio ◽  
P. Girard ◽  
S. Pravossoudovitch ◽  
A. Virazel ◽  
...  
Keyword(s):  
System On Chip ◽  
On Chip

scholarly journals SystemC Transaction-Level Modeling of an MPSoC Platform Based on an Open Source ISS by Using Interprocess Communication

2008 ◽  
Vol 2008 ◽  
pp. 1-10
Author(s):  
Sami Boukhechem ◽  
El-Bay Bourennane
Keyword(s):  
Open Source ◽  
System On Chip ◽  
Open Architecture ◽  
Multiprocessor System ◽  
Instruction Set ◽  
Levels Of Abstraction ◽  
Transaction Level Modeling ◽  
Synthesis Tool ◽  
Transaction Level ◽  
On Chip

Transaction-level modeling (TLM) is a promising technique to deal with the increasing complexity of modern embedded systems. This model allows a system designer to model a complete application, composed of hardware and software parts, at several levels of abstraction. For this purpose, we use systemC, which is proposed as a standardized modeling language. This paper presents a transaction-level modeling cosimulation methodology for modeling, validating, and verifying our embedded open architecture platform. The proposed platform is an open source multiprocessor system-on-chip (MPSoC) platform, integrated under the synthesis tool for adaptive and reconfigurable system-on-chip (STARSoC) environment. It relies on the integration between an open source instruction set simulators (ISSs), OR1Ksim platform, and the systemC simulation environment which contains other components (wishbone bus, memories, , etc.). The aim of this work is to provide designers with the possibility of faster and efficient architecture exploration at a higher level of abstractions, starting from an algorithmic description to implementation details.

Do semantic modal maps have a role in a constructionalization approach to modals?

2016 ◽  
Vol 8 (1) ◽  
pp. 97-124 ◽  
Author(s):  
Elizabeth Closs Traugott
Keyword(s):  
Construction Grammar ◽  
Levels Of Abstraction ◽  
Semantic Maps ◽  
Micro Level ◽  
Different Levels ◽  
Over Time ◽  
Conceptual Schemas

My aim in this paper is to show that, in modified form, semantic connectivity maps of the kind developed in van der Auwera & Plungian (1998) and van der Auwera (2013) can be useful for showing the development over time of relationships among polysemous constructions. Since these maps pertain primarily to meaning and are intended as contributions to cross-linguistic generalizations rather than to language-specific grammars, their purpose might seem orthogonal to construction grammar, in which form–meaning pairs are the basic units of grammar. I propose that the semantic maps can usefully be rethought as being of two kinds: schema-construction maps that represent relationships between abstract, conceptual schemas linked to underspecified form, and micro-construction maps that represent relationships between specific constructions. These two kinds of maps capture both form and meaning since they represent form–meaning pairings, but at different levels of abstraction. They can also capture direction of changes, as tendencies at the schema level and specific trajectories at the micro-level. My case study is the development of the marginal modals better, rather, sooner (see Denison & Cort 2010, van der Auwera & De Wit 2010). I show that better is significantly different in distribution and meaning from rather and sooner, and that, although they form a family of micro-constructions, they do not form a tight-knit group. This can be captured well by modified semantic maps.

A Hierarchy of System Descriptions via Atomic Linear Refinement

1992 ◽  
Vol 16 (3-4) ◽  
pp. 289-336
Author(s):  
Roberto Gorrieri
Keyword(s):  
Proof System ◽  
Weak Equivalence ◽  
Levels Of Abstraction ◽  
Complete Proof ◽  
Transition Systems ◽  
Action Refinement ◽  
Atomic Action ◽  
Description Languages ◽  
Different Levels

The problem of relating system descriptions at different levels of abstraction is studied in the field of Process Description Languages, following the so-called interleaving approach. Since we believe that several different languages should be used profitably during the hierarchical specification process, we investigate the problem of implementing a calculus into another one. As a case study, we introduce a pair of languages which will be increasingly enriched. The basic languages are sequential and nondeterministic; their first enrichment is obtained by adding an operator for asynchrony; then also communication is added, and finally restriction is dealt with. For each pair, the latter language extends the former with atomicity, obtained by adding to the signature of the former an operator of strong prefixing that makes atomic the execution of a sequence of actions. The two languages are intended to be a specification and an implementation language, respectively. To directly relate them, a mapping, called atomic linear refinement, is introduced from actions of the former to atomic sequences (i.e. sequences of actions built with strong prefixing) of the latter. An atomic linear refinement can be homomorphically extended to become a mapping among process terms of the two languages and thus also among the states of their associated transition systems. A notion of implementation, based on a sort of bisimulation (parametric with respect to an atomic action refinement), relates processes of the two languages. Given a specification process p and an atomic action refinement ρ, the refined process ρ(p) is proved to be an implementation of p. Moreover, a complete proof system for strong and weak equivalence are presented for both languages (and thus also for the operator of strong prefixing) and proved consistent with respect to refinement: if p and ρ are congruent processes of the specification language, then ρ(p) and ρ(q) are congruent, too.

Sign in / Sign up

Export Citation Format

Share Document