Dynamic Assertion-Based Verification for SystemC

[foster911]

Dynamic Assertion-Based Verification for SystemC
                                    by
                          Deian Tabakov

 

http://www.cs.rice.edu/CS/Verification/Theses/Archive/dtabakov_dissertation2010.pdf

 

Question:

Is it possible to do Assertion-Based Verification with pure SystemC and available SCV in reality like the SystemVerilog Assertion does or it needs changing the Kernel or extending the SCV API? How about UVM in SystemC? This could have the advantage of getting rid of language changing.

[maehne]

Assertions in SystemC are not so powerful as they are in SystemVerilog. The assert condition is tested instantaneously and does not allow to express any time constraints. Still, they are very useful to test invariants inside your design. If you use the sc_assert macro of SystemC, you will get the context reported from which the assertion was triggered. Please note that this will terminate the simulation as it is considered to be of fatal severity. Use the SC_REPORT_* macros to generate messages with other severity levels.

 

SCV mainly adds support for randomization and transaction tracing to SystemC. The verification working group is working towards the release of an updated version, which is compatible with the current version of the SystemC standard and modern C++ compilers.

 

Work has started to bring the UVM to the SystemC world. First results were presented by the European FP7 project VERDI at FDL 2013 and the ESCUG meeting, which both took place this September in Paris:

• http://www.ecsi.org/fdl/program#verdi
• http://www.ti.uni-tuebingen.de/ESCUGM28-Paris-2013.1570.0.html

[sumit_tuwien]

As Torsten said, assertions are not so powerful in SystemC. But static BMC is possible with SystemC.

 

• You can perform static bounded model checking using LLBMC, but it has a limited support for C++. And things soon become ugly with SystemC!
• CBMC with SCOOT is able to perform static bounded model checking for SystemC. I am planning to try it very soon.

 

I know that event-B team was working with SystemC, but results are unknown to me. I did not find any measurable results in the internet, that means the work in on going.

 

Regards, Sumit

[sonalidutta]

In http://www.cs.rice.edu/CS/Verification/Theses/Archive/dtabakov_dissertation2010.pdf:

 

An assertion is an LTL formula with a set of sampling points that describes a formal property of your SystemC model under verification. In Assertion-based Dynamic Verification of SystemC models, each assertion is converted to a C++ monitor class. A C++ monitor class is just a C++ encoding of a deterministic finite automaton. The transition function of the DFA is encoded as a step() function in the monitor class.

 

Now the question is when and how frequently to execute the step() function of a monitor class. This is where the sampling points come into the picture. You execute the step() function only when any of the specified set of sampling points occur during your simulation. In the above dissertation, it allows you to sample at different phases of the SystemC kernel, for example: when a new delta cycle begins, when a particular event is notified by the kernel or when a SystemC process suspends. This cannot be done with the unmodified version of the SystemC kernel since all these kernel informations are hidden from the user. So in the above work, the author puts a minimal patch on the SystemC kernel to expose the necessary kernel information.

 

But this is not mandatory. You can also only sample at different points in your user model. For that you do not need to modify the SystemC kernel. But allowing sampling also at kernel phases adds to the monitoring power. So as a summary, it is not necessary to change the kernel to do assertion-based verification of SystemC. But since in SystemC (unlike SystemVerilog), the kernel plays a very important role in the simulation, if you change the kernel to expose certain information, it might be useful.

 

Universal Verification Methodology (UVM) is a new "de-facto standard" for verification (based on Accellera's marketing materials) (Primer here: http://www.doulos.com/knowhow/sysverilog/uvm/tutorial_0/). UVM is a base class library for hooking up monitors and generating tests, but does not do anything about Kernel events or about generating monitors.