Assertion signal stable value

[Risto97]

Hello,
I am trying to integrate your project in my Systemc-UVM testbench.
I have run into few things that are missing for me, or I dont know how to write them.

For example SVA assertion like this one, which is a quite common rule, that other signals should not change while valid is high and ready low.
AWVALID & ~AWREADY|=>$stable({AWADDR,AWID,AWLEN,AWSIZE,AWCACHE,AWSIZE})

I didn't managed to implement it without adding additional code to the testbench, I tried this.
SCT_ASSERT(sigs->mem_valid & !sigs->mem_ready , SCT_TIME(0), sigs->mem_ready, sigs->mem_addr.value_changed_event());

This should work, but I have a problem that the mem_ready is not getting set in the same delta cycle as mem_addr.
Meaning that when mem_addr changes state, mem_ready is still 0, until few delta cycles later.
In this case mem_ready is driven by verilated RTL, and mem_addr and mem_valid are driven by UVM driver.

UVM_INFO nmi/nmi_monitor.cpp(86) @ 50 ns: env.nmi_agent_master.mon [READY: ] 0 Addr 3 Valid: 1 RData: 0 WData: 1021 wstrb: 15 instr: 0 delta count: 146
UVM_INFO nmi/nmi_monitor.cpp(86) @ 50 ns: env.nmi_agent_master.mon [READY: ] 0 Addr 3 Valid: 1 RData: 0 WData: 1021 wstrb: 15 instr: 0 delta count: 147
UVM_INFO nmi/nmi_monitor.cpp(86) @ 50 ns: env.nmi_agent_master.mon [READY: ] 0 Addr 3 Valid: 1 RData: 0 WData: 1021 wstrb: 15 instr: 0 delta count: 148
UVM_INFO nmi/nmi_monitor.cpp(86) @ 50 ns: env.nmi_agent_master.mon [READY: ] 1 Addr 3 Valid: 1 RData: 0 WData: 1021 wstrb: 15 instr: 0 delta count: 149
UVM_INFO nmi/nmi_monitor.cpp(86) @ 50 ns: env.nmi_agent_master.mon [READY: ] 1 Addr 3 Valid: 1 RData: 0 WData: 1021 wstrb: 15 instr: 0 delta count: 150

For example above you can see few delta cycles after mem_addr.value_changed_event() is notified in a process. You can see that mem_ready goes to one in few cycles.

I managed to solve it, by making an additional sc_signal addr_old, that is one cycle behind mem_addr.
SCT_ASSERT(sigs->mem_valid && !sigs->mem_ready , SCT_TIME(1), sigs->mem_addr == *addr_old , sigs->clk->posedge_event());
However this solution requires additional signals, which defeats the purpose of the library in my opinion.

Do you know of a more elegant way of solving it, or would you consider adding feature that would ease this property to the library?
I am willing to implement it, provided some guidance.

[mikhailmoiseev]

Hello,

It is possible to provide a SCT_ASSERT_STABLE macro which will work for single signal/port or expression of them:

// Module scope
SCT_ASSERT_STABLE(mem_valid && !mem_ready , mem_addr, clk->posedge_event());   // single signal
SCT_ASSERT_STABLE(mem_valid && !mem_ready , mem_data & mem_benable, clk->posedge_event());  // expression

To check several signals are stable, it needs several assertions.

Is that is useful enough?
Are you using assertions in module scope or in process function scope? Is that OK to have it in module scope only?

[Risto97]

Hello Mikhail,

Thank you for replying, yes that construct would be very useful, it would eliminate the need for additional signals.
I use the assertions mostly in module scope (I think). In UVM environment for now I define asserts in connect_phase of monitor.

If I can give another few ideas that might be useful to implement:

1. $rose property (immediately $fell is also easily implemented after that)
   Currently I use the next code to achieve $rose, as you can see I need additional signal psel_old.
   SCT_ASSERT(!*psel_old && sigs->psel, SCT_TIME(1), sigs->enable, sigs-pclk->posedge_event());

