Conclusion and Future Works
6.2 SystemC using Petri Net Modeling
The FSFG representation is commonly used in high-level design, however, the lan-guage based descriptions, such as SystemC [91,92], have more numerous practical applications. SystemC is a modeling platform consisting of C++ class libraries and a simulation kernel for design at the system-behavioral and RTL level. One of the major advantages of SystemC is that it can be used to describe a system at several levels of function description and down to synthesizable RTL. In [93], the authors gave the DSP recommended design flow. In the recommended flow, designs still need refinement or optimization techniques in their design flow. As showing in Figure. 6.6, the verification to check HLS design faults also becomes a challenge work.
D
2D a
a b
b
y (n+2)
u (n+1) u (n)
y (n)
y (n) y (n+2) = a[ a y(n) + b u(n) ] + b u(n+1)
Tmexecuting time
Taexecuting time IPB = 2 (Tm+ Ta) / 2 (a)
D
2D
b ab a2
y (n) u (n)
u (n+1)
(b)
y (n+2) y (n+2) = a2 y(n) + ab u(n) + b u(n+1)
IPB = (Tm+ Ta) / 2
Figure 6.4: (a) Original IIR filter with IP B = 2(Tm + Ta)/2, (b) IP B = (Tm+ Ta)/2 after lookahead
D
Figure 6.5: Applying M − 1 steps IIR filter of the lookahead design in previous case, with IP B = (Tm+ Ta)/M
HLS is crucial for the success of the design, the verification for HLS is even a challenge work. Except low level technique, HLS still dominates the performance of a system. PN based verification open the way to the development of the HLS formal verification techniques. We hope PN based verification method can handle more complex design in the future.
C algorithm
Matlab design
SystemC Behavior
Software - FW SystemC RTL
Verilog
Compile
Gate level simulation
Equivalence checking Synthesized
High-level optimization
HLS verification
System level
RTL / gate level
HLS optimization Abstraction
Implementation
Figure 6.6: System-level design flow and the PN-based verification
References
[1] Rolf Drechsler, “Towards formal verification on the system level”, Proceed-ings of the 15th IEEE International Workshop on Rapid System Prototyping, vol. 28, no. 30, pp. 2–5, jun 2004.
[2] Alan John Hu and Andrew K. Martin, Formal Methods In Computer-aided Design, Springer, 2004.
[3] William K. Lam, Hardware Design Verification: Simulation and Formal Method-Based Approaches, Prentice Hall, 2005.
[4] Carl Pixley, “Guest editor’s introduction: Formal verification of commercial integrated circuits”, IEEE Design and Test, vol. 18, no. 4, pp. 4–5, jul 2001.
[5] Vigyan Singhal, Carl Pixley, Adnan Aziz, and Robert K. Brayton, “The-ory of safe replacements for sequential circuits”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 20, no. 2, pp. 249–265, feb 2001.
[6] Aarti Gupta, “Formal hardware verification methods: a survey”, Formal Methods in System Design, vol. 1, no. 2-3, pp. 151–238, oct 1992.
[7] Christoph Kern and Mark R. Greenstreet, “Formal verification in hardware design: a survey”, ACM Transactions on Design Automation of Electronic Systems (TODAES), vol. 4, no. 2, pp. 123–193, apr 1999.
[8] Randal E. Bryant and James H. Kukula, “Formal methods for functional verification”, International Conference on Computer-Aided Design (IC-CAD), 2002.
[9] Jun Yuan, Carl Pixley, Adnan Aziz, and Ken Albin, “A framework for constrained functional verification”, International Conference on Computer Aided Design, pp. 142–145, nov 2003.
[10] Edmund M. Clarke, Orna Grumberg, and Doron A. Peled, Model Checking, MIT Press, 1999.
[11] Kedar S. Namjoshi and E. Allen Emerson, Verification, Model Checking, And Abstract Interpretation, Springer, 2006.
[12] Tsung-Hsi Chiang and Lan-Rong Dung, “System level verification on high-level synthesis of dataflow algorithms using Petri net”, WSEAS Transactions on Circuits and Systems, vol. 5, no. 6, pp. 790–796, 2006.
[13] Tsung-Hsi Chiang and Lan-Rong Dung, “Verification method of dataflow algorithms in high-level synthesis”, Journal of System and Software, vol. 80, no. 8, pp. 1256–1270, 2007.
[14] Tsung-Hsi Chiang and Lan-Rong Dung, “On verification on dataflow scheduling”, to be appeared in International Journal of Software Engineering and Knowledge Engineering, 2007.
[15] Tsung-Hsi Chiang and Lan-Rong Dung, “Hybrid verification technique for high-level synthesis of dataflow algorithms”, WSEAS Transactions on Cir-cuits and Systems, vol. 6, no. 3, pp. 348–354, 2007.
[16] Tsung-Hsi Chiang and Lan-Rong Dung, “Modeling and formal verification of dataflow graph in system-level design using Petri net”, IEEE International Symposium on Circuits and Systems (ISCAS 2005), 2005.
[17] Tsung-Hsi Chiang and Lan-Rong Dung, “System-level verification of dataflow graph using Petri net model”, 16th VLSI Design/CAD Taiwan, 2005.
[18] Tsung-Hsi Chiang and Lan-Rong Dung, “System-level verification on high-level synthesis of dataflow graph”, IEEE International Symposium on Cir-cuits and Systems (ISCAS 2006), 2006.
[19] Karl S. Brace, Richard L. Rudell, and Randal E. Bryant, “Efficient imple-mentation of a BDD package”, Proceedings of the 27th ACM/IEEE confer-ence on Design automation, pp. 40–45, 1991.
[20] Randal E. Bryant, “Symbolic Boolean manipulation with ordered binary-decision diagrams”, ACM Computing Surveys, vol. 24, no. 3, pp. 293–318, sep 1992.
[21] Randal E. Bryant, “Graph-based algorithms for Boolean function manipu-lation”, IEEE Transactions on Computers, vol. 35, no. 8, pp. 677–691, aug 1986.
[22] Rolf. Drechsler, Rudiger Ebendt, and Gorschwin Fey, Advanced BDD Opti-mization, Springer, 2005.
[23] Ruy J. G. B. de Queiroz, Logic for Concurrency and Synchronisation, Springer, 2003.
[24] Jun Yuan, Kurt Shultz, Carl Pixley, Hillel Miller, and Adnan Aziz, “Model-ing design constraints and bias“Model-ing in simulation us“Model-ing BDDs”, IEEE/ACM International Conference on Computer-Aided Design, pp. 584–589, 1999.
[25] Kenneth L. McMillan, “Applying SAT methods in unbounded symbolic model checking”, 14th International Conference on Computer Aided Verifi-cation, pp. 250–264, jul 2002.
[26] G. Parthasarathy, K-T. Cheng, and C-Y Huang, “An analysis of ATPG and SAT algorithms for formal verification”, Proceedings of the Sixth IEEE International High-Level Design Validation and Test Workshop (HLDVT
’01), pp. 177–182, 2001.
[27] Mukul R. Prasad, Armin Biere, and Aarti Gupta, “A survey of recent advances in SAT-based formal verification”, Software Tools for Technology Transfer, vol. 7, no. 2, pp. 156–173, 2005.
[28] J. R. Burch, E. M. Clarke, and D. E. Long, “Symbolic model checking with partitioned transition relations”, Proceeding of International Conference on Very Large Scale Integration, , no. 49–58, 1991.
[29] Jerry R. Burch, Edmund M. Clarke, David E. Long, Kenneth L. McMillan, and David L. Dill, “Symbolic model checking for sequential circuit verifica-tion”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 13, no. 4, pp. 401–424, apr 1994.
[30] Hyeong-Ju Kang and In-Cheol Park, “SAT-based unbounded symbolic model checking”, IEEE Transactions on Computer-Aided Design of Inte-grated Circuits and Systems, vol. 24, no. 2, pp. 129–140, feb 2005.
[31] Ganapathy Parthasarathy, Madhu K. Iyer, Kwang-Ting Cheng, and Li-C.
Wang, “Safety property verification using sequential sat and bounded model checking”, IEEE Design and Test of Computers, vol. 21, no. 2, pp. 132–143, mar 2004.
[32] J. R. Burch, E. M. Clarke, K. L. McMillan, and D. L. Dill, “Sequential circuit verification using symbolic model checking”, In 27th ACM/IEEE Design Automation Conference, 1990.
[33] Edmund M. Clarke and David E. Long, “Model checking and abstraction”, ACM Transactions on Programming Languages and Systems, 1992.
[34] Matt Kaufmann, Andrew Martin, and Carl Pixley, “Design constraints in symbolic model checking”, Proceedings of the 10th International Conference on Computer Aided Verification, vol. 1427, pp. 477–487, 1998.
[35] Joseph Kljaich, Brian T. Smith, and Anthony S. Wojcik, “Formal verifica-tion of fault tolerance using theorem-proving techniques”, IEEE Transac-tions on Computers, vol. 38, no. 3, pp. 366–376, mar 1989.
[36] Mark D Ryan and Michael Huth, Logic in Computer Science: Modelling and Reasoning about Systems, Cambridge University Press, 2004.
[37] Pranav Ashar, Subhrajit Bhattacharya, Anand Raghunathan, and Akira Mukaiyama, “Verification of RTL generated from scheduled behavior in a high-level synthesis flow”, Proceedings of the 1998 IEEE/ACM international conference on Computer-aided design, pp. 517–524, 1998.
[38] D. Sarkar, “Register transfer operation analysis during data path verifi-cation”, Proceedings of the 2002 conference on Asia South Pacific design automation / VLSI Design, pp. 172–177, jan 2002.
[39] C. Bolchini, R. Montandon, F. Salice, and D. Sciuto, “Design of VHDL-based totally self-checking finite-state machine anddata-path descriptions”, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 8, no. 1, pp. 98–103, feb 2000.
[40] Dominique Borrione, Julia Dushina, and Laurence Pierre, “A compositional model for the functional verification of high-levelsynthesis results”, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 8, no. 5, pp. 526–530, oct 2000.
[41] C Karfa, C Mandal, D Sarkar, S R. Pentakota, and Chris Reade, “A formal verification method of scheduling in high-level synthesis”, Proceedings of the 7th International Symposium on Quality Electronic Design, pp. 71–78, 2006.
[42] Nazanin Mansouri and Ranga Vemuri, “Automated correctness condition generation for formal verification of synthesized RTL designs”, Journal of Formal Methods in System Design, vol. 16, no. 1, pp. 59–91, jan 2000.
[43] Daniel D. Gajski and Loganath Ramachandran, “Introduction to high-level synthesis”, IEEE Design and Test, vol. 11, no. 4, pp. 44–54, oct 1994.
[44] Luciano Lavagno, Grant Martin, and Louis Scheffer, Electronic Design Au-tomation for Integrated Circuits Handbook, CRC, 2006.
[45] Daniel Gajski, Nikil Dutt, Allen Wu, and Steve Lin, High-level synthesis : introduction to chip and system design, Kluwer academic publishers, 1992.
[46] Daniel Gajski and Robert H. Kuhn, “New VLSI tools - guest editors’ intro-duction”, IEEE Computer, vol. 16, no. 12, pp. 11–14, 1983.
[47] Donald E. Thomas, Elizabeth D. Lagnese, Robert A. Walker, Jayanth V.
Rajan, Robert L. Blackburn, and John A. Nestor, Algorithmic and Register-Transfer Level Synthesis: The System Architect’s Workbench, Springer, 1989.
[48] Giovanni De Micheli, Synthesis and optimization of digital circuits, McGraw-Hill, 1994.
[49] Keshab K. Parhi, VLSI Digital Signal Processing Systems: Design and Im-plementation, Wiley, 1999.
[50] Vijay K. Madisetti, VLSI Digital Signal Processors, IEEE Press, 1995.
[51] A. Fettweis, “Realizability of digital filter networks”, Archiv fur Elektronik und Ubertragungstechnik, vol. 30, no. 2, pp. 90–96, 1976.
[52] Markku Renfors and Yrjo Neuvo, “Fast multiprocessor realizations of digital filters”, IEEE International Conference on ICASSP’80 Acoustics, Speech, and Signal Processing, vol. 5, pp. 916–919, apr 1980.
[53] Thomas P. Barnwell, C.J.M. Hodges, and Mark Randolph, “Optimum im-plementation of single time index signal flow graphs on synceronous multi-processor machines”, IEEE International Conference on ICASSP’82 Acous-tics, Speech, and Signal Processing, vol. 7, pp. 679–682, aug 1982.
[54] T. Barnwell, C. Hodges, and M. Randolph, “Optimum implementation of single time index signal flow graphs on synceronous multiprocessor ma-chines”, IEEE International Conference on ICASSP’82 Acoustics, Speech, and Signal Processing, vol. 7, pp. 679–682, 1982.
[55] C. E. Leiserson and J. B. Saxe, “Optimizing synchronous systems”, Journal of VLSI and Computer Systems, vol. 1, no. 1, pp. 41–67, 1983.
[56] Charles E. Leiserson and James B. Saxe, “Retiming synchronous circuitry”, Algorithmica, vol. 6, no. 1, pp. 5–35, 1991.
[57] Alexander Schrijver, Theory of Linear and Integer Programming, John Wiley and Sons, 1998.
[58] Cheng-Tsung Hwang, Jiahn-Hurng Lee, and Yu-Chin Hsu, “A formal ap-proach to the scheduling problem in high level synthesis”, IEEE Transac-tions on Computer-Aided Design of Integrated Circuits and Systems, vol. 10, no. 4, pp. 464–475, apr 1991.
[59] Keshab K. Parhi and David G. Messerschmitt, “Static rate-optimal schedul-ing of iterative data-flow programs via optimum unfoldschedul-ing”, IEEE Transac-tions on Computers, vol. 40, no. 2, pp. 178–195, feb 1991.
[60] Keshab K. Parhi, “Algorithm transformations for concurrent processors”, In Proceedings of the IEEE, vol. 77, no. 12, pp. 1879–1895, dec 1989.
[61] Liang-Fang Chao and Edwin Hsing-Mean Sha, “Scheduling data-flow graphs via retiming and unfolding”, IEEE Transactions on Parallel and Distributed Systems, vol. 8, no. 12, pp. 1259–1267, dec 1997.
[62] Nikil D. Dutt and Daniel D. Gajski, “Design synthesis and silicon compila-tion”, IEEE Design and Test, vol. 7, no. 6, pp. 8–23, nov 1990.
[63] Pierre G. Paulin and John P. Knight, “Algorithms for high-level synthesis”, IEEE Design and Test, vol. 6, no. 6, pp. 18–31, nov 1989.
[64] Robert A. Walker and Samit Chaudhuri, “Introduction to the scheduling problem”, IEEE Design and Test, vol. 12, no. 2, pp. 60–69, jun 1995.
[65] Carl Adam Petri, Communication with automata, PhD thesis, University of Bonn, 1966.
[66] James L. Peterson, Petri net theory and the modeling of system, Prentice-Hall, 1981.
[67] Tadao Murata, “Petri nets: properties, analysis and applications”, Proceed-ings of the IEEE, vol. 77, no. 4, pp. 541–580, apr 1989.
[68] Christos G. Cassandras and Stephane Lafortune, Introduction to Discrete Event Systems, Kluwer Academic Publishers, 1999.
[69] Rene David and Hassane Alla, Petri Nets and Grafcet: tools for modelling discrete event systems, Prentice Hall International, 1992.
[70] Wolfgang Reisig and Grzegorz Rozenberg, Lectures on Petri nets I: Basic Models, Springer, 1998.
[71] Wolfgang Reisig and Grzegorz Rozenberg, Advances in Petri Nets - Lectures on Petri nets II: Applications, Springer, dec 1998.
[72] Jorg Desel, Wolfgang Reisig, and Grzegorz Rozenberg, Lectures on Concur-rency and Petri Nets, Springer, 2004.
[73] Grzegorz Rozenberg, Advances in Petri Nets 1984, 1986, 1988, 1990 - Lec-ture Notes in Computer Science, Springer, 1984.
[74] Lan-Rong Dung and Hsueh-Chih Yang, “On multiple-voltage high-level syn-thesis using algorithmic transformations”, dec 2004, number 12, pp. 3100–
3108.
[75] Claude Girault and Rudiger Valk, Petri nets for systems engineering, Springer, 2003.
[76] Harvey E. Rose, Linear Algebra: A Pure Mathematical Approach, Springer, 2002.
[77] Kazuhito Ito, Lori E. Lucke, and Keshab K. Parhi, “ILP-based cost-optimal DSP synthesis with module selection and dataformat conversion”, IEEE Transactions on Very Large Scale Integration (VLSI) Systems, vol. 6, no. 4, pp. 582–594, dec 1998.
[78] Vijay K. Madisetti and Bryce A. Curtis, “A quantitative methodology for rapid prototyping and high-levelsynthesis of signal processing algorithms”, IEEE Transactions on Signal Processing, vol. 42, no. 11, pp. 3188–3208, nov 1994.
[79] Keshab K. Parhi, “High-level algorithm and architecture transformations for DSP synthesis”, Journal of VLSI Signal Processing Systems, vol. 9, no.
1-2, pp. 121–143, jan 1995.
[80] Xun Liu, Papaefthymiou, Marios C. Papaefthymiou, and Eby G. Friedman,
“Retiming and clock scheduling for digital circuit optimization”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 21, no. 2, pp. 184–203, feb 2002.
[81] George A. Constantinides, Peter Y. K. Cheung, and Wayne Luk, “Optimum and heuristic synthesis of multiple word-length architectures”, IEEE Trans-actions on Very Large Scale Integration (VLSI) Systems, vol. 13, no. 1, pp.
39–57, jan 2005.
[82] Michael R. Garey and David S. Johnson, Computers and Intractability: A Guide to the Theory of NP-Completeness, W.H. Freeman, 1990.
[83] Lintao Zhang and Sharad Malik, “The quest for efficient Boolean satisfiabil-ity solvers”, Proceedings of the 14th International Conference on Computer Aided Verification, pp. 17–36, jul 2002.
[84] Tracy Larrabee, “Test pattern generation using Boolean satisfiability”, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 11, no. 1, pp. 4–15, jan 1992.
[85] Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang, and Sharad Malik, “Chaff: engineering an efficient SAT solver”, Proceedings of Design Automation Conference, pp. 530–535, 2001.
[86] J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. G. Hwang,
“Symbolic model checking 10exp20 states and beyond”, In Logic in Com-puter Science, pp. 428–439, 1990.
[87] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, and Y. Zhu, “Symbolic model checking using SAT procedures instead of BDDs”, Proceedings of the 36th ACM/IEEE conference on Design automation, pp. 317–320, 1999.
[88] Edmund M. Clarke and E. Allen Emerson, “Design and synthesis of synchro-nization skeletons using branching time temporal logic”, in Lecture Notes In Computer Science. 1981, vol. 131, pp. 52–71, Springer-Verlag.
[89] Keshab K. Parhi and David G. Messerschmitt, “Pipelined VLSI recursive filter architectures using scattered look-ahead and decomposition”, Interna-tional Conference on Acoustics, Speech, and Signal Processing (ICASSP-88), vol. 4, pp. 2120–2123, apr 1988.
[90] Keshab K. Parhi and David G. Messerschmitt, “Pipeline interleaving and parallelism in recursive digital filters.i. pipelining using scattered look-ahead and decomposition”, IEEE Transactions on Acoustics, Speech, and Signal Processing, vol. 37, no. 7, pp. 1099–1117, jul 1989.
[91] ”, SystemC community, http://www.systemc.org/.
[92] “SystemC version 2.0 users guide”, Synopsys Inc, 2003.
http://www.systemc.org/.
[93] Itai Yarom and Gabi Glasser, “SystemC opportunities in chip design flow”, Proceedings of the 2004 11th IEEE International Conference on Electronics, Circuits and Systems ICECS 2004, vol. 13, no. 15, pp. 507–510, 2004.