[go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

From high-level modeling toward efficient and trustworthy circuits

  • Regular Paper
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

Behavior–interaction–priority (BIP) is a layered embedded system design and verification framework that provides separation of functionality, synchronization, and priority concerns to simplify system design and to establish correctness by construction. BIP framework comes with a runtime engine and a suite of verification tools that use D-Finder and NuSMV as model-checkers. In this paper, we provide a method and a supporting tool that take a BIP system and a set of invariants and compute a reduced sequential circuit with a system-specific scheduler and a designated output that is \(\mathtt {true}\) when the invariants hold. Our method uses ABC, a sequential circuit synthesis and verification framework, to (1) generate an efficient circuit implementation of the system that can be readily translated into FPGA or ASIC implementations and to (2) verify the system and debug it in case a counterexample is found. Moreover, we generate a concurrent C implementation of the circuit that can be directly used for runtime verification. We evaluated our method with two benchmark systems, and our results show that, compared to existing techniques, our method is faster and scales to larger sizes.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16
Fig. 17

Similar content being viewed by others

Notes

  1. The BIP engine implementing this semantics chooses one interaction at random, when faced with several enabled interactions.

References

  1. Abdellatif, T., Combaz, J., Sifakis, J.: Rigorous implementation of real-time systems—from theory to application. Math. Struct. Comput. Sci. 23(4), 882–914 (2013)

    Article  MathSciNet  MATH  Google Scholar 

  2. Amla, N., Du, X., Kuehlmann, A., Kurshan, R.P., McMillan, K.L.: An analysis of sat-based model checking techniques in an industrial environment. In: Borrione, D., Paul, W. (eds.) Correct Hardware Design and Verification Methods, pp. 254–268. Springer, Berlin, Heidelberg (2005)

    Chapter  Google Scholar 

  3. Aziz, A., Shiple, T., Singhal, V., Brayton, R., Sangiovanni-Vincentelli, A.: Formula dependent equivalence for compositional CTL model checking. J. Form. Methods Syst. Des. 21(2), 193–224 (2002)

    Article  MATH  Google Scholar 

  4. BIP Website. http://www-verimag.imag.fr/Rigorous-Design-of-Component-Based.html

  5. Balarin, F., Watanabe, Y., Hsieh, H., Lavagno, L., Passerone, C., Sangiovanni-Vincentelli, A.L.: Metropolis: an integrated electronic system design environment. IEEE Comput. 36(4), 45–52 (2003)

    Article  Google Scholar 

  6. Barnat, J., Brim, L., Havel, V.: LTL model checking of parallel programs with under-approximated TSO memory model. In: International Conference on Application of Concurrency to System Design (ACSD), pp. 51–59 (2013)

  7. Barnat, J., Brim, L., Safránek, D.: High-performance analysis of biological systems dynamics with the DiVinE model checker. Brief. Bioinform. 11(3), 301–312 (2010)

    Article  Google Scholar 

  8. Basu, A., Bensalem, S., Bozga, M., Combaz, J., Jaber, M., Nguyen, T.-H., Sifakis, J.: Rigorous component-based system design using the BIP framework. IEEE Softw. 28(3), 41–48 (2011)

    Article  Google Scholar 

  9. Basu, A., Bidinger, P., Bozga, M., Sifakis, J.: Distributed semantics and implementation for systems with interaction and priority. In: Formal Techniques for Networked and Distributed Systems—FORTE 2008, 28th IFIP WG 6.1 International Conference, Tokyo, Japan, June 10–13, 2008, Proceedings, pp. 116–133 (2008)

  10. Baumgartner, J., Kuehlmann, A., Abraham, J.: Property checking via structural analysis. In: Brinksma, E., Larsen, K.G. (eds.) Computer-Aided Verification. Springer, Berlin, Heidelberg (2002)

    Google Scholar 

  11. Bensalem, S., Bozga, M., Legay, A., Nguyen, T.-H., Sifakis, J., Yan, R.: Component-based verification using incremental design and invariants. Softw. Syst. Model. 15, 427–451 (2014)

    Article  Google Scholar 

  12. Bensalem, S., Bozga, M., Nguyen, T.-H., Sifakis, J.: D-Finder: a tool for compositional deadlock detection and verification. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification Volume 5643 of Lecture Notes in Computer Science, pp. 614–619. Springer, Berlin (2009)

    Google Scholar 

  13. Berezin, S., Campos, S., Clarke, E.M.: Compositional Reasoning in Model Checking. Springer, Berlin (1998)

    Book  Google Scholar 

  14. Biere, A.: Handbook of Satisfiability, vol. 185. IOS Press, Amsterdam (2009)

    MATH  Google Scholar 

  15. Bjesse, P., Boralv, A.: DAG-aware circuit compression for formal verification. In: International Conference on Computer-Aided Design (2004)

  16. Bjesse, P., Boralv, A.: Dag-aware circuit compression for formal verification. In: Proceedings of the 2004 IEEE/ACM International Conference on Computer-Aided Design, pp. 42–49. IEEE Computer Society (2004)

  17. Bjesse, P., Claessen, K.: SAT-based verification without state space traversal. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Formal Methods in Computer-Aided Design. Springer, Berlin, Heidelberg (2000)

  18. Bonakdarpour, B., Bozga, M., Jaber, M., Quilbeuf, J., Sifakis, J.: A framework for automated distributed implementation of component-based models. Distrib. Comput. 25(5), 383–409 (2012)

    Article  MATH  Google Scholar 

  19. Bradley, A.R.: Sat-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) Verification, Model Checking, and Abstract Interpretation, pp. 70–87. Springer, Berlin, Heidelberg (2011)

    Chapter  Google Scholar 

  20. Bradley, A.R., Manna, Z.: Checking safety by inductive generalization of counterexamples to induction. In: Formal Methods in Computer Aided Design, 2007: FMCAD’07, pp. 173–180. IEEE (2007)

  21. Brayton, R., Mishchenko, A.: ABC: an academic industrial-strength verification tool. In: Touili, T., Cook, B., Jackson, P. (eds.) Computer Aided Verification, pp. 24–40. Springer, Berlin, Heidelberg (2010)

    Chapter  Google Scholar 

  22. Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: \(10^{20}\) states and beyond. Inf. Comput. 98(2), 142–170 (1992)

    Article  MATH  Google Scholar 

  23. Burnim, J., Sen, K.: Heuristics for scalable dynamic test generation. In: 23rd IEEE/ACM International Conference on Automated Software Engineering (ASE 2008), 15–19 September 2008, L’Aquila, Italy, pp. 443–446. IEEE (2008)

  24. Bybell, T.: Gtkwave electronic waveform viewer (2010). http://gtkwave.sourceforge.net

  25. Chaudron, M.R.V., Eskenazi, E.M., Fioukov, A.V., Hammer, D.K.: A framework for formal component-based software architecting. In: OOPSLA, pp. 73–80 (2001)

  26. Cimatti, A., Clarke, E., Giunchiglia, F., Roveri, M.: NUSMV: a new symbolic model checker. Int. J. Softw. Tools Technol. Transf. 2(4), 410–425 (2000)

    Article  MATH  Google Scholar 

  27. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (1999)

    Google Scholar 

  28. Davare, A., Densmore, D., Guo, L., Passerone, R., Sangiovanni-Vincentelli, A.L., Simalatsar, A., Zhu, Q.: metroII: a design environment for cyber-physical systems. ACM Trans. Embed. Comput. Syst. 12(1s), 49 (2013)

    Article  Google Scholar 

  29. Dutertre, B., De Moura, L.: A fast linear-arithmetic solver for dpll (t). In: Ball, T., Jones, R.B. (eds.) Computer Aided Verification, pp. 81–94. Springer, Berlin, Heidelberg (2006)

    Chapter  Google Scholar 

  30. Een, N., Mishchenko, A., Brayton, R.: Efficient implementation of property directed reachability. In: Formal Methods in Computer-Aided Design (FMCAD), 2011, pp. 125–134. IEEE (2011)

  31. Eén, N., Sörensson, N.: Temporal induction by incremental sat solving. Electron. Notes Theor. Comput. Sci. 89(4), 543–560 (2003)

    Article  MATH  Google Scholar 

  32. Falcone, Y., Havelund, K., Reger, G.: A tutorial on runtime verification. In: Broy, M., Peled, D.A., Kalus, G. (eds.) Engineering Dependable Software Systems, Volume 34 of NATO Science for Peace and Security Series, D: Information and Communication Security, pp. 141–175. IOS Press, Amsterdam (2013)

    Google Scholar 

  33. Falcone, Y., Jaber, M., Nguyen, T.-H., Bozga, M., Bensalem, S.: Runtime verification of component-based systems in the BIP framework with formally-proved sound and complete instrumentation. Softw. Syst. Model. 14(1), 173–199 (2015)

    Article  Google Scholar 

  34. Gafni, E., Lamport, L.: Disk paxos. Distrib. Comput. 16(1), 1–20 (2003)

    Article  MATH  Google Scholar 

  35. Guerraoui, R., Kuncak, V., Losa, G.: Speculative linearizability. ACM Sigplan Not. 47(6), 55–66 (2012)

    Article  Google Scholar 

  36. Henzinger, T.A., Sifakis, J.: The embedded systems design challenge. In: Misra, J., Nipkow, T., Sekerinski, E. (eds.) FM 2006: Formal Methods, pp. 1–15. Springer, Berlin, Heidelberg (2006)

    Google Scholar 

  37. Ho, P.-H., Shiple, T., Harer, K., Kukula, J., Damiano, R., Bertacco, V., Taylor, J., Long, J.: Smart simulation using collaborative formal and simulation engines. In: International Conference on Computer-Aided Design (2000)

  38. Holzmann, G.: The model checker SPIN. IEEE Trans. Softw. Eng. 23, 279–295 (1997)

    Article  Google Scholar 

  39. Hurst, A.P., Mishchenko, A., Brayton, R.K.: Fast minimum-register retiming via binary maximum-flow. In: Formal Methods in Computer Aided Design, 2007. FMCAD’07, pp. 181–187. IEEE (2007)

  40. Jaber, M.: Centralized and Distributed Implementations of Correct-by-construction Component-based Systems by using Source-to-source Transformations in BIP. (Implémentations Centralisée et Répartie de Systèmes Corrects par construction à base des Composants par Transformations Source-à-source dans BIP). PhD thesis, Joseph Fourier University, Grenoble, France (2010)

  41. Kuehlmann, A., Baumgartner, J.: Transformation-based verification using generalized retiming. In: Berry, G., Comon, H., Finkel, A. (eds.) Computer-Aided Verification. Springer, Berlin, Heidelberg (2001)

    Google Scholar 

  42. Kuehlmann, A., Ganai, M., Paruthi, V.: Circuit-based Boolean reasoning. In: Design Automation Conference, pp. 232–237 (2001)

  43. Mony, H., et al.: Scalable automated verification via expert-system guided transformations. In: Hu, A.J., Martin, A.K. (eds.) Formal Methods in Computer-Aided Design. Springer, Berlin, Heidelberg (2004)

    Google Scholar 

  44. McMillan, K.L.: Interpolation and sat-based model checking. In: Hunt, W.A. Jr., Somenzi, F. (eds.) CAV, Volume 2725 of Lecture Notes in Computer Science, pp. 1–13. Springer, Berlin (2003)

  45. Mishchenko, A., Case, M., Brayton, R., Jang, S.: Scalable and scalably-verifiable sequential synthesis. In: IEEE/ACM International Conference on Computer-Aided Design, 2008. ICCAD 2008, pp. 234–241. IEEE (2008)

  46. Mishchenko, A., Chatterjee, S., Brayton, R.: Dag-aware AIG rewriting a fresh look at combinational logic synthesis. In: Proceedings of the 43rd Annual Design Automation Conference, pp. 532–535. ACM (2006)

  47. Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R.: Exploiting suspected redundancy without proving it. In: Design Automation Conference. ACM Press (2005)

  48. Mony, H., Baumgartner, J., Paruthi, V., Kanzelman, R.: Exploiting suspected redundancy without proving it. In: Proceedings of the 42nd Annual Design Automation Conference, pp. 463–466. ACM (2005)

  49. Moon, I.-H., Hachtel, G.D., Somenzi, F.: Border-block triangular form and conjunction schedule in image computation. In: Hunt, W.A. Jr., Johnson, S.D. (eds.) Formal Methods in Computer-Aided Design. Springer, Berlin, Heidelberg (2000)

  50. Moskewicz, M.W., Madigan, C.F., Zhao, Y., Zhang, L., Malik, S.: Chaff: engineering an efficient SAT solver. In: ACM Design Automation Conference (2001)

  51. Nguyen, T.-H.: Constructive Verification for Component-Based Systems. University of Grenoble, Grenoble (2010)

    Google Scholar 

  52. Niaki, S.H.A., Sander, I.: An automated parallel simulation flow for heterogeneous embedded systems. In: Design, Automation and Test in Europe (DATE), pp. 27–30 (2013)

  53. Noureddine, M., Jaber, M., Bliudze, S., Zaraket, F.A.: Reduction and abstraction techniques for BIP. In: Lanese, I., Madelaine, E. (eds.) Formal Aspects of Component Software (FACS). Springer, Cham (2014)

    Google Scholar 

  54. Panda, P.R.: Systemc: a modeling platform supporting multiple design abstractions. In: Proceedings of the 14th International Symposium on Systems Synthesis. ISSS ’01, pp. 75–80. ACM, New York, NY, USA (2001)

  55. Potop-Butucaru, D., Edwards, S.A., Berry, G.: Compiling Esterel. Springer, Berlin (2007)

    Google Scholar 

  56. Qiang, W., Bliudze, S.: Verification of component-based systems via predicate abstraction and simultaneous set reduction. In: Trustworthy Global Computing—10th International Symposium, TGC 2015, Madrid, Spain, August 31–September 1, 2015 Revised Selected Papers, pp. 147–162 (2015)

  57. Sander, I., Jantsch, A.: System modeling and transformational design refinement in forsyde. IEEE Trans. CAD (TCAD) Integr. Circuits Syst. 23(1), 17–32 (2004)

    Article  Google Scholar 

  58. Sentovich, E., Singh, K.J., Moon, C.W., Savoj, H., Brayton, R.K., Sangiovanni-Vincentelli, A.L.: Sequential circuit design using synthesis and optimization. In: ICCD, pp. 328–333. IEEE Computer Society (1992)

  59. Sipser, M.: Introduction to the Theory of Computation, vol. 27. Thomson Course Technology, Boston (2006)

    MATH  Google Scholar 

  60. Wang, D.: SAT Based Abstraction Refinement for Hardware Verification. PhD thesis, Carnegie Mellon University (2003)