2. Reporting flexibility: now you are using assert to terminate the execution when the fault is found by calling C++ assert();
   I don't like this behaviour, as I would like to print all of the errors that occurred and continue the simulation.
   So in order to mitigate this problem, I pass the -DNDEBUG flag to the compiler to ignore the assert (this completely breaks your sct_assert() function, as nothing is printed to the screen there). However SCT_ASSERT still works and I get this print:
   230 ns, Error : sct_property violation sigs->penable && !sigs->pready ##(1) sigs->penable
   As you can see I cannot see from which module the assert came from (I have same ASSERTS connected to different interfaces).

One way to solve this would be to be able to add custom message to the assert
SCT_ASSERT(!*psel_old && sigs->psel, SCT_TIME(1), sigs->enable, sigs-pclk->posedge_event(), "CUSTOM MESSAGE");
Another more complex way would be to have it somehow integrated with custom printer command, for example in UVM there are UVM_INFO, UVM_ERROR, UVM_WARNING, UWM_FATAL... Which could be useful to report assertion failures.
And have an useful summary at the end.
`--- UVM Report Summary ---

** Report counts by severity
UVM_INFO : 44
UVM_WARNING : 1
UVM_ERROR : 0
UVM_FATAL : 0
** Report counts by id
[APB AGENT build PHASE] 4
[APB DRIVER build PHASE] 4
[CFGDB/GET] 9
[CFGDB/SET] 16
[CONFIGURED AS MASTER] 1
[CONFIGURED AS SLAVE] 3
[RNTST] 1
[Running Monitor] 4
[TPRGED] 1
[UVMTOP] 1
[apb_m_seq] 1

UVM_INFO @ 1220 ns: reporter [FINISH] UVM-SystemC phasing completed; simulation finished`

[mikhailmoiseev]

Please check the updated repo. Stable/rose/fell added as described at https://github.com/intel/systemc-compiler/wiki/Assertions-in-SystemC
Hope you could help with checking corner cases.
One limitation is REXPR can be bool only. If that is critical for you, feel free to propose pull request.

Error messages for all the assertion fixed, now FILE:LINE reported instead of the assertion body.
Now, for sct_assert error message also reported if NDEBUG defined.

[Risto97]

Hello, thank you for implementing this.
I quickly tested the SCT_ROSE property as that one was a drop-in replacement. It worked, I will test it more on different testbenches and let you know if I run into a bug.

For the stable property, bool is not good enough in my case, because I want to assert if there was a change on the vector signal.
I will look into making a pull request for making it work for vectors, probably next month

[mikhailmoiseev]

Supported C++ and SystemC types in right expression of stable/rose/fell.
It needs to use read() function for signals/ports.

[mikhailmoiseev]

As soon as integer types are supported in stable (SCT_ASSERT_STABLE), see nothing else to do. Please confirm that it works at your side.

[Risto97]

I didn't have time to test it in more depth. I just returned from holidays and will hopefully get back to that project in next days/weeks.

[mikhailmoiseev]

Any updates on that? Can I close the issue?

[Risto97]

Hello Mikhail,

Sorry, I was busy with other things.

I think there is a problem.
Looking at the file: https://github.com/intel/systemc-compiler/blob/main/examples/asserts/temp_assert.cpp
Property in question: SCT_ASSERT_ROSE(cntr.read() == 10, (1), st1.read(), clk.pos());

This property fails but the time of the test is not long enough in this file.
If you change line 124 to wait for 15 cycles for example, then it will fail

14 ns, Error : sct_property rose violation /mnt/ext/systemc/systemc-compiler/bugs/rose/main.cpp:59
And in my opinion it should not fail, looking at the generated vcd:

Sorry for not investigating more on this, I just saw it and wanted to report it to you, if I don't have time to find it.
I will let you know if I find what is the problem

[mikhailmoiseev]

Thank you for the update. There were a few bugs in the test, which have been fixed.

[Risto97]

Actually the problem was on my side.
For me a lot of the assertions were failing from that test.
It turned out to be some problem with the C++ standard version of SystemC.
I recompiled the full toolchain with C++17 instead of C++14 and now it doesn't fail.

There were no warnings given by the compiler about using old c++ standard, so it was hard to understand the problem.
I will continue to test the assertions on more practical examples and let you know if I find a bug.