Jasper connectivity check

Unknown said:

<snip>

Now that I have started implementing rules for a real project, I do have some additional questions.

1) Is a rule as follows allowed:

 

CONNECTION, id_1, ,~inp,,op

Jose> Yes this is allowed.

Please notice the ~ operator at the source signal. I ask this as I have seen most of the description for connectivity talk about input to output propagation with a lot of conditions. But in the above case, there is an change in signal value (inverted output).

if this is not acceptable then is there an alternate way to describe this?

2) I want to use constants while writing the rules

   a) can I use alias to do this?

   b) can I use `define from Verilog/SystemVerilog

 

  For example, is the following allowed:

  e.g. 1  (t_mode == `TRUE)

 TRUE is a define in my Verilog file

 

 e.g. 2 (t_mode = TRUE)

 TRUE is defined as 1'b1 Alias in the rule file

 Jose> I need to research this.  I believe an ALIAS will work as we simply do a search and replace in connectivity spec. Give it try.  Not sure about Verilog defines.

3) One main use-case of Connectivity checker is for pin muxing logic.

Normally, these modules don't have clock. So, how to specify to tool that there is no reset or clock to the module?

 Jose> For clock simply issue:  "clock -none" in tcl file. If you do not have any pipeline connection then you can simply issue:  "reset -none" command in tcl file.

4) When I have to write rules for a 2-1 mux function of DUT, do I have to write 2 connection rules or there is a way to compress this description using a single connection rule?

 Jose> You need to specify 2 rules. One for each connection you want to describe.  If you are familiar with the IFV spreadsheet you can specify the mux connection in a single line but if you are starting with Jasper csv file format then simply specify a line per mux connection. Your example below is correct.

For example,

CONNECTION, id_1, ,inp_1,,op

COND_EXPR, sel == 1'b0

CONNECTION, id_2, ,inp_2,,op

COND_EXPR, sel == 1'b1

 5) The pin mux design I am trying to verify has technology components for mux logic.

I have simulation models for these technology components. These are behavioral codes.

Is there any guideline for handling tech. components in Jasper?

Jose> Jasper and formal tools consume only synthesizable rtl only.  Sorry.

Thanks a lot ... 

Unknown said:

<snip>

Now that I have started implementing rules for a real project, I do have some additional questions.

1) Is a rule as follows allowed:

 

CONNECTION, id_1, ,~inp,,op

Jose> Yes this is allowed.

Please notice the ~ operator at the source signal. I ask this as I have seen most of the description for connectivity talk about input to output propagation with a lot of conditions. But in the above case, there is an change in signal value (inverted output).

if this is not acceptable then is there an alternate way to describe this?

2) I want to use constants while writing the rules

   a) can I use alias to do this?

   b) can I use `define from Verilog/SystemVerilog

 

  For example, is the following allowed:

  e.g. 1  (t_mode == `TRUE)

 TRUE is a define in my Verilog file

 

 e.g. 2 (t_mode = TRUE)

 TRUE is defined as 1'b1 Alias in the rule file

 Jose> I need to research this.  I believe an ALIAS will work as we simply do a search and replace in connectivity spec. Give it try.  Not sure about Verilog defines.

3) One main use-case of Connectivity checker is for pin muxing logic.

Normally, these modules don't have clock. So, how to specify to tool that there is no reset or clock to the module?

 Jose> For clock simply issue:  "clock -none" in tcl file. If you do not have any pipeline connection then you can simply issue:  "reset -none" command in tcl file.

4) When I have to write rules for a 2-1 mux function of DUT, do I have to write 2 connection rules or there is a way to compress this description using a single connection rule?

 Jose> You need to specify 2 rules. One for each connection you want to describe.  If you are familiar with the IFV spreadsheet you can specify the mux connection in a single line but if you are starting with Jasper csv file format then simply specify a line per mux connection. Your example below is correct.

For example,

CONNECTION, id_1, ,inp_1,,op

COND_EXPR, sel == 1'b0

CONNECTION, id_2, ,inp_2,,op

COND_EXPR, sel == 1'b1

 5) The pin mux design I am trying to verify has technology components for mux logic.

I have simulation models for these technology components. These are behavioral codes.

Is there any guideline for handling tech. components in Jasper?

Jose> Jasper and formal tools consume only synthesizable rtl only.  Sorry.

Thanks a lot ...