Download references

Author information

Authors and Affiliations

  1. American University of Beirut, Beirut, Lebanon

    Fadi A. Zaraket & Mohamad Jaber

  2. Performability Engineering Research Group, University of Illinois at Urbana-Champaign, Urbana, IL, USA

    Mohamad Noureddine

  3. Laboratoire d’Informatique de Grenoble, Univ. Grenoble-Alpes, Inria, 38000, Grenoble, France

    Yliès Falcone

Authors
  1. Fadi A. Zaraket
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Mohamad Jaber
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mohamad Noureddine
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yliès Falcone
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Mohamad Jaber.

Additional information

The first two authors contributed equally to this work.

Appendix A: ABC reduction and verification techniques

Appendix A: ABC reduction and verification techniques

The ABC framework provides a set of algorithms that can be applied iteratively to (1) reduce the AIG into an equivalent AIG and (2) verify that a designated output of an AIG is always true. In what follows, we provide brief descriptions of several reduction and verification ABC algorithms.

1.1 A.1: Structural register sweep (SRS)

SRS detects registers that are stuck at constant and eliminates them from a given sequential AIG circuit. The technique starts by zeroing up all initial values of registers in the circuit. It then uses the ternary simulation algorithm in order to detect stuck-at-constant registers. The algorithm starts from the initial values of the registers and simulates the circuit using x values for the circuit’s primary inputs. The simulation algorithm stops when a new ternary state is equal to a previously computed ternary state. In this case, any register having the same constant value at each reachable ternary state will be declared to be stuck at constant and thus eliminated. The structural sweeping algorithm stop when no further reduction in the number of registers is possible [45].

