| Title | Formal Representation and Verification of Arithmetic Circuits Using Symbolic Computer Algebra |
| Author | *Yuki Watanabe, Naofumi Homma, Takafumi Aoki (Tohoku University, Japan), Tatsuo Higuchi (Tohoku Institute of Technology, Japan) |
| Page | pp. 461 - 468 |
| Keyword | datapath, arithmetic circuit, formal verification, computer algebra |
| Abstract | This paper presents an application of symbolic computer algebra to arithmetic circuit design. Our method represents an arithmetic circuit as a hierarchical graph, which consists of high-level mathematical objects based on weighted number systems and arithmetic formulae. We can verify the function of such circuit representation by polynomial reduction techniques using Groebner Bases as well as the conventional *BMD (multiplicative Binary Moment Diagram) techniques. In this paper, we investigate the basic characteristics of the proposed representation and verification through some case studies such as parallel multiplier and BCD (Binary-Coded Decimal) adder. The result shows that the proposed approach succeeded in verifying some arithmetic circuits where the conventional approaches failed. |
| Title | Range Equivalent Circuit Minimization |
| Author | *Yung-Chih Chen, Chun-Yao Wang (National Tsing Hua University, Taiwan) |
| Page | pp. 469 - 476 |
| Keyword | range redundant primary input, range-preserving simplification |
| Abstract | Simplifying a combinational circuit while preserving its range has a variety of applications, such as combinational equivalence checking and random simulation. Previous approaches use BDD technique to compute the range of one circuit, and then reconstruct the circuit with the computed range. Although the size of the new circuit is significantly reduced due to the range rearrangement, these methods suffer from the BDD blowup problem for large circuits. Thus, in this paper, we propose a new method to simplify combinational circuits without explicit range computation. We first introduce a new concept of range stuck-at fault test, and show that an untestable range stuck-at fault on a primary input indicates this primary input is range redundant (not responsible for the circuit’s range). We then present a procedure to determine if a given range stuck-at fault on a primary input is untestable. Our method iteratively identifies and removes range redundant primary inputs to simplify a combinational circuit without performing range computation. Accordingly, large circuits that BDD-based methods cannot deal with can be handled. We conduct experiments on a set of ISCAS’85 and MCNC benchmarks. The experimental results show that our approach can minimize circuits such that less number of primary inputs are left. The ratio of our approach and a previous non-BDD-based method over the reduced number of primary inputs is 1.57 on average. |
| Title | Predictive Test Strategy for CMOS RF Mixers |
| Author | *Kay Suenaga, Rodrigo Picos, Sebastia Bota, Miquel Roca, Eugeni Isern, Eugeni Garcia-Moreno (University of Balearic Islands, Spain) |
| Page | pp. 477 - 483 |
| Keyword | CMOS, RF Mixer, Predictive Test, RF Test |
| Abstract | Abstract - In this paper, we present two built-in self-test strategies for the down-converter stage in a GSM receiver. These strategies are based on estimating its performance parameters from measurements in test mode. By using some receiver blocks as part of the test set-up and reusing it, the circuitry overhead is kept small. The first strategy uses the LO signal as the only test stimuli. The second strategy uses additional test circuitry, a generator and an auxiliary mixer. Prediction accuracies are similar in both strategies, but the second one simplifies the measure process of the test observables. |
| Title | Unifying AMBA based Verification Environment at SystemC / RTL / FPGA Levels: Using 3D Graphics SoC As an Example |
| Author | *Wei-Sheng Huang, Ruei-Ting Gu, Ing-Jer Huang (National Sun Yat-Sen University, Taiwan) |
| Page | pp. 484 - 487 |
| Keyword | test-pattern, auto regrssion test, unify, verification environment |
| Abstract | This paper presents an AMBA-based mutual-verification environment that unifies the different level of verification environment. It makes the test-patterns reuse in different verification environment and regression test automation easier. In addition, mutual-verification environment can reduce the verification efforts because the level of verification is raised from cycle-level to program-level. In modern complex IC design, make the verification more efficient could reduce lots of costs and gain a better verification quality dramatically. |
| Title | Hardware/Software Covalidation with FPGA and RTOS Model |
| Author | *Seiya Shibata, Shinya Honda, Yuko Hara, Hiroyuki Tomiyama, Hiroaki Takada (Nagoya University, Japan) |
| Page | pp. 488 - 494 |
| Keyword | Covalidation, FPGA, RTOS, Embedded Systems |
| Abstract | This paper presents a hardware/software covalidation environment for embedded systems. Our covalidation environment consists of a software simulator which simulates a set of application tasks together with an RTOS running on a processor, multiple hardware simulators, FPGA emulators and a covalidation backplane. For shortening validation time, our covalidation environment uses fast RTOS simulation model for software and FPGA for hardware. Using the covalidation environment, we successfully performed covalidation of an MPEG4 decoder system. |
| Title | Pipeline-Aware Instruction-Level Power Analysis for VLIW DSP Core |
| Author | Wen-Tsan Hsieh, Hsin-Ying Liao, *Chien-Nan Jimmy Liu (National Central University, Taiwan), Shu-Yu Cheng, Ji-Jan Chen (SOC Technology Center of Industrial Technological Research Institute, Taiwan) |
| Page | pp. 495 - 499 |
| Keyword | software power model, instruction level power analysis, power model, pipline-aware, VLIW |
| Abstract | In this work, we develop a new instruction-level power analysis approach for pipelined VLIW DSP cores. The proposed approach can take care of both the base power cost and inter-instruction effect cost in each pipeline stage as well as possible, so the power estimation can be much closer to the real pipeline behavior. The experimental results have shown that the average error of our approach is less than 3%. |
| Title | Automatic Generation of Custom Interface Transactors for Verification Environments |
| Author | *Rafael K. Morizawa, Hiroaki Iwashita, Koichiro Takayama (Fujitsu Laboratories, LTD., Japan) |
| Page | pp. 500 - 506 |
| Keyword | Transactor generation, Testbench generation, Protocol checker |
| Abstract | The verification cost of complex SoCs has been increasing in a fast
pace. Thus it is necessary to cut as much as possible any costs that
are not directly associated to the verification task itself.
From our experience, we have noticed that building the
verification environment (also called testbench) is not an easy
task, takes time, and has a negative impact in the overall
verification cost.
The main reason of the complexity of a verification environment lies
in the interfacing between the DUT (Design Under Test) and the
testbench. Although standard interface protocols are available,
custom complex interface protocols are used instead in order to
optimize the hardware's communication throughput and latency.
One way to alleviate this problem is to abstract this interfacing by
using transactors.
In this paper we propose a methodology to automatically generate
transactors. We also present a case study where the proposed
methodology has been used to build the verification environment of a
bus bridge used in a commercial product. |
| Title | Analog Simulation Meets Digital Verification- A Formal Assertion Approach for Mixed-Signal Verification |
| Author | *Alexander Jesser, Lars Hedrich (University of Frankfurt a.M., Germany), Stefan Laemmermann, Roland Weiss, Juergen Ruf, Thomas Kropf, Wolfgang Rosenstiel (University of Tuebingen, Germany), Alexander Pacholik, Wolfgang Fengler (Technical University of Ilmenau, Germany) |
| Page | pp. 507 - 514 |
| Keyword | Analog and mixed-signal design, Verification and simulation, Assertion-based verification, Property specifiction language |
| Abstract | Functional and formal verification are important methodologies for complex mixed-signal designs. But there exists a verification gap between the analog and digital blocks of a mixed-signal system. Our approach improves the verification process by creating mixed-signal assertions which are described by a combination of digital assertions and analog
properties. The proposed method is a new assertion-based verification flow for designing mixed-signal circuits. The effectiveness of the approach is demonstrated on a sigma/delta-converter. |
| Title | Encoding Assertions with Dynamic Local Variables for Bounded Property Checking |
| Author | *Sho Takeuchi, Kiyoharu Hamaguchi, Toshinobu Kashiwabara (Graduate School of Information Science and Technology, Osaka University, Japan) |
| Page | pp. 515 - 521 |
| Keyword | Assertion-Based Verification, Bounded Model Checking, SystemVerilog, Dynamic Local Variable |
| Abstract | To perform functional formal verification, bounded property checking for assertions has been proposed.
However, it is difficult to handle assertions including dynamic local variables such as in SystemVerilog.
In this paper, we assume a restriction for assertions with dynamic local variables that substitution to each dynamic local variable is allowed only once in the assertion at the left-hand side of an implication operator.
Under this restriction, we investigate an algorithm for verifying assertions with one storing variable for each dynamic local variable using bounded property checking.
We implemented the algorithm and performed some experiments. |
| Title | Evaluation of All-Digital PLL by Using Clock-Period Comparator |
| Author | *Yukinobu Makihara, Masayuki Ikebe, Eiichi Sano (Hokkaido University, Japan) |
| Page | pp. 522 - 528 |
| Keyword | digitally controlled PLL, clock-period comparator, loop characteristic |
| Abstract | For a digitally controlled phase-locked loop (PLL), we evaluate the use of a clock-period comparator (CPC).
In this PLL, only the frequency lock operation should be performed; however, the phase lock operation is also simultaneously achieved by performing the clock-period comparison.
In addition, we succeeded in digitizing a voltage controlled oscillator (VCO) with a linear characteristic.
We confirmed a phase lock operation with a slight loop characteristic through SPICE simulation. |
| Title | A Lateral Unified-CBiCMOS Buffer Circuit for Driving 5-nF Maximum Load Capacitance per CCD Clock |
| Author | *Masatoshi Kobayashi, Takashi Hamahata, Toshiro Akino (Kinki University, Japan), Kenji Nishi (Kinki University Technology College, Japan), Cuong Vo Le, Kohsei Takehara, T. Goji Etoh (Kinki University, Japan) |
| Page | pp. 529 - 535 |
| Keyword | Slanted linear CCD storage, ISIS, CMOS/SOI, Lateral unified-CBiCMOS |
| Abstract | Since 2001, we have been developing an in-situ storage image sensor (ISIS) that captures 100 to 150 consecutive images at a frame rate of 1 Mfps and an ultra-high-speed video camera for use with this ISIS. Currently, basic research is continuing in an attempt to increase the frame rate up to 100 Mfps. The CCD chip of this camera has a 10 V maximum voltage supply source and a 5 nF maximum load capacitance per CCD clock. The goal of this study is to design a prototype power supply chip for generating the CCD clock and for driving the load capacitance of the CCD chip. A further goal is to verify the circuit behavior, based on a 1-ìm CMOS/SOI process having breakdown voltages of almost 20 V. A lateral unified-CBiCMOS buffer circuit consists of n- and p-channel MOSFETs that include parasitic lateral npn- and pnp-BJTs having partially depleted p- and n-base layers, respectively, on an epitaxial substrate and SOI. A forward current is applied to the base terminal of the channel MOSFET, adding a normal pull-up or pull-down MOSFET as a current source. A new device structure is designed to reduce the resistance values between the drains and the bases, while also keeping both MOSFETs inactive and activating either the lateral npn or pnp BJT. A clock generator consisting of a ring oscillator with a 21-stage CMOS inverter amplified and driven by a buffer circuit is designed. Circuit simulation using 1-ìm LEVEL-3 model parameters for the MOSFETs and a current gain of âF = 100 for the BJTs reduced the delay time of the unified-CBiCMOS buffer circuit by approximately 1/4, compared to that for an equivalent two-stage CMOS inverter circuit designed on the basis of logical effort for driving a load capacitance of 5 nF at Vdd = 10 V. The power supply chip with the unified-CBiCMOS buffer circuit can drive the CCD chip at a frame rate of 10 Mfps for a maximum 5-nF load capacitance. |
| Title | A CMOS Transconductor with Rail-to-Rail Input Stage under 1.8-V Supply Voltage |
| Author | *Tien-Yu Lo, Cheng-Sheng Kao, Wen-Hung Hsieh, Chung-Chih Hung (National Chiao Tung University, Taiwan) |
| Page | pp. 536 - 539 |
| Keyword | Transconductor, Rail-to-rail |
| Abstract | This paper presents a CMOS low-voltage rail-to-rail transconductor under a supply voltage 1.8-V. Instead of using an n-type and a p-type differential input pair, we use an n-type and a level-shift n-type differential input pair to design a rail-to-rail input stage. Instead of the reported complex structure, a novel level-shift n-type differential input pair is designed to maintain constant transconductance. This work is designed in TSMC 0.18-¨¬m CMOS technology. Results show that the fluctuation of total transconductance of the proposed transconductor is less than ¡À 3%. |
| Title | Charge Recycling between Divided Blocks in MTCMOS Circuits |
| Author | *Akira Tada, Hiromi Notani, Genichi Tanaka, Takashi Ipposhi (Renesas Technology Corporation, Japan), Masaaki Iijima, Masahiro Numa (Kobe University, Japan) |
| Page | pp. 540 - 544 |
| Keyword | power gating, MTCMOS, low power, charge recycling, leak current |
| Abstract | An important issue with MTCMOS circuits is the energy consumption for charging virtual P/G lines during the sleep/active mode transitions. Charge recycling is an effective technique. We propose a technique to reuse more charge by dividing a circuit into several blocks, where the charge is transferred between the properly selected pairs. Assuming ideal situation, we can improve the energy saving ratio up to 63.6% from 50%. The proposed method has improved the ratio by 10.0%, and total power by 7.1%. |
| Title | CoDaMa: An XML-based Framework to Manipulate Control Data Flow Graphs |
| Author | *Shunitsu Kohara, Shi Youhua, Nozomu Togawa, Masao Yanagisawa, Tatsuo Ohtsuki (Waseda University, Japan) |
| Page | pp. 545 - 549 |
| Keyword | CDFG, XML, framework, HW/SW co-synthesis, high-level synthesis |
| Abstract | This paper proposes an XML-based framework to manipulate
CDFGs (Control Data Flow Graphs) for HW/SW (Hardware / Software)
co-synthesis systems or high-level synthesis systems.
With the increased scale of the recent SoC applications,
synthesis systems require implemented more advanced
functions. It would result in increased development efforts.
The developers using our framework can implement algorithm and
construct the systems easily by using XML descriptions as
intermediate representation of application programs and providing the
input/output interface. |