diff --git a/verification/example.md b/verification/example.md index f61eb85..4594e1b 100644 --- a/verification/example.md +++ b/verification/example.md @@ -1,6 +1,6 @@ # Examples -Here we'd like to give some examples of the refinement relations. The features described may include some of the syntactic sugar we are currently working on, which will be marked in the text. +Here we'd like to give some examples of the refinement mapping. ## Conditional Mapping @@ -8,7 +8,7 @@ In variable mapping section, the conditional mapping is helpful in many cases. B ### Mapping Loop Body with Unrolled Pipelines -Suppose we have a specification for AES-128 function, which consist of 10 rounds of cryptographic operations, each round takes results from previous round and generate new ciphertext and new round key which will be used in the next round. In the ILA model, this is described with the help of child-instructions that form a loop. Whereas, the implementation is a pipeline which corresponds to an unrolling of the loop in the specification. This is illustrated in the figure below. +Suppose we have a specification for AES-128 function, which consist of 10 rounds of cryptographic operations, each round takes results from previous round and generate new ciphertext and new round key which will be used in the next round. In the ILA model, this is described with the help of child-instructions that form a loop. The implementation is a pipeline which corresponds to an unrolling of the loop. This is illustrated in the figure below. ![](../.gitbook/assets/aes-128-loop.png) @@ -16,25 +16,14 @@ When verifying the child-instructions, we need to map the state variables holdin ```javascript "state mapping": { - "ciphertext" : [["ILA.round == 0", "s_in" ], - ["ILA.round == 1", "s0" ], - ["ILA.round == 2", "s1" ], + "ciphertext" : [["ILA.round == 0", "RTL.s_in" ], + ["ILA.round == 1", "RTL.s0" ], + ["ILA.round == 2", "RTL.s1" ], ... ] } ``` -Or, alternatively, you can use: - -```javascript - "state mapping": { - "ciphertext" : [{"cond":"ILA.round == 0", "map":"s_in" }, - {"cond":"ILA.round == 1", "map":"s0" }, - {"cond":"ILA.round == 2", "map":"s1" }, - ... - ] - } -``` Regarding the `round` variable in ILA, because the loop in Verilog is fully unrolled and the effects of `round` are already reflected in the mapping of `ciphertext`, we don't need a mapping for `round`. We can simply write: @@ -46,7 +35,7 @@ Regarding the `round` variable in ILA, because the loop in Verilog is fully unro ``` {% hint style="info" %} -The condition are treated as a ordered list, namely, only when the first condition does not hold, will the rest of the mapping be considered. You can have a default case with condition `1'b1` or `null`. +The condition are treated as a ordered list, namely, only when the first condition does not hold, will the rest of the mapping be considered. You can have a default case with condition `1'b1`. {% endhint %} ### Mapping State Variables with On-the-Fly Values @@ -60,15 +49,15 @@ When tackling pipelined designs, for a software-visible state variable \(e.g., a ```javascript "state mapping": { ..., - "r1" : [ {"cond":"m1.reg_1_w_stage[1]", "map":"ex_alu_result"}, - {"cond":"m1.reg_1_w_stage[0]", "map":"ex_wb_val"}, - {"cond":null, "map":"register[1]"} ], + "r1" : [ [ "m1.reg_1_w_stage[1]", "RTL.ex_alu_result"], + [ "m1.reg_1_w_stage[0]", "RTL.ex_wb_val" ], + [ "1'b1", "RTL.register[1]" ]], "r2" : [...], ... } ``` -**Light-weight flushing.** This is a setting similar to what has been used in ARM's ISA-Formal work. One can use prophecy variables \(variables holding values available in the future\) to help construct the mapping. The value-on-the-fly will be written back to the architectural register file in the future and we can map a register with that future value. Our variable mapping allows this mapping using what we call "value holder" \(it is essentially an auxiliary variable and note that it can also hold history values\). The light-weight flushing setting is illustrated in the figure below: +**Light-weight flushing.** This is a setting similar to what has been used in ARM's ISA-Formal work. One can use prophecy variables \(variables holding values available in the future\) to help construct the mapping. The value-on-the-fly will be written back to the architectural register file in the future and we can map a register with that future value. Our variable mapping allows this mapping using what we call "value recorder" \(it is essentially an auxiliary variable and note that it can also hold history values\). The light-weight flushing setting is illustrated in the figure below: ![](../.gitbook/assets/future-values.png) @@ -77,191 +66,23 @@ Again for the previous pipeline example, we can have the variable mapping as fol ```javascript "state mapping": { ..., - "r1" : [ {"cond":"__START__", "map":"#valueholder_r1#"}, - {"cond":"__IEND__", "map":"register[1]"}], + "r1" : [ ["#decode#", "( RTL.register[1] )@( stage_tracker == 1 )"], + ["#commit#", "RTL.register[1]"]], "r2" : [...], ... } ``` -Here `#` quoted names are the names to value holders. The condition `__START__` indicates, at the beginning of the instruction under verification, `r1` is mapped to the value holder \(a future value in our case\) and at the end of the instruction execution \(indicated by `__IEND__`\), it is mapped to the write-back value in the register file. - -Value holders are defined in the `value-holder` section in the variable mapping file. Below is an example. The condition here indicates when to take the value of `m1.register[1]` and hold it for use universally. `stage_tracker` is an example of the monitor that one may add to track the stage of an instrcution in the pipeline \(if the original design already has some tracking mechanism, it can be used instead\). - -```javascript -"value-holder": { - "valueholder_r1":{ - "cond" : "stage_tracker == 1", // Commit point of the previous instruction - "val" : "m1.register[1]", - "width": 8 - } -} -``` - -{% hint style="info" %} -`width` in the above example can be set to `"auto"` which will allow the tool to automatically determine the width of the value holder. -{% endhint %} - -{% hint style="info" %} -We are working on a syntactic sugar in the form of `val@cond` in the `state-mapping` part which can automatically generate a value holder. In the future we shall allow the following shortcut: - -```javascript - "state mapping": { - ..., - "r1" : [ {"cond":"__START__", "map":"register[1] @ (stage_tracker == 1)"}, - {"cond":"__IEND__", "map":"register[1]"}], - "r2" : [...], - ... - } -``` -{% endhint %} - -## Stage Tracker - -As shown by the previous example, it is very often that one would like to track the stage of an instruction. Currently this is done via inline Verilog monitors. For the previous example, we have a monitor like the following. - -```javascript - "verilog-inline-monitors" : { - "stage_tracker" : { - "verilog": - ["always @(posedge clk) begin", - " if (__START__) stage_tracker <= 0;", - " else if (__STARTED__ && !__ENDED__) stage_tracker <= stage_tracker + 1;", - "end"], - "defs" :[ ["stage_tracker", 2, "reg"] ], - "refs" :[] - } -``` - -This monitor starts the tracking when the instruction under verification starts to execute and counts up till the instruction finishes. This works for the simple case as the pipeline will not stall and the tracker does not need to stall either. However, in general this is not true and below we provide an example to handle a more general case. - -In the example below, there are 3 intermediate stages and a final write-back \(s4\) stage. The monitor here uses the signals inside the pipeline like `m1.s1_to_s2$D_IN` and `m1.s1_to_s2$EN` to tell if the current instruction moves to the next stage. These are indicated by the signals like `s1_to_s2`. - -```javascript - "verilog-inline-monitors" : { - "stage_tracker" : { - "verilog": - [ - "wire s1_begin = m1.stage1_rg_full;", - "wire s1_to_s2 = m1.s1_to_s2$D_IN & m1.s1_to_s2$EN;", - "wire s2_to_s3 = m1.s2_to_s3$D_IN & m1.s2_to_s3$EN;", - "wire s3_to_s4 = m1.s3_deq$EN & m1.s3_deq$D_IN;", - "always @(*) begin monitor_s1 = s1_begin & ~monitor_s1_already & __START__; end", - "always @(posedge clk) begin", - " if(rst)", - " monitor_s1_already <= 0;", - " else if (monitor_s1 && monitor_s2_nxt)", - " monitor_s1_already <= 1;", - "end", - "always @(*) begin monitor_s2_nxt = (monitor_s2 == 0) ? ( s1_to_s2 & monitor_s1 ? 1'b1 : 1'b0) : ", - " ( s2_to_s3 ? 1'b0 : 1'b1); end", - "always @(posedge clk) begin", - " if(rst) begin", - " monitor_s2 <= 0;", - " monitor_s2_already <= 0;", - " end", - " else begin", - " monitor_s2 <= monitor_s2_nxt;", - " if (monitor_s2 & monitor_s3_nxt)", - " monitor_s2_already <= 1;", - " end", - "end", - "always @(*) begin monitor_s3_nxt = (monitor_s3 == 0) ? ( s2_to_s3 & monitor_s2 ? 1'b1 : 1'b0) : ", - " (s3_to_s4 ? 1'b0 : 1'b1) ; end ", - "always @(posedge clk) begin", - " if(rst) begin", - " monitor_s3 <= 0;", - " monitor_s3_delay <= 0;", - " end", - " else begin", - " monitor_s3 <= monitor_s3_nxt;", - " if (monitor_s3)", - " monitor_s3_delay <= 1'b1; // enough", - " end", - "end", - "always @(*) begin monitor_s4_nxt = ", - " monitor_s3 && s3_to_s4 ? 1'b1 : monitor_s4; end", - "always @(posedge clk) begin", - " if(rst) begin", - " monitor_s4 <= 0;", - " monitor_s4_delay <= 0;", - " end", - " else begin", - " monitor_s4 <= monitor_s4_nxt;", - " if (monitor_s4)", - " monitor_s4_delay <= 1'b1;", - " end", - "end", - "always @(*) begin end_of_pipeline = monitor_s4 && ~monitor_s4_delay ; end // just check one cycle" - ], - "defs" : - [ - ["end_of_pipeline" , 1 , "reg"] , - ["monitor_s1_already" , 1 , "reg"] , - ["monitor_s1" , 1 , "reg"] , - ["monitor_s1_delay" , 1 , "reg"] , - ["monitor_s2" , 1 , "reg"] , - ["monitor_s2_nxt" , 1 , "reg"] , - ["monitor_s2_already" , 1 , "reg"] , - ["monitor_s3" , 1 , "reg"] , - ["monitor_s3_nxt" , 1 , "reg"] , - ["monitor_s3_delay" , 1 , "reg"] , - ["monitor_s4_nxt" , 1 , "reg"] , - ["monitor_s4" , 1 , "reg"] , - ["monitor_s4_delay" , 1 , "reg"] - ] , - - "refs" :[ - "m1.stage1_rg_full", - "m1.s1_to_s2$D_IN", - "m1.s1_to_s2$EN", - "m1.s2_to_s3$D_IN", - "m1.s2_to_s3$EN", - "m1.s3_deq$D_IN", - "m1.s3_deq$EN", - "m1.rg_retiring$EN" ] - }// stage tracker - } -``` - -{% hint style="info" %} -As the tracking of pipeline stages is a very common scenario, we are also working on a template to automatically generate a pipeline stage tracker. We expect this to handle the case of branching pipelines \(where there are fan-out points to dispatch instructions through any of the downstream pipelines, and merge point that coalesce the end of multiple pipelines\). Events are specified based on their effects on the stages as `exit` event and `enter` event. We shall also allow caching temporary values in auxiliary variables at the time of the events. -{% endhint %} - -## Simple Delays - -Another common scenario is that we'd like to delay a signal for a few cycles. The general way for this is an inline-monitor. For example, we'd like to delay `xram_ack` for one cycle and use it as the finish condition for an instruction. First, we can have a few lines in `verilog-inline-monitors` section as follows: - -```javascript -"verilog-inline-monitors" : { - "xram_ack_delay_1" : { - "verilog": [ - "always @(posedge clk) begin xram_ack_delay_1 <= xram_ack; end" - ], - "defs" : [["xram_ack_delay_1" , 1 , "reg"]], - "refs" : ["xram_ack"] - } -} -``` - -Recall that `defs` contains the auxiliary variables that we'd like to create and `refs` are the signals in the original design that we use in the monitor. - -{% hint style="info" %} -We are working on a syntactic sugar in the form of `signal ## cycle` and `(expression) ## cycle` that will create verilog-inline-monitor automatically to delay a signal for the given number of cycles. -{% endhint %} +Here `#` quoted names are the names of the phases. The condition `#decode#` indicates, at the beginning of the instruction under verification, `r1` is mapped to the value recorder \(a future value in our case\) and at the end of the instruction execution \(indicated by `#commit#`\), it is mapped to the write-back value in the register file. ## Mapping of Memory The specification of memory state variable mapping can be very different depends on the types of memory. -The memory in Verilog be internal or external. While the memory in ILA may be modeled as an internal or memory state variable, as well. -There isn't a strict dependency between the two choices. And there are four combinations as described below. +The memory in Verilog can be internal or external. While the memory in ILA may be modeled as an internal or memory state variable, as well. Therefore, there are four combinations as described below. ### Internal Memory in both ILA and RTL -Currently, there isn't a uniform and scalable way to handle this case for both Pono and JasperGold. -The current implemented approach is to declare the memory as internal in the annotation section, however, this won't scale to large memory. -Below gives an example. - +In this case, you can use the array expression in `state mapping` section to match the arrays. Let's see an example. The implementation contains two internal memories `mema` and `memb`, when `start` signal is asserted, it will swap the contents between two addresses in these two memories, where the addresses are specified by the input indices. ```text @@ -311,29 +132,17 @@ The ILA model also model these as internal memory state variables and the ILA ha } ``` -The mapping of the memories in ILA and Verilog is very straight-forward (below only shows the `state mapping` section). +The mapping of the memories in ILA and Verilog is very straight-forward: ```javascript "state mapping": { - "mema":"mema", - "memb":"memb"}, + "mema":"RTL.mema", + "memb":"RTL.memb"}, ``` -This simple handling will work for all backends, but would not scale to large memories. -If it is possible to convert the internal memory to an external one by commenting away the declaration of the Verilog array and the associated read/write logic, then we can use the memory abstraction approach that applies to external memory. (Note in the conversion, please keep the read/write signals intact as they will be treated as if they are interface signals to the external memory, and our tool can automatically pull these signals to the top level module.) - +In the backend, model checker like Pono will use array theory to handle the properties. However for JasperGold, the array will be kept concrete and would not scale to large memories. +If it is possible to convert the internal memory to an external one by commenting away the declaration of the Verilog array and the associated read/write logic, then we can use the interface mapping approach that applies to external memory. (Note in the conversion, please keep the read/write signals intact as they will be treated as interface signals to the external memory, and our tool can automatically pull these signals to the top-level module.) -{% hint style="info" %} -Currently, there is a limitation on the memory abstraction model, which only supports making one read and one write concrete. So, if the internal array is read or written more than twice during the execution of the instruction and they must be concrete to avoid the spurious counterexample due to the abstraction, you might have to consider the commercial solution (the Proof Accelerator in JasperGold, which is essentially a memory abstraction but can be configured to support multiple concrete read and write). -{% endhint %} - -{% hint style="info" %} -Specifically, for the Pono backend, we are working on a solution to use SMT array theory to support mapping of arrays. However, although no Verilog modification is needed, it might be difficult for the model checkers to prove unbounded correctness. -{% endhint %} - -{% hint style="info" %} -We are also considering the possibility of intergrating CHC solvers to overcome the above difficulty when handling arrays. Comments and feedbacks on this are greatly appreciated. -{% endhint %} ### Internal Memory in ILA and External Memory in RTL @@ -362,23 +171,22 @@ module swap ( endmodule ``` -Below shows the signal mapping below. Here it is a bit tricky as in Verilog there is no such signal that holds the output of the -read from these two arrays (they are directly used to overwrite the contect in another location). So we will need to create auxiliary variables to support this. In the table, we use `#mema_rdata#` and `#memb_rdata#` as the place-holders. +Below shows the signal mapping below. Here it is a bit tricky as in Verilog there is no such signal that holds the output of the read from these two arrays (they are directly used to overwrite the contect in another location). So we will need to create auxiliary variables to support this. In the table, we use `mema_rdata` and `memb_rdata` as the place-holders. | memory.port | signal | |------------- |-------------- | -| mema.ren | start | -| mema.raddr | addra | -| mema.rdata | #mema_rdata# | -| mema.wen | start | -| mema.waddr | addra | -| mema.wdata | #memb_rdata# | -| memb.ren | start | -| memb.raddr | addrb | -| memb.rdata | #memb_rdata# | -| memb.wen | start | -| memb.waddr | addrb | -| memb.wdata | #mema_rdata# | +| mema.ren | RTL.start | +| mema.raddr | RTL.addra | +| mema.rdata | mema_rdata | +| mema.wen | RTL.start | +| mema.waddr | RTL.addra | +| mema.wdata | memb_rdata | +| memb.ren | RTL.start | +| memb.raddr | RTL.addrb | +| memb.rdata | memb_rdata | +| memb.wen | RTL.start | +| memb.waddr | RTL.addrb | +| memb.wdata | mema_rdata | The overall state variable mapping should looks like this: @@ -388,35 +196,37 @@ The overall state variable mapping should looks like this: "models": { "ILA":"m0" , "VERILOG": "m1" }, "instruction mapping": [], "state mapping": { - "mema":"**MEM**mema", - "memb":"**MEM**memb"}, - - "interface mapping": { - "rst":"**RESET**", - "clk":"**CLOCK**", - "addra":"addra", - "addrb":"addrb", - "start":"start" + "mema": + { + "ren" : "RTL.start" , + "raddr" : "RTL.addra" , + "rdata" : "mema_rdata", + "wen" : "RTL.start" , + "waddr" : "RTL.addra" , + "wdata" : "memb_rdata" + }, + "memb": + { + "ren" : "RTL.start" , + "raddr" : "RTL.addrb" , + "rdata" : "memb_rdata", + "wen" : "RTL.start" , + "waddr" : "RTL.addrb" , + "wdata" : "mema_rdata" + } + }, + "input mapping": { + "addra":"RTL.addra", + "addrb":"RTL.addrb", + "start":"RTL.start" }, - "annotation" : { - "memory-ports" : { - "mema.ren" : "start" , - "mema.raddr" : "addra" , - "mema.rdata" : "#mema_rdata#" , - "mema.wen" : "start" , - "mema.waddr" : "addra" , - "mema.wdata" : "#memb_rdata#" , - "memb.ren" : "start" , - "memb.raddr" : "addrb" , - "memb.rdata" : "#memb_rdata#" , - "memb.wen" : "start" , - "memb.waddr" : "addrb" , - "memb.wdata" : "#mema_rdata#" - } + "RTL interface connection": { + "RESET" : "rst", + "CLOCK" : "clk" }, - "verilog-inline-monitors" : { + "monitor" : { "read_value_holder" : { "verilog": [], "defs" :[ ["mema_rdata", 8, "wire"],["memb_rdata", 8, "wire"] ], @@ -426,14 +236,6 @@ The overall state variable mapping should looks like this: } ``` -And to aid efficient reasoning, you should also enable `MemAbsReadAbstraction` option in the configuration for `VerilogVerificationTargetGenerator`. An example is given below: - -```cpp - VerilogVerificationTargetGenerator::vtg_config_t vtg_cfg; // default configuration - vtg_cfg.MemAbsReadAbstraction = true; // enable read abstraction in the abstract memory model - VerilogVerificationTargetGenerator vg( ... /* the arguments are omitted here */ , - vtg_cfg); // give vtg_cfg as the extra configuration -``` ### External Memory in ILA and Internal Memory in RTL @@ -442,7 +244,7 @@ In this case, you may want to consider to convert the internal Verilog memory as ### External Memory in both ILA and RTL In this case, you can try to map the directly interface signals between ILA and RTL, if -you are unable to write it as an one-to-one mapping in `interface mapping` section, `mapping control` section is available for you. +you are unable to write it as an one-to-one mapping in `input mapping` section, you can also use `additional mapping` section to specify the relation between the two sets of interfaces. diff --git a/verification/refinement.md b/verification/refinement.md index 690eeeb..3516a84 100644 --- a/verification/refinement.md +++ b/verification/refinement.md @@ -1,228 +1,288 @@ # Refinement Relation -The refinement map or refinement relation mainly consists of two parts: _variable mappings_ and _instruction completion conditions_. These two parts are specified in two separate files, one referred as _var-map_ and the other _inst-cond_. +## General Information -Besides the above two parts, there are other auxiliary information needed. They are: +Refinement relation is specified in JSON format and is provided as two files, one referred to as _variable mappings_ and the other as _instruction completion conditions_. +The JSON format allows specifying data structures like map and list and support data-types like string, integer and `null` (for empty field). -* **module naming**: The names of the ILA module and the Verilog module. -* **global invariants**: Some properties that are globally true for the Verilog design that will be checked separately and can be safely assumed when verifying individual instructions. -* **interface signal information**: What does the interface of the Verilog top module look like and what do these signals mean to the tool. -* **uninterpreted function mapping**: What an uninterpreted function inside the ILA model corresponds to. +A map (similar to a dictionary in Python) has the following syntax: +```javascript +{ + // a map is a set of key-value pairs + // the key must be string in "" + // the value can be anything + "a-string-for-key" : "a-string-for-value", + "a-string-for-another-key" : 123, + "a-string-for-a-third-key" : ... +} +``` -## The Structure of Variable Mappings +A list is an ordered set of elements, where each element can be any string, integer, or nested data structures. JSON format does not require the elements of a list to have the same type. +The top-level of a JSON file is a map and we call the key-value pairs in this top-level map as sections. + +## The Structure of Variable Mapping + +Below shows the general structure of the variable mapping file (or in short, var-map). Each section (like `state mapping"`) will be explained in details later. Section `additional mapping`, `assumptions`, `monitor` and `functions` are optional. Section names are case-insensitive and you can always use hypen (`-`) or underscore (`_`) to replace space in the section names. ```javascript { - "models": { - "ILA" : "" , - "VERILOG": "" - }, "state mapping": { - "" : "", + "" : "", + // more ... + }, + "input mapping": { + "" : "", // more ... }, - "interface mapping": { - "" : "", + "RTL interface connection" :{ + "CLOCK" : { + "" : "", // an input or a list of inputs + "" : ["", ""] }, + "RESET" : "", // an input or a list of inputs + "NRESET" : "", // an input or a list of inputs + "CUSTOMRESET" : "", // an input or a list of inputs + } + "additional mapping": [ + "", // more ... - }, - "mapping control": [ - "", + ], + "assumptions": [ + "", // more ... ], - "functions":{ - "": [ - [ - "", "", - "", "", + "monitor" : { + "" : { + "template" : "phase tracker", + ... + // instantiate a phase tracker template + // each template has its other fields + // to fill in + }, + "" : { + "template" : "value recorder", + ... + // instantiate a value recorder + // c,v,w + + }, + "" : { + "verilog" : "", + ... + // directly writing verilog here + }, + "" : "" + ... + } + "functions":{ // for uninterpreted functions + "": [ // list of invocation + { // an invocation is a map with `result` and `arg` + "result" : "", + "args" : { "", ...} // args // more ... - ] + }, + ... ] } } ``` -## The Structure of Instruction Completion Conditions -```javascript -{ - "instructions": - [ - { - "instruction" :"", - "ready bound" :12345, // - "ready signal" :"", - "max bound" :12345, // - "start condition" :"", - "flush constraint":"", - "pre-flush end" :"", - "post-flush end" :"" - } - ] -} -``` +## Refinement Expression, Condition and Signal Names -## Module Naming +In the above general structure, you can find terms like "refinement expression", "condition" or "signal name". Refinement expressions are basically valid Verilog expressions with some minor differences. We introduce new syntax for *value recorder*, *delay expression* and *phase identifiers*, and these will be explained in the later sections of this document. +The Verilog expressions can be interpreted as either (1) the expression of a function which specifies how ILA architectural state variables can be computed from the Verilog signals or (2) a relation between ILA architectural state variable and RTL signals. The difference in the interpretation is determined by whether the expression is a predicate in the last level. For example, a expression `RTL.v1 + RTL.v2` is not a predicate, whereas `ILA.v1 == RTL.v1 + RTL.v2` is a predicate. Whether the refinement expression is regarded as a predicate is independent from the bit-width. For example, `RTL.one_bit_signal` is not a predicate, even it is one-bit wide, whereas `RTL.one_bit_signal == 1'b1` is a predicate. -The module naming section comes first in the _var-map_ JSON file. It is a dictionary \(map\) with two elements. One element should have the key `ILA` and the value of it is what will be used as the instance name of the ILA module. The other element should have the key `VERILOG` with the value to be the instance name of the Verilog module. These names are used in all the expressions later when you want to refer to a variable in Verilog or ILA. +"Condition" is similar to a "refinement expression" as it follows the same syntactic requirements. However, the type or the outcome of a condition must be 1-bit. Even if it is not in the form of a predicate, it will be interpreted as a predicate (by implicitly adding `xxx == 1'b1` in the top-level). -## Variable Mapping +"Signal name" refers to a single signal (in RTL) and you cannot have any computation there. -The variable mapping in the JSON file is a map data structure. The keys of this map are the state variable names in the ILA model while the values are the Verilog variables. There are cases that one Verilog state variable can be mapped to multiple Verilog state variables and the mapping may be some special function. So the allowed value field of this map can be: -1. A Verilog variable name as a string. If the Verilog variable is in the top module of Verilog, you can omit the module name \(it does not hurt to add it\). Otherwise, you must specify the complete hierarchy. For example, if you want to refer to a signal `S` in module `A` that is instantiated with name `IA` in the top module, while the top module's instance name is `VERILOG` \(specified in the previous section\), then you should use `VERILOG.IA.S` to refer to it. -2. A predicate that has at least a `=` in it \(you can use `>=` , `<=` , `==` and etc.\) This is just for our parser to distinguish it from the first case. -3. A string-string pair that is in the form of a list or map. If it is given as a list, the first element is regarded as the condition and the second element is regarded as the mapping. It conveys the meaning of "when the condition is true, the ILA and Verilog variables should have the mapping". If the condition is not true, there is no mapping guaranteed. If the string-string pair is given as a map, it must have two elements. One element should have the key `cond` and the other should have the key `map`. The `map` part could be a string of Verilog variable name as in case \(1\) or a Verilog expression as case \(2\). -4. A list of string-string pairs, each pair follows requirement in \(3\). -5. If the ILA variable on the left is a memory, the right side depends on whether the Verilog memory is internal or external. If inside Verilog, there is an array that corresponds to this memory, you can directly use this name on the right side. Otherwise, you can make this ILA memory to map with an external memory using `"ILA-mem-name":"**MEM**ILA-mem-name"`. +## Special Syntax in Refinement Expressions -Below are some of the examples: +### Value Recorder -```javascript -{ - "state mapping": { - "ILA_state_1" : "Verilog_state_1", // case 1 - "ILA_state_2" : "ILA_state_2 == Verilog_state_2 + Verilog_state_3", // case 2 - "ILA_state_3" : ["__START__", "Verilog_state_3"], // case 3.a - "ILA_state_4" : { "cond":"__START__", "map":"Verilog_state_4"}, // case 3.b - "ILA_state_5" : [["__START__", "Verilog_state_5"], ["__IEND__","Verilog_state_6"]], // case 4 - "ILA_mem_state" : "Verilog_array_name", // case 5.a : internal memory in Verilog - "ILA_mem_state" : "**MEM**ILA_mem_state", // case 5.b : external memory in Verilog - // more ... - }, - // other fields ... -} -``` +Value holder is one special kind of auxiliary variables and can be introduced to capture the value of a Verilog variable at a certain time or under a certain condition. This is different from directly creating an auxiliary register in RTL. The value of a RTL register is not available for use before it is assigned under the condition, +whereas, the content of a value holder is globally available even before the clock cycle where the specified condition is true. This is achieved with the help of assumptions. -The corresponding generated assumptions will be in the following form: +The following syntax is used to make a value recorder: `value @ condition`, where each of the value and condition part can be RTL signals or expressions. If either the `value` or `condition` is more than a signal name, a pair of parantheses is needed, like `( RTL.v1 + RTL.v2 ) @ RTL.s1.commit`. +Nested value recorders (value recorders in `value` or `condition`) are not allowed. -```text -wire __m10__ = Verilog_state_1 == __ILA_SO_ILA_state_1 ; -wire variable_map_assume___p1__ILA_state_1 = (~ __START__) || (__m10__) ; // __START__ --> Verilog_state_1 == __ILA_SO_ILA_state_1 +### Simple Delay -wire __m12__ = Verilog_state_2 + Verilog_state_3 == ILA_state_2 ; -wire variable_map_assume___p3__ILA_state_2 = (~ __START__) || (__m12__) ; +You can delay a signal by a fixed number of cycles using `signal ## cycle`. For example, if you need the value of signal `RTL.v1` one cycle after `RTL.s1.commit` becomes true for mapping, then you can write `RTL.v1 @ (RTL.s1.commit ## 1)` -wire __m14__ = (~ __START__ ) || ( Verilog_state_3 == ILA_state_3 ) ; -wire variable_map_assume___p5__ILA_state_3 = (~ __START__) || (__m14__) ; +### Phase Trackers -wire __m16__ = (~ __START__ ) || ( Verilog_state_4 == ILA_state_4 ) ; -wire variable_map_assume___p7__ILA_state_4 = (~ __START__) || (__m16__) ; +If the RTL executes the instructions in multiple phases (e.g., pipeline stages), you will need to declare these phases in order to track the progression of the instruction and to find out its time of finish. This requires using phases trackers. +By default, there are two built-in phase trackers: `#decode#` and `#commit#`. +It is recommended to wrapped the phase trackers in a pair of `#`. +The specification of stages will be explain later. -wire __m18__ = ( (~ __START__ ) || ( Verilog_state_5 == ILA_state_5 ) ) && ( ~( ~__START__ && __IEND__ ) || Verilog_state_6 == ILA_state_5 ) ; // __START__ --> match1 && (~__START__ && __IEND__) --> match2 -wire variable_map_assume___p9__ILA_state_5 = (~ __START__) || (__m18__) ; +## Module Naming -// map to an internal Verilog array : element-wise equality -assign __m20__ = ( __ILA_SO_mem_0 == VerilogArray_0_)&&( __ILA_SO_mem_1 == VerilogArray_1_)&&... ; -assign variable_map_assume___p11__ = (~ __START__ )|| (__m20__) ; +When you refer to signal in RTL, you can use something like `RTL.module_instance_name1.module_instance_name2.signal` to refer to it. And if you use a variable (either input or state variable) in ILA, you can use the format `ILA.var_name`. -// map to an external Verilog array : using memory abstraction -// no assumption is needed -``` +## State Mapping and Input Mapping -and the assertions: +The state mapping in the JSON file is a map data structure. The keys of this map are the state variable names in the ILA model while the value of the map can be (1) a refinement expression, (2) a list of condition-refinement expression pairs for conditional mapping (a pair is written as a list of two elements) (3) a memory expression for mapping internal array in RTL, or (4) a map following a pre-defined template for external memory. And below shows the syntactic structure of state mapping: -```text -wire __m0__ = Verilog_state_1 == __ILA_SO_ILA_state_1 ; -wire variable_map_assert___p1__ILA_state_1 = (~ __IEND__) || (__m0__) ; // IEND --> Verilog_state_1 == __ILA_SO_ILA_state_1 +```javascript +{ + "state mapping": { + "ILA_bitvec_state_var_1" : "", // case 1 + "ILA_bitvec_state_var_2" : [ + ["", ""], + ["", ""]], // case 2 + "ILA_mem_state_var_1" : "", // case 3 : internal RTL memory + "ILA_mem_state_var_2" : { // case 4 : external RTL memory + "wen" : "", + "waddr" : "", + "wdata" : "", + "ren" : "", + "raddr" : "", + "rdata" : "" + }, + // more ... + }, + // other fields ... +} +``` -wire __m2__ = Verilog_state_2 + Verilog_state_3 == ILA_state_2 ; -wire variable_map_assert___p3__ILA_state_2 = (~ __IEND__) || (__m2__) ; +For conditional mapping, the list of conditions has a priority. The first listed condition will be tested first, and if it is true, the first refinement expression will be used and then comes to the second and third. -wire __m4__ = (~ __START__ ) || ( Verilog_state_3 == ILA_state_3 ) ; -wire variable_map_assert___p5__ILA_state_3 = (~ __IEND__) || (__m4__) ; +A memory expression allows more than a Verilog array name, because sometimes, the mapping for array variables is not one-to-one. We support conditional mapping in this case, you can specify it in the similar syntax as case (2), or you can use ` conditon ? var1 : var2 `. -wire __m6__ = (~ __START__ ) || ( Verilog_state_4 == ILA_state_4 ) ; -wire variable_map_assert___p7__ILA_state_4 = (~ __IEND__) || (__m6__) ; +For an external memory, the mapping is actually between interface signals. The ILA array variables use 6 interface signals (see the table below) which should be mapped with the RTL signals. You can use refinement expression or condition-refinement pair for these signal mapping. Later, we shall see some examples of mapping internal or external arrays in ILA with either internal or external arrays in RTL. -wire __m8__ = ( (~ __START__ ) || ( Verilog_state_5 == ILA_state_5 ) ) && ( ~( ~__START__ && __IEND__ ) || Verilog_state_6 == ILA_state_5 ) ; // __START__ --> match1 && (~__START__ && __IEND__) --> match2 -wire variable_map_assert___p9__ILA_state_5 = (~ __IEND__) || (__m8__) ; +| interface signals | meaning | +|------------- |-------------- | +| ren | read enable | +| raddr | read address | +| rdata | read data | +| wen | write enable | +| waddr | write address | +| wdata | write data | -// map to an internal Verilog array : element-wise equality -assign __m10__ = ( __ILA_SO_mem_0 == VerilogArray_0_)&&( __ILA_SO_mem_1 == VerilogArray_1_)&&... ; -assign variable_map_assert___p11__ = (~ __IEND__ )|| (__m10__) ; -// map to an external Verilog array : using memory abstraction -absmem #( - .AW(32), - .DW(8), - .TTS(4294967296) ) -mi0(..., .mem_EQ_(mem_EQ_) ); -assign variable_map_assert__p13__ = (~ __IEND__) || (mem_EQ_) ; -``` +The `input mapping` is similar to `state mapping` but there the keys are the ILA input variables. Currently, input variables with array type are not supported. -One note in the above example: the condition can refer to special signals \(`__START__` and `__IEND__`\), which are the condition when the instruction-under-verification starts to execute and finishes. -## Instruction Completion Condition +## Other Sections in Variable Mapping -The instruction completion condition is specified per instruction. In the JSON file, it is a list of maps. The list does not need to be a full list of instructions. Those not in the list will not be verified. Each dictionary must have an element whose key is `instruction` and the value of this element is the name of the instruction in the ILA model. Besides this name element, it must contain one of the `ready bound` or the `ready signal` element. The `ready bound` specifies a bound that the instruction takes. It is used for instructions that take a fixed number of cycles. Alternatively, one can provide a signal \(or a predicate\) in the `ready signal` field. +Within the same file of variable mapping, there are other sections: (1) clock and reset mapping, (2) clock and reset configuration, (3) uninterpreted function mapping, (4) additional mapping (5) assumptions and (6) RTL monitors. -There are several optional fields. They are `start condition`, `max bound`, `flush constraint`, `pre-flush end` and `post-flush end`. -The `start condition` field, if provided, should be a list of strings. Each string is a Verilog expression that acts as a predicate on the Verilog design. It can be used to constrain the Verilog implementation state, because usually there are more microarchitectural \(implementation states\) in the design. For the starting state of an instruction, these microarchitectural states should be `consistent` with the visible states in the ILA, and you can use this field to enforce the `consistency` at your discretion. You can use `$decode$` and `$valid$` to refer to the instruction's decode function or its ILA valid condition. +### Interface Mapping -The `max bound` can be used when `ready signal` field is provided. It provides an assumption that the condition that the `ready signal` field specified will occur in the given number of cycles, and this will limit the model checking to that bound. Usually this is used for the additional environment assumptions about the input \(for example, how many cycles at most there are for a request to be served with a response\). +The interface mapping is used to specify which input port(s) is/are clock or reset signals. An example is shown below. The `CLOCK` field is a map from the name of the clock to the input pins. If there is only one clock, you can provide either a single input pin or multiple pin names in list which will be connected to the same clock. For reset, you can choose among the active-high/active-low or custom reset patterns using `RESET`, `NRESET` or `CUSTOMRESET`. -The `flush constraint`, `pre-flush end` and `post-flush end` signals are used when using the flushing verification setting. For this verification setting, you can refer to [TODAES19](https://bo-yuan-huang.github.io/ILAng-Doc/todaes18.pdf) on the ILA-based verification or the [Burch-Dill's approach](https://dl.acm.org/citation.cfm?id=735662) on processor verification. +By default, all input ports are connected as the wrapper's input and all output ports are connected with the wrappper's output. In case you want to specify how the input ports should be connected, you can use the `INPUT PORTS` field. -## Global Invariants -In the verification of instructions, we do not assume the design starts from the initial states. This helps us to get a better guarantee of the instruction correctness when only bounded model checking is used. However, if there is no constraints on the starting state of an instruction, there might be spurious bugs just because the design starts from a state that it will never reach when started from the reset state. In order to avoid this false positive, we use global invariants to constrain on the starting state. These invariants help rule out some unreachable states and the tool will generate a separate target to check whether the provided invariants are globally true or not. These invariants should be provided as a list of strings, where each string is a Verilog predicate. In the future, we will exploit invariant synthesis techniques to help synthesize these invariants. +```javascript + "RTL interface connection": { + // below creates two clocks : clkA and clkB + // clkA is connected to wclk + // and clkB is connected to rclk and clk + "CLOCK" : { "clkA" : "wclk", "clkB" : ["rclk", "clk"] }, + // or "CLOCK" : "clk" , single clock -- single pin + // or "CLOCK" : ["wclk", "rclk"] , multiple input pins use + // the same single clock + "RESET" : "reset", // you can have a list of signals here + "NRESET" : ["nreset1", "nreset2"], // like this + "CUSTOMRESET" : {"name" : "input-pin", ...}, + "INPUT PORTS" : { + "" : "" + } + } +``` -## Interface Signal Information -The Verilog module comes with a set of I/O signals and the tool needs to know how these signals should be connected. The `interface mapping` field is a map whose keys are the Verilog I/O signal names and whose values can be one of the following: -* An ILA input name. This means that the Verilog input signal corresponds to one ILA input. They must have the same encoding and bit-width. -* `**KEEP**` directive. Telling the tool to have a wire of the same name and to connect it as the verification wrapper I/O. -* `**NC**` directive, indicating that this port does not need to be connected. -* `**SO**` directive, indicating that this is actually a direct output from a visible state variable \(a state variable that is modeled in the ILA\). -* `**RESET**` or `**NRESET**` directive. Indicating that this signal is the reset signal, active-high or active-low \(we assume synchronous reset\). -* `**CLOCK**` directive, indicating that this is the clock signal. -* `**MEM**name.signal` directive, indicating this signal is the connection to an external/shared memory. The name part should be the ILA state variable name of the memory, and the signal part could be one of the following: `wdata`,`rdata`, `waddr`,`raddr`, `wen`, `ren`. If the signal does not directly correspond to the write/read data, write/read address, write/read enable signal, it should be specified as `**KEEP**`, you can specify the mapping using "annotation" which will be dicussed below. -For example, for a Verilog input signal `control`, the effects of applying different directives are: +### Clock and Reset Configuration -* An ILA input name, e.g., `c1`. The tool will check if ILA indeed has the input `c1` and the type is matched. The wire `__ILA_I_c1` will be created and will be connected to the input port `control`. -* `**KEEP**` directive. The tool will check if the signal is input or output and create an input/output wire named `__VLG_I_control` with the proper width and connect to the port. -* `**NC**` directive. The tool will have it unconnected like `.control()`. -* `**SO**` directive. The tool will check if it is indeed an output and create an output wire `__VLG_SO_control` and connect to the port. In this example, because it is actually an input, the tool will give warning. -* `**RESET**` or `**NRESET**`. It will be connected as `.control(rst)` or `.control(~rst)`, where `rst` is the reset signal of the wrapper. -* `**CLOCK**` directive. It will be connected as `.control(clk)`, where `clk` is the clock signal of the wrapper. -* `**MEM**name.signal`. The tool will check if `name` is an ILA memory name. It will be connected as `.control(__MEM_name_0_signal)`. +In the interface mapping part, the clock and reset pins are specified. If there is one clock and the reset sequence is just one cycle, you don't need to explicitly state the clock and reset configurations. -## Notes on Memory State Variable +In the `reset` section, you can specify (1) the initial state (2) the length of the reset sequence, and (3) the custom reset sequence. A sequence is list of 0s or 1s. You can duplicate a sequence by adding a `"*N"` element in the end, where `N` is the number of copies to make. If you don't need reset sequence, you can set `cycles` to 0. And if both reset sequence and the initial state are provided, the RTL design will go through a reset sequence after the specified initial state. -Memory state variable might be internal or external to the module. An internal memory variable corresponds to a verilog array, and therefore no specific I/O interface is needed to access the memory. An external memory is a memory that connects with the current module via I/O interface. By default, all memory variables in the ILA are treated as external memory. The default setting can be override by _annotation_ in refinement map, and here is an example: +An example of the `reset` section is provided below. ```javascript - "annotation" : { - "memory" : { - "rf":"internal", - "mem":"external" - } - } + "reset" : { + "initial-state" : { + // this can be used with/without the reset sequence + "RTL.v1" : "1'b1", + "RTL.v2" : "2'b01", + ... + }, + "cycles" : 5, + // or 1 by default, this affects RESET, NRESET, CUSTOMRESET.n + // if you don't need reset, use 0 here + "custom-seq" : {"CUSTOMRESET.1": [0 , [1, "*3"], [0, "*1"] ] } +} ``` -The above annotation specifies memory named as `rf` and `mem` as internal and external respectively. Being internal or external affects how properties are generated. The mapping of internal memory is element-wise with expressions comparing two verilog arrays entry by entry, which is inefficient for a large memory. The mapping of external memory will use memory abstraction, which is more efficient. \(In the future, we will support mapping internal memory using the Array data-type of the underlying property verifier.\) +The `clock` section is only needed if you have multiple clocks. Currently, the tool will only handle the case where the frequency of the clock signals have a least common multiple. Therefore, they can be simulated using a single clock signal. The `clock` tells the tool how to simulate this clock signal. +This can be specified using either `custom` or `factor` field. The `custom` field should be sequences of 0s and 1s where you can use the similar duplicate operator as in the custom sequence of reset configuration. Alternatively, you can use the `factor` section to specify how many cycles of 0s and 1s and the starting offset of each clock. + + +An example of the `clock` section is provided below, where using the `factor` field and the `custom` field actually creates the same set of clock signals. -For the external memory, it is likely that there isn't a one-to-one mapping between the module interface and the six signals required by the memory abstraction module: `wdata` (write-data) ,`rdata` (read-data), `waddr` (write-address),`raddr` (read-address), `wen` (write-enable), `ren` (read-enable). Therefore, we support specifying the mapping using the annotation here. An example of the syntax is given below. ```javascript - "annotation" : { - "memory-ports" : { - "MemoryName.port1" : "Verilog-expression-here", - "MemoryName.port2" : "Verilog-expression-here" - } - } + "clock" : + { + "factor" : { + "clkA" : { + "high" : 6 + "low" : 6 + // 12x gclk's period + }, + "clkB" : { + "high" : 2 + "low" : 1 + // 3x gclk's period + // duty cycle 2/3 + }, + "clkC" : { + "high" : 2 + "low" : 4, + "offset" : 3 + // 6x gclk's period + // duty cycle 1/3 + // 1 1 0 0 0 0 + // start:^ + // offset should be positive + } + // tool will calcuate the min length + // LCM(12,3,6) = 12 + } + } + + // Alternatively, you can use the custom field. + // Using both the factor and custom fields is + // not allowed. + "clock" : + { + "custom" : { + "length" : 12, + "clocks": { + "CLOCK.1": [ [1, "*6"], [0,"*6"] ], + "CLOCK.2": [ [1, 1, 0], "*4" ], + "CLOCK.3": [ [0, "*3"], [1, "*2"] , [0, "*4"] , [1, "*2"], 0 ] + } + } + } + ``` -In the above example, `MemoryName` should be the name of the memory state variable in ILA and `port1`, `port2` should be one of `wdata` (write-data) ,`rdata` (read-data), `waddr` (write-address),`raddr` (read-address), `wen` (write-enable), `ren` (read-enable). The Verilog expression after the colon represents how to use the Verilog signal to compute the interface signals. -Note that this kind of mapping assumes the ports of an abstract memory state can be represented as a function of solely the Verilog signals. If this is not feasible for the design you are looking at, you can use the additional mapping capability provided by `mapping control` section described later in this chapter. -## Uninterpreted Function Mapping +### Uninterpreted Function Mapping -The ILA model may use uninterpreted functions, however, in the verification, the tool must know the correspondence of this uninterpreted function in order to reason about the correctness. In the `functions` field of the _var-map_ JSON, a map should be provided if uninterpreted function is used in the ILA model. The keys of the map are the function names, with the values in a list. Each element of this list is for one application of this function. Per each function application, the tool needs to know the correspondence of the arguments/result in the Verilog and when that happens, this is like a condition/mapping pair, and it is specified as a list. The correspondence of the function result goes first followed by the arguments \(in the same order as the arguments in ILA function definitions\). +The ILA model may use uninterpreted functions, however, in the verification, the tool must know the correspondence of this uninterpreted function in order to reason about the correctness. In the `functions` field of the _var-map_ JSON, a list should be provided if uninterpreted function is used in the ILA model. +Each element of this list is for one application of this function. Per each function application, the tool needs to know the correspondence of the arguments/result in the Verilog. And this is specified with a map. The keys of the map are the function names, with the values also in a map containing `result` and `arg` fields. `result` field accepts a single refinement expression while `arg` accepts a list. For example in the ILA there is such specification @@ -231,59 +291,158 @@ For example in the ILA there is such specification instr.SetUpdate(state0, div(arg0, arg1) ); ``` -Then in the refinement map +Then in the refinement map, `div` is followed by a list of one element (because there is only one function application in ILA). ```javascript { "functions" : { - "div" : [ - ["cond1", "verilog-signal-result", "cond2", "verilog-signal-arg0", "cond3", "verilog-signal-arg1", ] + "div" : [ { + "result" : "", + "arg" : [ + // there are only two arguments in div + "", + "" + ] + } ] } } ``` -## Additional Mapping +### Additional Mapping -Sometimes, the mapping between Verilog variables and ILA state variables does not fit easily into the state mapping section. For example, you may need a customized mapping from the Verilog design's memory interface to the provided 6-signal memory interface. The AES case study provides an example of this. The Verilog design uses two signals `stb` and `wr` to indicate memory read and write enable, which are different from the `ren` and `wen` signals. Therefore a mapping can be provided as follows: +Sometimes, the mapping between Verilog variables and ILA state variables does not fit easily into the state mapping section. +In this case you specified additional mapping using `additional mapping` section. It takes a list of strings and each string should be a valid Verilog expression. This will be translated as assumptions, which only appear when verifying individual instructions and will not be used when checking or synthesizing starting state invariants. ```javascript -"mapping control" : [ - "( wr & stb) == __MEM_XRAM_0_wen" , - "(~wr & stb) == __MEM_XRAM_0_ren" +"additional mapping" : [ + "( RTL.wr & RTL.stb) == (ILA.m1 & ILA.m2)" , + "(~RTL.wr & RTL.stb) == (ILA.m2 & ILA.m3)" ] ``` -Assumptions in the `mapping control` section does not appear in the invariant or invariant synthesis target. - -## Additional Assumptions +### Additional Assumptions This section allows users to add additional assumptions in the verification. They can be, for example, an assumption about the module I/O. ```javascript "assumptions" : [ // the two inputs can not be both 1 - "! ( verilog_module.input1 & verilog_module.input2 )" + "! ( RTL.input1 & RTL.input2 )" ] ``` Assumptions in this section are in effect when verifying the instructions, the invariants and when synthesizing the invariants. -## Value Holder +### RTL Monitors + +RTL monitors are additional logic and states that are added to aid the specification of refinement mapping. +Our tool provides two templates (value recorder and phase tracker) and also allows arbitrary synthesizable Verilog to be used. + +#### Phase Tracker + +Phase tracker is a template for creating auxiliary variables to track the phase of an instruction. An example is shown below. +It defines 4 phases, and the rules of entering and exiting each phase is specified in the `rules` field. +For each phase, you can give it name, otherwise you can refer to it as `phaseX` where `X` is an index number starting from 1. +There are two phases that are implicitly declared, which are `#decode#` and `#commit#`. +The entering condition should explicitly have its previous stage in the conjunction. + + +```javascript + "monitor" : { + "tracker" : { // this is just a name + "template" : "phase tracker", + "event-alias" : { // will be translated as creating 1-bit wire + "issue" : "SomeVerilogExpressionsHere", + // for example + "i2e" : "RTL.s2_to_s3 & RTL.s2_to_s3", + "e2c" : "RTL.s3_deq & RTL.s3_deq" + }, + "rules" : [ + { // 1 + "enter" : { + "event" : "issue & #decode#" + }, + "exit" : { + "event" : "i2e" + } + }, + { // 2, if you give it a name, then + "name" : "second_phase" + "enter" : { + "event" : "i2e & #phase1#" + }, + "exit" : { + "event" : "e2c" + // it is redundant to add & #phase2# + } + }, + { // 3 + "enter" : { // you can use the name elsewhere + "event" : "e2c & #second_phase#", + }, + "exit" : { + "event" : "e2c ## 1", + } + } + ] + // instantiate a phase tracker template + // each template has its other fields + // to fill in + } +``` + +Additionally, you can declare alias for events which can be referred to in the rules. You can also define auxiliary variables and update them using actions. Below shows an example of tracking a command/instruction through a FIFO. When the command/instruction enters the FIFO, we need to take down the write pointer of the FIFO (stored in auxiliary variable `fifo_ptr`) so that we can know when the command/instruction gets out of the FIFO. + + +```javascript + "monitor" : { + "TrackingThroughFifo" : { // this is just a name + "template" : "phase tracker", + "aux-var" : [ ["fifo_ptr", "reg", 8] ], + "rules" : [ + { // 1 + "enter" : { + "event" : "RTL.fifo_wen & #decode# ", + "action" : "fifo_ptr <= RTL.fifo_wptr;" + }, + "exit" : { + "event" : "RTL.fifo_ren & RTL.fifo_rptr == fifo_ptr" + } + }, + { // 2 + "enter" : { + "event" : "RTL.fifo_ren & RTL.fifo_rptr == fifo_ptr & #phase1#" + }, + "exit" : { + "event" : "..." + } + } + ] + } + } +``` + +The phase tracker also allows specifying branching and convergence. This is useful, for example, in the verification of superscaler out-of-order processor implementation, where there are multiple pipelines and instructions can be dynamically dispatched to some processing pipelines. A phase can be referred to in other parts of the refinement specification using `#MonitorName_PhaseName#` (unnamed stages are named as `stageX` where X is the index in the list of rules, and the index starts from 0). + + +#### Value Recoder + +Value recorder can be created using `value @ condition` syntax in the refinement expressions. Alternatively, you can also create explicit value recorders. An example showing the syntax for specifying explicit value recorder is provided below. For the `width` field, you can also use `"auto"` to ask the tool to automatically infer the width needed to hold the value. -Value holder \(a.k.a prophecy variables, auxiliary variables and etc.\) can be introduced to capture the value of a Verilog variable at a certain time \(or under a certain condition\). Below is an example of a value holder: ```javascript -"value-holder": { - "r1_pvholder" : { - "cond": "m1.write_enable == 1", - "val":"m1.registers[1]", + "monitor" : { + "r1_pvholder" : { // this is just a name + "template" : "value recorder", + "cond": "RTL.write_enable == 1", + "val":"RTL.registers[1]", "width":8 - } -} + } + } ``` -The above value holder will be translated to the following Verilog code fragments in the Verilog. +The above value recorder will be translated into the corresponding Verilog below. ```text input [7:0] __r1_pvholder_init__; @@ -293,37 +452,84 @@ always @(posedge clk) begin if(rst) begin r1_pvholder <= __r1_pvholder_init__; end - else if(1) begin + else begin r1_pvholder <= r1_pvholder; end end -assume property ((m1.write_enable == 1) |-> ((r1_pvholder) == (m1.registers[1]))); +assume property ((RTL.write_enable == 1) |-> ((r1_pvholder) == (RTL.registers[1]))); ``` -It creates an auxiliary Verilog variable `r1_pvholder` which carries a undetermined value. Its value keeps the same all the time, and an assumption says this undetermined value is same as the specified value `m1.registers[1]`, under the condition that `m1.write_enable == 1`. This variables can be referenced in other sections by `#r1_pvholder#` \(this tells the tool not to find this signal name in the original Verilog design. The `width` part can also be a string `"auto"`, which tells the tool to automatically determine the width \(in case of failure, error will be prompted.\) This value holder does not check if there is only one cycle that `m1.write_enable == 1` holds. If there are multiple cycles that its condition holds, the assumption may overconstrain if `m1.registers[1]` should carry different values at these points. This situation should be avoided. +It creates an auxiliary Verilog variable `r1_pvholder` which carries a undetermined value. Its value keeps the same all the time, and an assumption says this undetermined value is same as the specified value `RTL.registers[1]`, under the condition that `RTL.write_enable == 1`. This variables can be referenced in other sections by `r1_pvholder`. This value holder does not check if there is only one cycle that `RTL.write_enable == 1` holds. If there are multiple cycles that its condition holds, the assumption may overconstrain if `RTL.registers[1]` should carry different values at these points. This situation should be avoided. -## Verilog Monitor -In the case that user may want to add customized auxiliary variables, we support inline monitors for this purpose. +#### Arbitrary Verilog -An example is given as follows: +You can also add arbitrary synthesizable Verilog as the monitor. An example is shown below: ```javascript - "verilog-inline-monitors" : { - "stage_tracker" : { + "monitor" : { + "counter" : { "verilog": ["always @(posedge clk) begin", - " if (__START__) stage_tracker <= 0;", - " else if (__STARTED__ && !__ENDED__) stage_tracker <= stage_tracker + 1;", + " if (RTL.signal_1) counter <= 0;", + " else if (RTL.signal_2 && ! RTL.signal_3) counter <= counter + 1;", "end"], - "defs" :[ ["stage_tracker", 2, "reg"] ], - "refs" :[] + "defs" :[ ["counter", 2, "reg"] ], + "refs" :[ "RTL.signal_1" , "RTL.signal_2", "RTL.signal_3" ] }, } ``` -This creates a 2-bit variable `stage_tracker` to track the number of cycles \(this is just for demoing the syntax of Verilog monitor, you can in fact use the embedded variable `__CYCLE_CNT__` to track the number of cycles\). Variables that should be accessible outside the monitor should be defined in the `defs` list with its name, bit-width and its type: `reg` or `wire`. Variables used only inside the monitor can be defined inside the `verilog` code list. Any variable inside the original Verilog, if referenced, should be put in the list of `refs`. This will help our tool to add auxiliary wires to connect them with the monitor. +This creates a 2-bit variable `counter` to count the number of cycles under a certain condition. Variables that should be accessible outside the monitor should be defined in the `defs` list with its name, bit-width and its type: `reg` or `wire`. Variables used only inside the monitor can be defined inside the `verilog` code list. Any variable inside the original Verilog, if referenced, should be put in the list of `refs`. This will help our tool to add auxiliary wires to connect them with the monitor. + +Monitors are normally only in effect when verifying instructions. If you want a monitor to appear also when verifying the invariants, you can add the `"keep-for-invariants":true` attribute in the monitor's description following the `defs` and `refs` attributes. + +Additionally, you can load Verilog from file using `"verilog-from-file":""` instead of the ` +verilog` field above. You can also have additional Verilog appended to the generated wrapper using field `append-verilog` and `append-verilog-from-file`. + + +## Instruction Completion Condition + + + +The instruction completion condition is specified per instruction. In the JSON file, it is a list of maps. The list does not need to be a full list of instructions. Those not in the list will not be verified. Each dictionary must have an element whose key is `instruction` and the value of this element is the name of the instruction in the ILA model. Besides this name element, it must contain one of the `ready bound` or the `ready signal` element. The `ready bound` specifies a bound that the instruction takes. It is used for instructions that take a fixed number of cycles. Alternatively, one can provide a signal \(or a predicate\) in the `ready signal` field. + +There are two optional fields. They are `start condition`, `max bound`. + +The `start condition` field, if provided, should be a list of strings. Each string is a Verilog expression that acts as a predicate on the Verilog design. It can be used to constrain the Verilog implementation state, because usually there are more microarchitectural \(implementation states\) in the design. For the starting state of an instruction, these microarchitectural states should be `consistent` with the visible states in the ILA, and you can use this field to enforce the `consistency` at your discretion. You can use `$decode$` and `$valid$` to refer to the instruction's decode function or its ILA valid condition. + +The `max bound` can be used when `ready signal` field is provided. It provides an assumption that the condition that the `ready signal` field specified will occur in the given number of cycles, and this will limit the model checking to that bound. Usually this is used for the additional environment assumptions about the input \(for example, how many cycles at most there are for a request to be served with a response\). + + +### The Structure of Instruction Completion Condition + +The structure of the instruction completion condition is relatively simple as shown below. `max bound` and `start condition` are optional, and you can only choose one between `ready bound` and `ready signal`. + + +```javascript +{ + "instructions": + [ + { + "instruction" :"", + "ready bound" :12345, // + "ready signal" :"", + "max bound" :12345, // + "start condition" :"" + } + ], + + "global invariants" : + [ + "Verilog-expressions-here", + ... + ] +} +``` + +### Global Invariants + +In the verification of instructions, we do not assume the design starts from the initial states. This helps us to get a better guarantee of the instruction correctness when only bounded model checking is used. However, if there is no constraints on the starting state of an instruction, there might be spurious bugs just because the design starts from a state that it will never reach when started from the reset state. In order to avoid this false positive, we use global invariants to constrain on the starting state. These invariants help rule out some unreachable states and the tool will generate a separate target to check whether the provided invariants are globally true or not. These invariants should be provided as a list of strings, where each string is a Verilog predicate. -Value holders and monitors are normally only in effect when verifying instructions. If you want a monitor to appear also when verifying the invariants, you can add the `"keep-for-invariants":true` attribute in the monitor's description following the `defs` and `refs` attributes. diff --git a/verification/target.md b/verification/target.md index a13480d..2c8801f 100644 --- a/verification/target.md +++ b/verification/target.md @@ -1,20 +1,27 @@ # Verification Target -The verification target can be generated by create a `VerilogVerificationTargetGenerator` object. Some prerequisites are: - -1. ILAng should be configured to have the switch `ILANG_INSTALL_DEV` turned on. -2. Include the header `ilang/vtarget-out/vtarget_gen.h` +The verification target can be generated by creating the `IlaVerilogRefinementChecker` object. The arguments of the constructors are: -1. A list of paths to search for Verilog include files -2. A list of Verilog design files -3. The Verilog top module -4. The variable mapping file \(first part of refinement map\) -5. The instruction start/ready conditions \(second part of refinement map\) -6. The output path of the verification targets -7. The ILA model -8. The choice backend \(CoSA/JapserGold, the latter is not open-source and not included in the demo\) -9. \(Optional\) Target generator configuration -10. \(Optional\) Verilog generator configuration +1. The ILA object +2. A list of paths to search for Verilog include files +3. A list of Verilog design files +4. The Verilog top module +5. The variable mapping file \(first part of refinement map\) +6. The instruction start/ready conditions \(second part of refinement map\) +7. The output path of the verification targets +8. The choice of backend, which can be either `ModelCheckerSelection::JASPERGOLD` or `ModelCheckerSelection::PONO` +9. \(Optional\) Verilog generator configuration + +Some of the useful options are listed below (see `include/ilang/rtl_verify.h` for a full list): + + +| Option | Meaning | Possible values | +|---------------------|-----------------|-------------| +| ForceInstCheckReset | Whether to start from an arbitrary state | true/false | +| PonoEngine | Engines for Pono | "ind", "bmc", "ic3ia", "ic3sa", ... | +| PonoOtherOptions | Additional options for Pono | e.g., " -v 1 " sets verbose level to be 1. | +| YosysSmtArrayForRegFile | Whether to use SMT arrays for Verilog arrays | true/false | +