1.2 A.2: Signal correspondence (Scorr)

Scorr uses k-step induction in order to detect and merge sets of classes of sequentially equivalent nodes [45]. The base case for this algorithm is that the equivalence between the classes holds for the first k frames, and the inductive case is that given the base case, starting from any state, the equivalence holds in the \((k+1)\mathrm{st}\) state. Key to the signal correspondence algorithm is the way the candidate equivalences are assumed for the base case. Abc implements speculative reduction, originally presented in [48], which merges, but does not remove, any node of an equivalence class onto its representative, in each of the first k time frames. Instead of removing the merged node, a constraint is added to assert that the node and its representative are equal. This technique is claimed to decrease the number of constraints added to the SAT solved for induction.

1.3 A.3: Rewriting

Rewriting aims at finding nodes in a directed acyclic graph (DAG) where by replacing subgraphs rooted at these nodes by pre-computed subgraphs can introduce important reductions in the DAG size, while keeping the functionality of these nodes intact. The algorithm traverses the DAG in depth-first post-order and gives a score for each root node. The score represents the number of nodes that would result from performing a rewrite at this node. If a rewrite exists such that the size of the DAG is decreased, such a rewrite is performed and scores are recomputed accordingly. Rewriting has been proposed initially in [16], targeted for Reduced Boolean circuits (RBC); it was later implemented and improved for ABC in [46].

