feat(auxmodules): Allow helper modules that enable easy refinement proofs:

- `AuxModule`: an external Module that is hooked up at the top level:
        - allows addition of auxilliary (extra) signals
        - specifications can refer to these signals
- example: `designs/counter` and `specs/counter.py`

fix(onetrace): One trace verification needs to only dump properties with one instance

TODO: clean-up the PyConfig and TaskMgr classes, they can most probably be combined, making interfaces simpler

Signed-off-by: Adwait Godbole <[email protected]>

Author: adwait

.gitignore

@@ -12,6 +12,7 @@ dump
 
 # SVA intermediate files
 *.pyc.sv
+reset.rseq
 
 # Jasper directory
 jgproject/

designs/counter/config.json

@@ -0,0 +1,12 @@
+{
+    "jasper" : {
+        "jdir"      : "designs/counter",
+        "script"    : "counter.tcl",
+        "pycfile"   : "counter.pyc.sv",
+        "context"   : "<embedded>::einter"
+    },
+    "spec" : {
+        "pycspec" : "counter",
+        "k"       : 3
+    }
+}

designs/counter/counter.sv

@@ -0,0 +1,43 @@
+
+
+module counter (
+    input clk,
+    input rst,
+    output [7:0] counter
+);
+
+    // Counter that increments by 1
+    logic [7:0] counter_internal;
+
+    always_ff @(posedge clk or posedge rst) begin
+        if (rst) begin
+            counter_internal <= 8'h00;
+        end else begin
+            counter_internal <= counter_internal + 1;
+        end
+    end
+
+    assign counter = counter_internal;
+
+endmodule
+
+
+module parity (
+    input clk,
+    input rst,
+    input [7:0] counter
+);
+
+    // OddEven parity
+    logic parity;
+
+    // toggle parity bit
+    always_ff @(posedge clk or posedge rst) begin
+        if (rst) begin
+            parity <= 1'b0;
+        end else begin
+            parity <= ~parity;
+        end
+    end
+
+endmodule

designs/counter/counter.tcl

@@ -0,0 +1,85 @@
+set banner "========== New session =========="
+puts $banner
+
+clear -all
+
+# Disable some info messages and warning messages
+# set_message -disable VERI-9033 ; # array automatically black-boxed
+# set_message -disable WNL008 ; # module is undefined. All instances will be black-boxed
+# set_message -disable VERI-1002 ; # Can't disable this error message (net does not have a driver)
+# set_message -disable VERI-1407 ; # attribute target identifier not found in this scope
+set_message -disable VERI-1018 ; # info
+set_message -disable VERI-1328 ; # info
+set_message -disable VERI-2571 ; # info
+# set_message -disable VERI-2571 ; # info: disabling old hierarchical reference handler
+set_message -disable INL011 ; # info: processing file
+# set_message -disable VERI-1482 ; # analyzing verilog file
+set_message -disable VERI-1141 ; # system task is not supported
+set_message -disable VERI-1060 ; # 'initial' construct is ignored
+set_message -disable VERI-1142 ; # system task is ignored for synthesis
+# set_message -disable ISW003 ; # top module name
+# set_message -disable HIER-8002 ; # disabling old hierarchical reference handler
+set_message -disable WNL046 ; # renaming embedded assertions due to name conflicts
+set_message -disable VERI-1995 ; # unique/priority if/case is not full
+                                 # (we check these conditions with the elaborate
+                                 #  option -extract_case_assertions)
+
+set JASPER_FILES {
+    one_trace.sv
+}
+
+set env(DESIGN_HOME) [pwd]
+set err_status [catch {analyze -sv12 +define+JASPER +define+SYNTHESIS +libext+.v+.sv+.vh+.svh+ -f design.lst {*}$JASPER_FILES} err_msg]
+if $err_status {error $err_msg}
+
+elaborate \
+    -top einter \
+    -extract_case_assertions \
+    -no_preconditions \
+
+proc write_reset_seq {file} {
+    puts $file "fvreset 1'b1"
+    puts $file 1
+    puts $file "fvreset 1'b0"
+    puts $file {$}
+    close $file
+}
+
+proc reset_formal {} {
+    write_reset_seq  [open "reset.rseq" w]
+    # reset -expression fvreset
+    reset -sequence "reset.rseq"
+}
+
+
+clock clk
+
+# Constrain primary inputs to only change on @(posedge eph1)
+clock -rate -default clk
+
+reset_formal
+
+# Set default Jasper proof engines (overrides use_nb engine settings)
+#set_engine_mode {Ht Hp B K I N D AG AM Tri}
+set_engine_mode {Ht}
+
+set_max_trace_length 4
+
+# Adds $prefix to each string in $list
+proc map_prefix {prefix list} {
+    set out {}
+    foreach s $list {
+        lappend out "${prefix}${s}"
+    }
+    return $out
+}
+
+# The input signals of a module instance
+proc instance_inputs {inst} {
+    map_prefix "${inst}." [get_design_info -instance $inst -list input -silent]
+}
+
+# The output signals of a module instance
+proc instance_outputs {inst} {
+    map_prefix "${inst}." [get_design_info -instance $inst -list output -silent]
+}

designs/counter/design.lst

@@ -0,0 +1 @@
+${DESIGN_HOME}/counter.sv

designs/counter/one_trace.sv

@@ -0,0 +1,17 @@
+// Parent module with a miter with different inputs
+module einter (
+    input wire clk
+);
+
+    counter a (
+        .clk(clk)
+    );
+
+    default clocking cb @(posedge clk);
+    endclocking // cb
+
+    logic fvreset;
+
+    `include "counter.pyc.sv"
+
+endmodule

pycaliper/per/__init__.py

@@ -14,6 +14,8 @@
     PERHole,
     CtrAlignHole,
     SVFunc,
+    AuxPort,
+    AuxModule,
     rose,
     fell,
 )