[RFC] Fault Property Language

[leonardt]

Design Goals

• Provide a python embedded language for writing assert/cover properties using magma values
• Simple integration with magma design code (write inline with generators) to minimize overhead
• Compile through CoreIR to SystemVerilog to integrate with mainstream verification tools

Initial Requirements

These are the initial features identified by users. The goal is to provide a minimal set of useful primitives that hopefully capture the various issues that might arise in the design of the language. These primitives should be immediately useful for writing assertions, without being too complex to facilitate rapid development of an initial prototype (e.g. we don't need to support all of SVA from the start).

Types of assertions

1. Immediate/final assertions - unclocked boolean expressions that are either applied in the initial or final phase of simulation.

   f.assert_immediate(prop0, name="name0")
   f.assert_final(prop1, name="name1")

2. Concurrent properties - clocked (and usually guarded by reset). Three main types: assert, covers, and assume. assume is use for formal property verification and is treated as an assert in simulation.

   f.assert(prop0, name="name0", on=m.posedge(io.CLK)).disable_if(!io.RESETN)
   
   f.cover(prop1 , name="name1", on=m.posedge(io.CLK)).disable_if(!io.RESETN)
   
   f.assume(prop2, name="name2", on=m.posedge(io.CLK)).disable_if(!io.RESETN)

   disable_if is optional (maybe just make it kwarg to be consistent?). Should support negedge, as well as multiple clocks.

Property Primitives

We present two proposed interfaces. The first uses a "hack" to define custom infix operators (see http://tomerfiliba.com/blog/Infix-Operators/ for an example). This provides a decently ergonomic alternative to SVA's convenient operators given Python's lack of corresponding operator definitions or ability to define custom operators. The second uses a string interface to allow the user to pass an operator as string. This is mainly targeted towards experienced SVA users that would like to use their familiar syntax.

1. Suffix Implication - S is the antecedent (triggering condition), P is the consequent (checked when P holds). SVA's overlapping implication operator S |-> P.

   S |f.implies| P
   f.sva(S, "|->", P)

2. Pound Delay - Basic primitive for defining temporal sequences of boolean expressions that are evaluated over time (clock ticks). We use square braces for consistency with variable pound delay (next item) which can leverage slice syntax.

   # write is followed by read in one clock cycle
   io.write |f.delay[1]| io.read
   f.sva(io.write, "##1", io.read)
   
   # if write happens, read must happen after three cycles
   io.write |f.implies|f.delay[3]| io.read
   f.sva(io.write, "|-> ##1", io.read)

3. Variable Pound Delay - Extends pound delay to encode a variable number of cycles

   # write is followed by read in one or two clock cycles
   io.write |f.delay[1:2]| io.read
   f.sva(io.write, "##[1:2]", io.read)
   
   # if write happens, read must happen after one or two cycles
   io.write |f.implies|f.delay[1:2]| io.read
   f.sva(io.write, "|-> ##[1:2]", io.read)
   
   # Zero or more cycles
   io.ready |f.implies|f.delay[0:]| io.valid
   f.sva(io.ready, "|-> ##[*]", io.valid)      # or "|-> ##[*0:$]"
   
   # One or more cycles
   io.ready |f.implies|f.delay[1:]| io.valid
   f.sva(io.ready, "|-> ##[+]", io.valid).     # or "|-> ##[*1:$]"

4. Repetition - Indicate that a temporal sequence occurs a number of times

   # Consecutive repetition - sequence (seq0) repeats itself a specified number (`N`) of times
   seq0 |f.repeat[N]| seq1
   f.sva(seq0, "[*N]", seq1)
   
   # Zero or more times
   seq0 |f.repeat[0:]| seq1
   f.sva(seq0, "[*]", seq1)
   
   # One or more times
   seq0 |f.repeat[1:]| seq1
   f.sva(seq0, "[+]", seq1)

5. Goto repetition - Check if boolean expression has been true for a specified number of ticks, but not necessarily on consecutive cycles.

   # bool_exp has been true three times
   bool_exp |f.goto[3]| seq
   f.sva(bool_exp, "[-> 3]", seq)
   
   # bool_exp has been true three to 5 times
   bool_exp |f.goto[3:5]| seq
   f.sva(bool_exp, "[-> 3:5]", seq)

6. Eventually - If A is asserted, B should go high sometime in the future (eventually)

   A |f.implies|f.eventually| B
   f.sva(A, "|-> s_eventually", B)

7. throughout - Check that a condition holds true during the evaluation of an entire sequence

   # on posedge a, check b is high until c goes low
   f.rose(a) |f.implies| (b |f.throughout| ~(c |f.goto[1]) )
   f.sva(f.rose(a), "|->", (b, "throughout", "!", c, "[-> 1]"))

8. until - Evaluates to true if A evaluates to true at every clock tick until one clock tick before B

   # on posedge a, check for b to be high continuously 
   # until one cycle before c goes low
   f.rose(a) |f.implies| (b |f.until| ~c)
   f.sva(f.rose(a), "|->", (b, "until", ~c))

9. until_with - Like until, except overlapping with the cycle that B occurs

    # on posedge a, check for b to be high continuously 
    # until the cycle that c goes low
    f.rose(a) |f.implies| (b |f.until_with| ~c)
    f.sva(f.rose(a), "|->", (b, "until_with", ~c))

10. inside - use Python in for set membership TODO

System and Sampled Value Functions

These can simply be provided as functions imported via fault (and compiled to their corresponding function by insert a $ prefix for the name)

• f.onehot0
• f.onehot
• f.countones
• f.isunknown
• f.past - note past can have optional arguments (e.g. 3 cycles ago)
• f.rose
• f.fell
• f.stable

Other

• f.not (for negating properties, different than bitwise invert), also other like and, or

Supporting Methodologies

Verilog Defines

Common workflows use ifdef macros to wrap properties so they can be controlled in the target environment (e.g. wrap assert/assume with ifdef ASSERT_ON and cover with ifdef COVER_ON). Magma can provide a notion of a compile guard that can be used to mark asserts/assumes/covers with a variable that is emitted by the compiler.

ASSERT_ON = f.compile_guard("ASSERT_ON")
f.assert(...).guard(ASSERT_ON)

Macros

We can use standard python functions to automatically wrap properties with a guard (emulating the standard macro approach). We can similarly simplify the description of the name, clock and reset. However, we unfortunately can't provide the convenience of macros of using a default clock/reset name (where they insert a standard name symbol). We could support passing an IO object and automatically discovering the clock, or inspecting the calling environment to discover the clock signal.

def guarded_assert(prop, clk, reset):
    f.assert(prop, name=f"SVA_ERROR_{name}", on=m.posedge(clk))\
     .disable_if(!reset)\
     .guard(ASSERT_ON)

[rsetaluri]

Design Goals

• Provide a python embedded language for writing assert/cover properties using magma values
• Simple integration with magma design code (write inline with generators) to minimize overhead
• Compile through CoreIR to SystemVerilog to integrate with mainstream verification tools

Initial Requirements

These are the initial features identified by users. The goal is to provide a minimal set of useful primitives that hopefully capture the various issues that might arise in the design of the language. These primitives should be immediately useful for writing assertions, without being too complex to facilitate rapid development of an initial prototype (e.g. we don't need to support all of SVA from the start).

Types of assertions

1. Immediate/final assertions - unclocked boolean expressions that are either applied in the initial or final phase of simulation.

   f.assert(prop0, name="name0")
   f.assert_final(prop1, name="name1")

2. Concurrent properties - clocked (and usually guarded by reset). Three main types: assert, covers, and assume. assume is use for formal property verification and is treated as an assert in simulation.

   f.assert(prop0, name="name0", on=m.posedge(io.CLK)).disable_if(!io.RESETN)
   
   f.cover(prop1 , name="name1", on=m.posedge(io.CLK)).disable_if(!io.RESETN)
   
   f.assume(prop2, name="name2", on=m.posedge(io.CLK)).disable_if(!io.RESETN)

   disable_if is optional (maybe just make it kwarg to be consistent?). Should support negedge, as well as multiple clocks.

Property Primitives

We present two proposed interfaces. The first uses a "hack" to define custom infix operators (see http://tomerfiliba.com/blog/Infix-Operators/ for an example). This provides a decently ergonomic alternative to SVA's convenient operators given Python's lack of corresponding operator definitions or ability to define custom operators. The second uses a string interface to allow the user to pass an operator as string. This is mainly targeted towards experienced SVA users that would like to use their familiar syntax.

1. Suffix Implication - S is the antecedent (triggering condition), P is the consequent (checked when P holds). SVA's overlapping implication operator S |-> P.

   S |f.implies| P
   f.sva(S, "|->" P)

2. Pound Delay - Basic primitive for defining temporal sequences of boolean expressions that are evaluated over time (clock ticks). We use square braces for consistency with variable pound delay (next item) which can leverage slice syntax.

   # write is followed by read in one clock cycle
   io.write |f.delay[1]| io.read
   f.sva(io.write, "##1", io.read)
   
   # if write happens, read must happen after three cycles
   io.write |f.implies|f.delay[3]| io.read
   f.sva(io.write, "|-> ##1", io.read)

3. Variable Pound Delay - Extends pound delay to encode a variable number of cycles

   # write is followed by read in one or two clock cycles
   io.write |f.delay[1:2]| io.read
   f.sva(io.write, "##[1:2]", io.read)
   
   # if write happens, read must happen after one or two cycles
   io.write |f.implies|f.delay[1:2]| io.read
   f.sva(io.write, "|-> ##[1:2]", io.read)
   
   # Zero or more cycles
   io.ready |f.implies|f.delay[0:]| io.valid
   f.sva(io.ready, "|-> [*]", io.valid)      # or "|-> ##[*0:$]"
   
   # One or more cycles
   io.ready |f.implies|f.delay[1:]| io.valid
   f.sva(io.ready, "|-> [+]", io.valid).     # or "|-> ##[*1:$]"

4. Repetition - Indicate that a temporal sequence occurs a number of times

   # Consecutive repetition - sequence (seq0) repeats itself a specified number (`N`) of times
   seq0 |f.repeat[N]| seq1
   f.sva(seq0, "[*N]", seq1)
   
   # Zero or more times
   seq0 |f.repeat[0:]| seq1
   f.sva(seq0, "[*]", seq1)
   
   # One or more times
   seq0 |f.repeat[1:]| seq1
   f.sva(seq0, "[+]", seq1)

5. Goto repetition - Check if boolean expression has been true for a specified number of ticks, but not necessarily on consecutive cycles.

   # bool_exp has been true three times
   bool_exp |f.goto[3]| seq
   f.sva(bool_exp, "[-> 3]", seq)
   
   # bool_exp has been true three to 5 times
   bool_exp |f.goto[3:5]| seq
   f.sva(bool_exp, "[-> 3:5]", seq)

6. Eventually - If A is asserted, B should go high sometime in the future (eventually)

   A |f.implies|f.eventually| B
   f.sva(A, "|-> s_eventually", B)

7. throughout - Check that a condition holds true during the evaluation of an entire sequence

   # on posedge a, check b is high until c goes low
   f.rose(a) |f.implies| (b |f.throughout| ~(c |f.goto[1]) )
   f.sva(f.rose(a), "|->", (b, "throughout", "!", c, "[-> 1]"))

8. until - Evaluates to true if A evaluates to true at every clock tick until one clock tick before B

   # on posedge a, check for b to be high continuously 
   # until one cycle before c goes low
   f.rose(a) |f.implies| (b |f.until| ~c)
   f.sva(f.rose(a), "|->", (b, "until", ~c))

9. until_with - Like until, except overlapping with the cycle that B occurs

   # on posedge a, check for b to be high continuously 
   # until the cycle that c goes low
   f.rose(a) |f.implies| (b |f.until_with| ~c)
   f.sva(f.rose(a), "|->", (b, "until_with", ~c))

10. inside - use Python in for set membership TODO

System and Sampled Value Functions

These can simply be provided as functions imported via fault (and compiled to their corresponding function by insert a $ prefix for the name)

• f.onehot0
• f.onehot
• f.countones
• f.isunknown
• f.past - note past can have optional arguments (e.g. 3 cycles ago)
• f.rose
• f.fell
• f.stable

Other

• f.not (for negating properties, different than bitwise invert), also other like and, or

Supporting Methodologies

Verilog Defines

Common workflows use ifdef macros to wrap properties so they can be controlled in the target environment (e.g. wrap assert/assume with ifdef ASSERT_ON and cover with ifdef COVER_ON). Magma can provide a notion of a compile guard that can be used to mark asserts/assumes/covers with a variable that is emitted by the compiler.

ASSERT_ON = f.compile_guard("ASSERT_ON")
f.assert(...).guard(ASSERT_ON)

Macros

We can use standard python functions to automatically wrap properties with a guard (emulating the standard macro approach). We can similarly simplify the description of the name, clock and reset. However, we unfortunately can't provide the convenience of macros of using a default clock/reset name (where they insert a standard name symbol). We could support passing an IO object and automatically discovering the clock, or inspecting the calling environment to discover the clock signal.

def guarded_assert(prop, clk, reset):
    f.assert(prop, name=f"SVA_ERROR_{name}", on=m.posedge(clk))\
     .disable_if(!reset)\
     .guard(ASSERT_ON)

[leonardt]

Since the prototype for this has been merged/released, I will close this and open new issues to track.