Skip to content

Commit

Permalink
Add Xprova codegen templates
Browse files Browse the repository at this point in the history
  • Loading branch information
@gtarawneh
gtarawneh committed Nov 21, 2017
1 parent 728124d commit 4137d9a
Show file tree
Hide file tree
Showing 4 changed files with 456 additions and 26 deletions.
12 changes: 6 additions & 6 deletions templates/circuit.v → templates_ifv/circuit.v
View file
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
// vi: set ft=verilog :

module circuit (
input reset
, input clk
{{- ", det" if dbits -}}
input reset,
input clk,
{{- "det," if dbits -}}

{%- for input in inputs %}
, input {{ input }}_precap // input
input {{ input }}_precap, // input
{%- endfor %}

{%- for input in outputs|sort %}
, output {{ input }} // output
{%- for input in outputs %}
output {{ input }} {{- "," if not loop.last }} // output
{%- endfor %}
);

Expand Down
41 changes: 21 additions & 20 deletions templates/spec.v → templates_ifv/spec.v
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,20 +5,20 @@
`define clk_rst @(posedge clk) disable iff (reset)

module spec (
input reset
, input clk
, input [{{firebits-1}}:0] fire
input reset,
input clk,
input [{{firebits-1}}:0] fire,

{%- for net in nets %}
, input {{net}}
input {{net}},
{%- endfor %}

{%- for net in nets %}
, input {{net}}_precap
input {{net}}_precap {{- "," if not loop.last or stateless_outs}}
{%- endfor %}

{%- for output in stateless_outs %}
, input {{ output }} // (stateless) output
input {{ output }} {{- "," if not loop.last}} // (stateless) output
{%- endfor %}
);

Expand Down Expand Up @@ -60,8 +60,9 @@ module spec (
{%- set sign = tr[-1] -%}
{%- set from_ind = state_inds[from] -%}
{%- set to_ind = state_inds[to] -%}
{%- set fire_ind = firing_indices[signal] -%}
{%- set verilog_tr = ("~" + signal) if sign == "-" else signal %}
if (state == {{ from_ind }} && {{ verilog_tr }}) state <= {{ to_ind }}; // {{ to }}
if (state == {{ from_ind }} && {{ verilog_tr }}_precap && fire == {{fire_ind}}) state <= {{ to_ind }}; // {{ to }}
{%- endfor %}

end
Expand Down Expand Up @@ -90,14 +91,14 @@ module spec (

// Assumptions (spec compliance):
{% for input in inputs %}
compliance_{{input}}_rise: assume property ( `clk_rst $rose({{input}}) |-> {{input}}_can_rise );
compliance_{{input}}_fall: assume property ( `clk_rst $fell({{input}}) |-> {{input}}_can_fall );
compliance_{{input}}_rise: assume property ( `clk_rst $rose({{input}}) |-> $past({{input}}_can_rise) );
compliance_{{input}}_fall: assume property ( `clk_rst $fell({{input}}) |-> $past({{input}}_can_fall) );
{%- endfor %}

// Assertions (spec compliance):
{% for output in outputs %}
compliance_{{output}}_rise: assert property ( `clk_rst $rose({{output}}) |-> {{output}}_can_rise );
compliance_{{output}}_fall: assert property ( `clk_rst $fell({{output}}) |-> {{output}}_can_fall );
compliance_{{output}}_rise: assert property ( `clk_rst $rose({{output}}) |-> $past({{output}}_can_rise) );
compliance_{{output}}_fall: assert property ( `clk_rst $fell({{output}}) |-> $past({{output}}_can_fall) );
{%- endfor %}

// Enable signals:
Expand All @@ -116,13 +117,13 @@ module spec (

// Output Persistency Properties:
{% for net in stateful_nets %}
persistency_{{net}}: assert property ( `clk_rst {{net}}_ena |=> ({{net}}_ena || ~$stable({{net}})) );
// persistency_{{net}}: assert property ( `clk_rst {{net}}_ena |=> ({{net}}_ena || ~$stable({{net}})) );
persistency_{{net}}: assert property ( `clk_rst $fell({{net}}_ena) |-> ~$stable({{net}}) );
{%- endfor %}

// Deadlock

// Deadlock freeness: on each cycle, at least one internal transition is
// enabled or an input can change.
// Deadlock freeness: on each cycle, at least one transition is enabled.

assign exist_enabled_transition =
{%- for input in inputs %}
Expand All @@ -140,7 +141,7 @@ module spec (
// );

deadlock_free: assert property ( `clk_rst
not (##[1:$] ~exist_enabled_transition)
exist_enabled_transition
);

// Transition firing assumptions: a transitions can only be fired when
Expand All @@ -162,16 +163,16 @@ endmodule
module bind_info();

bind circuit spec u1 (
.reset(reset)
, .clk(clk)
, .fire(fire)
.reset(reset),
.clk(clk),
.fire(fire),

{%- for net in nets %}
, .{{net}}({{net}})
.{{net}}({{net}}),
{%- endfor -%}

{%- for net in nets %}
, .{{net}}_precap({{net}}_precap)
.{{net}}_precap({{net}}_precap) {{- "," if not loop.last}}
{%- endfor -%}
);

Expand Down
250 changes: 250 additions & 0 deletions templates_xprova/circuit.v
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,250 @@
// vi: set ft=verilog :

// ---- Xprova properties ----

{%- set ntransitions = nets|length %}

// Assumptions (spec compliance):
{% for input in inputs %}
assume $rose({{input}}) |-> @1 {{input}}_can_rise
assume $fell({{input}}) |-> @1 {{input}}_can_fall
{%- endfor %}

// Assertions (spec compliance):
{% for output in outputs %}
assert $rose({{output}}) |-> @1 {{output}}_can_rise
assert $fell({{output}}) |-> @1 {{output}}_can_fall
{%- endfor %}

// Output Persistency Properties (internals must be removed)
{% for net in stateful_nets %}
assert $fell({{net}}_ena) |-> $changed({{net}})
{%- endfor %}

assume fire <= {{ntransitions}}

assert exist_enabled_transition

// Transition firing assumptions:

{% for input in inputs %}
{%- set pre_net = input + "_precap" %}
{%- set fire_ind = loop.index0 -%}
assume (fire == {{fire_ind}}) |-> ({{input}} ^ {{pre_net}})
{% endfor -%}

{% for net in stateful_nets %}
{%- set fire_ind = loop.index0 + inputs|length -%}
assume (fire == {{fire_ind}}) |-> ({{net}} ^ {{net}}_precap)
{% endfor %}
// ---- end of Xprova properties ----

`include "workcraft.v"
`include "gates.v"
`include "builtins.v"

module circuit (
input reset,
input clk,
input [{{firebits-1}}:0] fire,
{{- "det," if dbits -}}

{%- for input in inputs %}
input {{ input }}_precap, // input
{%- endfor %}

{%- for input in outputs %}
output {{ input }}, // output
{%- endfor %}

{%- for signal in inputs+outputs %}
output {{ signal }}_can_fall,
output {{ signal }}_can_rise,
{%- endfor %}
output exist_enabled_transition,

{%- for signal in nets %}
output {{signal}}_ena,
{%- endfor %}

{%- for signal in nets -%}
{%- if signal not in inputs %}
output {{signal}}_precap,
{%- endif -%}
{%- endfor %}
);


{%- for input in inputs %}

{% set initial_value = initial_circuit[input] -%}

// input signal '{{input}}' (initial value = {{initial_value}})

DFF {{input}}_ff (
.CK(clk),
.ST({{ "reset" if initial_value else "1'b0" }}),
.RS({{ "reset" if not initial_value else "1'b0" }}),
.D({{input}}_precap),
.Q({{input}}),
.ENA(fire == {{loop.index0}})
);

{%- endfor -%}

{#-------- Stateful Modules --------#}

{% for instance, mod in stateful.iteritems() %}

{%- set output_pin = get_output_pin(mod) -%}
{%- set output_net = get_output_net(mod) -%}
{%- set output_pre = output_net + "_precap" %}
{%- set category = "output" if output_net in outputs else "internal" -%}
{% set initial_value = initial_circuit[output_net] -%}
{% set fire_ind = firing_indices[output_net] %}

// {{category}} signal '{{output_net}}' (initial value = {{initial_value}})

{%- if lib[mod["type"]]["type"] == "GATE" %}

{#-------- Gate -------- #}

{{mod["type"]}} {{instance}} (

{%- for pin, net in mod["connections"].iteritems() %}
{%- set pin_net = output_pre if pin==output_pin else net -%}
.{{pin}}({{pin_net}}){{ ", " if not loop.last }}
{%- endfor -%}
); {{"// virtual module" if mod.get("virtual")}}

DFF {{instance}}_ff (
.CK(clk),
.ST({{ "reset" if initial_value else "1'b0" }}),
.RS({{ "reset" if not initial_value else "1'b0" }}),
.D({{output_pre}}),
.Q({{output_net}}),
.ENA(fire == {{fire_ind}})
);

{#-------- End of Gate --------#}

{%- else %}

{#-------- Latch -------- #}

{{mod["type"]}} {{instance}} (
.CK(clk),
.RS({{ "reset" if not initial_value else "1'b0" }}),
.ST({{ "reset" if initial_value else "1'b0" }}),
.PRECAP({{output_pre}}),

{%- for pin, net in mod["connections"].iteritems() %}
.{{pin}}({{net}}),
{%- endfor %}
.ENA(fire == {{fire_ind}})
);

{#-------- End of Latch --------#}

{%- endif %}

{%- endfor %}

{#-------- End of Stateful Modules -------- #}

// Stateless modules

{#-------- Non-stateful Modules --------#}

{% for instance, mod in stateless.iteritems() %}

{%- set output_net = get_output_net(mod) -%}

{{mod["type"]}} {{instance}} (

{%- for pin, net in mod["connections"].iteritems() -%}
.{{pin}}({{net}}){{ ", " if not loop.last }}
{%- endfor -%}
);

{%- endfor -%}

{#-------- End of non-stateful Modules -------- #}

// spec

integer state;

always @(posedge clk or posedge reset) begin

if (reset) begin

{%- set initial_ind = state_inds[initial_spec] %}

state <= {{ initial_ind }}; // {{ initial_spec }}

end else begin
{% for from, tr, to in transitions -%}
{%- set signal = tr[:-1] -%}
{%- set sign = tr[-1] -%}
{%- set from_ind = state_inds[from] -%}
{%- set to_ind = state_inds[to] -%}
{%- set fire_ind = firing_indices[signal] -%}
{%- set verilog_tr = ("~" + signal) if sign == "-" else signal %}
if (state == {{ from_ind }} && {{ verilog_tr }}_precap && fire == {{fire_ind}}) state <= {{ to_ind }}; // {{ to }}
{%- endfor %}

end

end

// Spec Compliance Properties:

{%- for signal in inputs + outputs %}

wire {{ signal }}_can_fall = 0
{%- for prior, tr, _ in transitions if tr == signal + "-" %}
{%- set prior_ind = state_inds[prior] %}
{{ "|| (state == %d)"|format(prior_ind) }}
{%- endfor -%}
;

wire {{ signal }}_can_rise = 0
{%- for prior, tr, _ in transitions if tr == signal + "+" %}
{%- set prior_ind = state_inds[prior] %}
{{ "|| (state == %d)"|format(prior_ind) }}
{%- endfor -%}
;

{%- endfor %}


// Enable signals:

// Note: while internal transition enable status are indicated by (net ^
// net_precap), inputs are generated by the environment and may therefore
// may be enabled wile the expression (input ^ input_precap) is false.
// Input enable status must therefore be derived from the spec, as
// input_can_rise | input_can_fall.

{% for input in inputs %}
assign {{input}}_ena = {{input}}_can_rise | {{input}}_can_fall;
{%- endfor -%}
{%- for net in stateful_nets %}
assign {{net}}_ena = {{net}}_precap ^ {{net}};
{%- endfor %}

// Deadlock

// Deadlock freeness: on each cycle, at least one transition is enabled.

assign exist_enabled_transition =
{%- for input in inputs %}
| {{input}}_ena
{%- endfor -%}
{%- for net in stateful_nets %}
| {{net}}_ena
{%- endfor -%}
;

endmodule
Loading

0 comments on commit 4137d9a

Please sign in to comment.