1.4 A.4: Retiming

Retiming a sequential circuit is a standard technique used in sequential synthesis, aiming at the relocation of the registers in the circuit in order to optimize some of the circuit characteristics. Retiming can either target the minimization of the delay in the circuit, or the minimization of the number of registers given a delay constraint, or the unconstrained minimization of the number of registers in the circuit. It does so while keeping the output functionality of the circuit intact [39]

1.5 A.5: Property directed reachability (Pdr)

The Pdr algorithm aims at proving that no violating state is reachable from the initial state of a given AIG network. It maintains a trace representing a list of over-approximations of the states reachable from the initial state, along with a set of proof obligations, which can be a set of bad states or a set of states from which a bad state is reachable. Given the trace and the set of obligations, the Pdr algorithm manipulates them and keeps on adding facts to the trace until either an inductive invariant is reached and the property is proved, or a counterexample is found (a bad state is proven to be reachable). The algorithm was originally developed by Aaron Bradley in [19, 20] and was later improved by Een et al in [30].

1.6 A.6: Temporal induction

Temporal induction carries an inductive proof of the property over the time steps of a sequential circuit. Similar to a standard inductive proof, it consists of a base case and an inductive hypothesis. These steps are typically expressed as SAT problems to be solved by traditional SAT solvers. k-step induction strengthens simple temporal inductive proofs by assuming that the property holds for the first k time steps (states), i.e., a longer base case needs to be proven [31]. Since the target is to prove unsatisfiability (proving that the negation of the property is unsatisfiable), if the base case is satisfiable, a counterexample is returned. Otherwise, the induction step is checked by assuming that the property holds for all the states except the last one (the \((k+1)\)’th state) [14].

1.7 A.7: Interpolation

Given an unsatisfiable formula \(A \wedge B\), an interpolant I is a formula such that \(A \implies I\), \(I \wedge B\) is unsatisfiable and I contains only common variables to A and B. Given a system M, a property p and a bound k, interpolation-based verification starts by attempting bounded model-checking (BMC) with the bound k. If a counterexample is found, the algorithm returns. Otherwise, it partitions the problem into a prefix pre and a suffix suf, such that the problem is the conjunction of the two. Then, the interpolant I of \({ pre}\) and \({ suf}\) is computed, and it represents an over-approximation of the set of states reachable in one step from the initial state of the algorithm. If I contains no new states, a fixpoint is reached and the property is proved. Otherwise, the algorithm reiterates and replaces the initial states with new states added by I [2].

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Zaraket, F.A., Jaber, M., Noureddine, M. et al. From high-level modeling toward efficient and trustworthy circuits. Int J Softw Tools Technol Transfer 21, 143–163 (2019). https://doi.org/10.1007/s10009-017-0462-5

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-017-0462-5

Keywords