Verification of Synchronization in SpecC Description with the Use of Difference Decision Diagrams(Logic and High Synthesis)(<Special Section>VLSI Design and CAD Algorithms)

スポンサーリンク

概要

• 論文の詳細を見る

• SpecC language is designated to handle the design of entire system from specification to implementation and of hardware/software co-design. Concurrency is one of the features of SpecC which expresses the parallel execution of processes. Describing the systems which contain concurrent behaviors would have some data exchanging or transferring among them. Therefore, the synchronization semantics (notify/wait) of events should be incorporated. The actual design, which is usually sophisticated by its characteristic and functionalities, may contain a bunch of event synchronization codes. This will make the design difficult and time-consuming to verify. In this paper, we introduce a technique which helps verifying the synchronization of events in SpecC. The original SpecC code containing synchronization semantics is parsed and translated into a Boolean SpecC code. The difference decision diagrams (DDDs) is used to verify for event synchronization on Boolean SpecC code. The counter examples for tracing back to the original source are given when the verification results turn out to be unsatisfied. Here we also introduce idea on automatically refinement when the results are unsatisfied and preset some preliminary results.

• 社団法人電子情報通信学会の論文
• 2003-12-01

著者

• SAKUNKONCHAK Thanyapat

  VLSI Design and Education Center (VDEC), The University of Tokyo

• KOMATSU Satoshi

  VLSI Design and Education Center (VDEC), The University of Tokyo

• FUJITA MASAHIRO

  Department of Pathology, Keiyukai Sapporo Hospital

• Komatsu S

  Univ. Tokyo Tokyo Jpn

• Komatsu Satoshi

  Vlsi Design And Education Center (vdec) The University Of Tokyo

• Sakunkonchak Thanyapat

  Vlsi Design And Education Center (vdec) The University Of Tokyo

• Fujita M

  Vlsi Design And Education Center (vdec) The University Of Tokyo

• SAKUNKONCHAK Thanyapat

  Department of Electronics Engineering, University of Tokyo

• Fujita Masahiro

  Department Of Anatomy Sapporo Medical University

関連論文

• Synchronization Verification in System-Level Design with ILP Solvers(System Level Design,VLSI Design and CAD Algorithms)
• RECURRENCE AFTER ENDOSCOPIC MUCOSAL RESECTION OF ESOPHAGEAL SQUAMOUS CELL CARCINOMA INVADING THE MUSCULARIS MUCOSAE OR UPPER SUBMUCOSA
• Endoscopic Ultrasonography for the Detection of Lymph Node Metastasis in Superficial Esophageal Carcinoma
• Synthesis and Structure-Antibacterial Activity Relationships of 7-(3-Amino-1-propynyl and 3-Amino-1-propenyl)quinolones
• 5-Alkoxyimidazoquinolones as Potential Antibacterial Agents. Synthesis and Structure-Activity Relationships
• Primary low-grade gastric mucosa-associated lymphoid tissue (MALT) lymphoma with polypoid appearance. Polypoid gastric MALT lymphoma : A clinicopathologic study of eight cases
• Development of Three-Dimensional Structure Formation Simulator of Colloidal Nanoparticles during Drying
• Jejunal carcinoid tumor mimicking leiomyosarcoma: preoperative diagnosis by endoscopic biopsy
• Expression of sulfated carbohydrate chain and core peptides of mucin detected by monoclonal antibodies in Barrett's esophagus and esophageal adenocarcinoma
• Low Power and Fault Tolerant Encoding Methods for On-Chip Data Transfer in Practical Applications(Low Power Methodology, VLSI Design and CAD Algorithms)
• Approaches for Reducing Power Consumption in VLSI Bus Circuits (Special Issue on Low-Power High-Speed CMOS LSI Technologies)
• Formation of Well-Aligned Thin Films of Rod-Like Nanoparticles via Solvent Evaporation : A Simulation Study
• Cell cycle control by daf-21/Hsp90 at the first meiotic prophase/metaphase boundary during oogenesis in Caenorhabditis elegans
• Effects of Particle Size on the Monolayer Structure of Nanoparticles Formed via a Wet-Coating Process
• Effect of strength of the flyer plate material on the collision parameters in explosive welding
• The AMS Extension to System Level Design Language-SpecC(System Level Design,VLSI Design and CAD Algorithms)
• Synchronization Mechanism for Timed/Untimed Mixed-Signal System Level Design Environment(Selected Papers from the 18th Workshop on Circuits and Systems in Karuizawa)
• Irredundant Low Power Address Bus Encoding Techniques Based on Adaptive Codebooks
• 639 Investigation on Performance of Extremely High Impulsive Pressure Generator Using Collision of High Velocity Jet
• Effects of Vigabatrin on the GABAergic System as Determined by [^(123)I] Iomazenil SPECT and GABA MRS
• 7-(2-Aminomethyl-1-azetidinyl)-4-oxoquinoline-3-carboxylic Acids as Potent Antibacterial Agents : Design, Synthesis, and Antibacterial Activity
• Flash Radiographic Study of Shock Wave Propagation in Laminated Composites
• 3A12 Flow Cytometric Nuclear DNA Content Analysis of Renal Tumors in Children
• Irredundant Low Power Address Bus Encoding Techniques Based on Adaptive Codebooks(Power Optimization)(VLSI Design and CAD Algorithms)
• Interconnect-Aware Pipeline Synthesis for Array-Based Architectures
• Can hybrid FDG-PET/CT detect subclinical lymph node metastasis of esophageal cancer appropriately and contribute to radiation treatment planning? A comparison of image-based and pathological findings
• Myogenic lineage differentiated mesenchymal stem cells enhance recovery from dextran sulfate sodium-induced colitis in the rat
• Direct Simulation Model of Concentrated Particulate Flow in Pressure-Driven Dead-End Microfiltration
• Two-Dimensional Simulation of Lift Velocities of Spherical Particles in Crossflow Microfiltration
• Verification of Synchronization in SpecC Description with the Use of Difference Decision Diagrams(Logic and High Synthesis)(VLSI Design and CAD Algorithms)
• The use of single-shot explosive welding technique for the fabrication of aluminum/stainless steel composites
• Single-Shot Explosive Welding of Hard-to-Weld JIS A5083/SUS304 Clad Using SUS304 Intermediate Plate
• An explosive bonding method performed by reflective action of underwater shock wave
• 640 An Effective Application of Reflective Action of Underwater Shock Wave for Explosive Bonding Process
• A High-Speed Multiplier-Free Realization of IIR Filter Using ROM's and Elevated Signal Rate(Special Section on Papers Selected from ITC-CSCC 2000)
• Applications of SPECT imaging of dopaminergic neurotransmission in neuropsychiatric disorders
• Logic Optimization of Asynchronous Speed-Independent Circuits Using Transduction Methods (特集:システムLSIの設計技術と設計自動化)
• Basic Characteristics of the Explosive Welding Technique Using Underwater Shock Wave and Its Possibilities
• Thin Film of Silica Nanoparticles with Highly Ordered Hemispherical Macropores
• Formal Verification based on recurrence equations and equivalence checking
• Simulation Model of Concentrated Colloidal Rod-Like Nanoparticles
• Computation of Capillary Interactions among Many Particles at Free Surface
• High-Throughput Electron Beam Direct Writing of VIA Layers by Character Projection with One-Dimensional VIA Characters
• Residents' Evaluation of Local Portal Site's Providers in Terms of Credibility(APCIM2009 Best Papers)
• A Structured Routing Architecture for Practical Application of Character Projection Method in Electron-Beam Direct Writing

もっと見る 閉じる

スポンサーリンク