~danilovesky/workcraft/trunk-bug-1395102

<a href="http://en.wikipedia.org/wiki/C-element" class="interwiki iw_wp" title="http://en.wikipedia.org/wiki/C-element">C-element</a> is a gate that synchronises the phases of its inputs. A symbol for a 2-input C-element and its timing diagram are shown in the figures below. Initially all the signals are in the low state. When both inputs <code>in1</code> and <code>in2</code> go high, the output <code>out</code> also switches to logical 1. It stays in this state until both inputs go low, at which stage the output switches to logical 0.

</p>

100

</tr>

101

102

<td class="col0 centeralign"> Symbol </td>

103

</tr>

104

</table></div>

105

</div><div class="wrap_column wrap_third plugin_wrap"><div class="table sectionedit9"><table class="inline">

106

107

108

</tr>

109

110

<td class="col0 centeralign"> Timing diagram </td>

111

</tr>

112

</table></div>

113

</div></div>

114

</div>

115

116

<h2 class="sectionedit10" id="modelling">Modelling</h2>

117

118

119

<p>

120

Let us model the C-element behaviour using STG formalism. Create a new STG work called <em>stg-celement</em> and <em>translate</em> the sequence of events in the timing diagram into a sequence of STG transitions. Basically you need to create a signal transition for each event of the timing diagram and capture the causality between these events by means of directed arcs between signal transitions.

121

</p>

122

123

<p>

124

Start with the reset phase of the C-element where <code>out-</code> event is caused by <code>in1-</code> and <code>in2-</code> events:

125

</p>

126

<ul>

127

128

Activate the <strong>signal transition generator</strong> <img src="../../../help/editor_tools-signal_transition.png" class="media" title="[T] Signal Transition" alt="[T] Signal Transition" />. Pay attention to the hint at the bottom of the screen: <em>Click to create a rising (or falling with Ctrl) transition of an output (or input with Shift) signal</em>.

129

</div></li>

130

131

Click the Editor panel in the location where you want the <code>out-</code> transition to appear.

132

</div></li>

133

134

Hold <kbd>Shift</kbd> and click in the desired location of <code>in1-</code> transition. The default name for the input signal is <code>in</code>, therefore you need to rename it. Go to the Property editor and change <em>in name</em> from <code>in</code> to <code>in1</code>.

135

</div></li>

136

137

Create <code>in2-</code> transition the same way as <code>in1-</code>.

138

</div></li>

139

140

Activate <strong>connection tool</strong> <img src="../../../help/editor_tools-connect.png" class="media" title="[C] Connect" alt="[C] Connect" />. Pay attention to the hints at the bottom of the screen. Initially the hint says <em>Click on the first component.</em> After the first component is chosen, the hint changes to <em>Click on the second component or create a node point. Hold Ctrl to connect continuously</em>.

141

</div></li>

142

143

Click <code>in1-</code>, move the mouse pointer to the <code>out-</code> transition and click again. A causality arc from <code>in1-</code> to <code>out-</code> will be created.

144

</div></li>

145

146

Repeat the connection procedure to capture causality between <code>in2-</code> and <code>out-</code> transitions.

147

</div></li>

148

</ul>

149

150

151

<p>

152

153

</p>

154

155

<p>

156

Similarly capture the set phase of the C-element:

157

</p>

158

<ul>

159

160

Create transitions <code>in1+</code>, <code>in2+</code> and <code>out+</code>. As before, rename the default <code>in</code> signal to <code>in1</code> and <code>in2</code> respectively.

161

</div></li>

162

163

Create causality arcs from <code>in1+</code> to <code>out+</code> and from <code>in2+</code> to <code>out+</code>.

164

</div></li>

165

166

Use the <strong>selection tool</strong> <img src="../../../help/editor_tools-select.png" class="media" title="[S] Select" alt="[S] Select" /> to rearrange the STG nodes similar to the following figure.

167

</div></li>

168

</ul>

169

170

171

<p>

172

173

</p>

174

175

<p>

176

Now connect the set and reset portions of the specification:

177

</p>

178

<ul>

179

180

The same as before, use <strong>connection tool</strong> <img src="../../../help/editor_tools-connect.png" class="media" title="[C] Connect" alt="[C] Connect" /> to introduce causality from <code>out+</code> to <code>in1-</code> and to <code>in2-</code>.

181

</div></li>

182

183

Create an arc from <code>out-</code> to <code>in1+</code>, but this time instead of a straight line connection use a polyline. After choosing the source of the connection (<code>out-</code> transition) click aside of the existing nodes - this will create a node point of a polyline. Continue forming the shape of the polyline by creating its node points, and finally choose the destination transition <code>in1+</code>.

184

</div></li>

185

186

Repeat the same procedure for creating a polyline connection from <code>out-</code> to <code>in2+</code>.

187

</div></li>

188

</ul>

189

190

191

<p>

192

193

</p>

194

195

<p>

196

Finally, specify the initial state of the C-element in accordance to the starting point of the timing diagram:

197

</p>

198

<ul>

199

200

Activate the <strong>selection tool</strong> <img src="../../../help/editor_tools-select.png" class="media" title="[S] Select" alt="[S] Select" />.

201

</div></li>

202

203

Select the arc from <code>out-</code> to <code>in1+</code> and in the Property editor set the <em>Tokens</em> value to 1.

204

</div></li>

205

206

Similarly put a token on the arc from <code>out-</code> to <code>in2+</code>.

207

</div></li>

208

</ul>

209

210

211

<p>

212

213

</p>

214

215

</div>

216

217

<h2 class="sectionedit11" id="verification_of_specification">Verification of specification</h2>

218

219

220

<p>

221

Activate the <strong>simulation tool</strong> <img src="../../../help/editor_tools-simulate.png" class="media" title="[M] Simulate" alt="[M] Simulate" /> and exercise the obtained STG model. Click one of the enabled signal transitions (they are highlighted in orange) to <em>evaluate</em> the STG into the next state. Note that the sequence of fired transitions is recorded in the simulation trace that is somewhat similar to the original timing diagram. Check that the simulation traces resemble to the intended behaviour of a C-element.

222

</p>

223

224

<p>

225

Before proceeding to the synthesis of the C-element it is a good idea to verify that its specification meets essential requirements, e.g. that it is consistent and is free from deadlocks.

226

</p>

227

228

<p>

229

To verify the signal consistency (i.e. that the rising and falling phases of each signal alternate in all possible execution traces) select <em>Tools→Verification→Check for consistency [MPSat]</em> menu item. Similarly, for deadlock checking select <em>Tools→Verification→Check for deadlocks [MPSat]</em> menu item.

230

</p>

231

232

<p>

233

If the specification violates consistency or has a deadlock then a trace leading to the problematic state will be reported. This trace can be simulated for better understanding the reported issues and for correcting them in the specification.

234

</p>

235

236

</div>

237

238

<h2 class="sectionedit12" id="synthesis">Synthesis</h2>

239

240

241

<p>

242

The STG specification can now be synthesised into an asynchronous circuit implementation either with Petrify or MPSat backend tools via <em>Tools→Synthesis</em> menu.

243

</p>

244

245

<p>

246

A complex gate solution obtained with Petrify (<em>Tools→Synthesis→Complex gate synthesis [Petrify]</em> menu item) is as follows <span class="wrap_important ">Note that solution is not unique and you may get a slightly different equation.</span>:

247

</p>

248

249

250

<p>

251

By opening the parenthesis one can obtained the following equation:

252

</p>

253

254

255

<p>

256

This equation can be directly mapped into an OR-AND complex gate whose function is <code>Z = A*B + C*D + E*F</code> ; let us call it <em>OA222</em> gate. The association of the C-element ports to the <em>OA222</em> gate pins is best described by the following Verilog module:

257

</p>

258

<pre class="code verilog"><span class="kw1">module</span> celement <span class="br0">(</span>in1<span class="sy0">,</span> in2<span class="sy0">,</span> out<span class="br0">)</span><span class="sy0">;</span>

259

<span class="kw1">input</span> in1<span class="sy0">;</span>

260

<span class="kw1">input</span> in2<span class="sy0">;</span>

261

<span class="kw1">output</span> out<span class="sy0">;</span>

262

OA222 inst_c <span class="br0">(</span>.A<span class="br0">(</span>in1<span class="br0">)</span><span class="sy0">,</span> .B<span class="br0">(</span>in2<span class="br0">)</span><span class="sy0">,</span> .C<span class="br0">(</span>in2<span class="br0">)</span><span class="sy0">,</span> .D<span class="br0">(</span>out<span class="br0">)</span><span class="sy0">,</span> .E<span class="br0">(</span>in1<span class="br0">)</span><span class="sy0">,</span> .F<span class="br0">(</span>out<span class="br0">)</span><span class="sy0">,</span> .Z<span class="br0">(</span>out<span class="br0">)</span><span class="br0">)</span><span class="sy0">;</span>

263

<span class="kw1">endmodule</span></pre>

264

265

</div>

266

267

<h2 class="sectionedit13" id="circuit_capturing">Circuit capturing</h2>

268

269

270

<p>

271

Create a new Digital Circuit work called <em>circuit-celement-cg</em> and capture the implementation suggested by Petrify in form of a gate-level netlist. <span class="wrap_info ">In the future versions of Workcraft the derivation of a circuit from the synthesis output will be automated, but for now please do it manually.</span>

272

</p>

273

<ul>

274

275

Activate <strong>functional generator</strong> <img src="../../../help/editor_tools-function.png" class="media" title="[F] Function" alt="[F] Function" /> and click in the desired position of the OR-AND complex gate.

276

</div></li>

277

278

Activate <strong>selection tool</strong> <img src="../../../help/editor_tools-select.png" class="media" title="[S] Select" alt="[S] Select" />.

279

</div></li>

280

281

Select the only pin of the newly created function component.

282

</div></li>

283

284

In the Property editor change the <em>Name</em> of the pin to <code>Z</code> and modify its <em>Set function</em> to <code>A*B+C*D+E*F</code>.

285

</div></li>

286

</ul>

287

288

289

<p>

290

291

</p>

292

<ul>

293

294

Select the function component and in the Property editor change its rendering type from <em>Box</em> to <em>Gate</em>.

295

</div></li>

296

</ul>

297

298

299

<p>

300

301

</p>

302

<ul>

303

304

Activate <strong>port generator</strong> <img src="../../../help/editor_tools-port.png" class="media" title="[P] Input/output port" alt="[P] Input/output port" />. Pay attention to the hint at the bottom of the screen: <em>Click to create an output port (hold Shift for input port)</em>.

305

</div></li>

306

307

Click in intended location of the output port. Note that by default the port will be named <code>out1</code> - you can change this name to <code>out</code> later.

308

</div></li>

309

310

Hold <kbd>Shift</kbd> and click in the desired locations of the input ports – they will be automatically assigned <code>in0</code> and <code>in1</code> names.

311

</div></li>

312

313

Switch to the selection tool. Choose the output port, go to the property editor and change port <em>Name</em> to <code>out</code>. Similarly change the name of input port <code>in0</code> to <code>in2</code>.

314

</div></li>

315

</ul>

316

317

318

<p>

319

320

</p>

321

<ul>

322

323

Activate <strong>connection tool</strong> <img src="../../../help/editor_tools-connect.png" class="media" title="[C] Connect" alt="[C] Connect" />.

324

</div></li>

325

326

Connect input ports <code>in1</code> to the 1<sup>st</sup> and 5<sup>th</sup> pins of the complex gate (<code>A</code> and <code>E</code> respectively).

327

</div></li>

328

329

Connect input ports <code>in2</code> to the 2<sup>nd</sup> and 3<sup>rd</sup> pins of the complex gate (<code>B</code> and <code>C</code> respectively).

330

</div></li>

331

332

Connect the output pin of the gate to the output port <code>out</code> and to the 4<sup>th</sup> and 6<sup>th</sup> inputs of the gate (<code>D</code> and <code>F</code> respectively).

333

</div></li>

334

</ul>

335

336

337

<p>

338

339

</p>

340

341

<p>

342

You may want to tidy up the circuit schematic and make it more readable by adding forks into the wires. This can be done with the <strong>joint generator</strong> <img src="../../../help/editor_tools-joint.png" class="media" title="[J] Joint" alt="[J] Joint" />. The resultant circuit should look similar to the following diagram.

343

</p>

344

345

<p>

346

347

</p>

348

349

</div>

350

351

<h2 class="sectionedit14" id="verification_of_implementation">Verification of implementation</h2>

352

353

354

<p>

355

Activate the <strong>simulation tool</strong> <img src="../../../help/editor_tools-simulate.png" class="media" title="[M] Simulate" alt="[M] Simulate" /> and simulate the captured complex gate implementation of the C-element. Ports, pins and wires are colour-coded: blue means low level and red means high level of the signal. Excited pins and ports are highlighted in orange.

356

</p>

357

358

<p>

359

Click one of the exited pins to toggle its logical value. Similar to the STG simulation, the sequence of signal events is recorded in the simulation trace and can be subsequently replayed for analysing the circuit behaviour.

360

</p>

361

362

<p>

363

Note that in simulation the C-element inputs are not restricted in any way, i.e. they can change in an unexpected manner causing malfunction of the circuit. This can be confirmed by checking the circuit for hazards <em>Tools→Verification→Check for hazards only</em> – the circuit has a hazard after the following trace: <code>0: in2+, in1+</code>.

364

</p>

365

366

<p>

367

Play this trace to discover that indeed, by the end of the trace the output of the C-element is excited and ready to switch to logical 1, but an unexpected <code>in1-</code> or <code>in2-</code> transition would disable it, that does not fit the specification.

368

</p>

369

370

<p>

371

Restrict the environment behaviour in such a way that the circuit only receives those inputs that are expected according to the specification. For example, you can feed the inverted value of C-element output to its inputs.

372

</p>

373

<ul>

374

375

Activate the <strong>selection tool</strong> <img src="../../../help/editor_tools-select.png" class="media" title="[S] Select" alt="[S] Select" />.

376

</div></li>

377

378

Select both input ports <code>in1</code> and <code>in2</code> (hold <kbd>Shift</kbd> and click each of them).

379

</div></li>

380

381

In the property editor assign the same <em>Set function</em> <code>!out</code> to both inputs (<code>!</code> means inversion – see <a href="..../../help/boolean_expression.html" class="wikilink1" title="help:boolean_expression">Boolean expressions</a> for details).

382

</div></li>

383

</ul>

384

385

386

<p>

387

388

</p>

389

390

<p>

391

Repeat the verification procedure to check if the circuit is free of hazards under the well behaved environment. Also check the circuit for deadlocks and verify if it conforms to the environment specification. All these verification steps can be run via <em>Tools→Verification→Check circuit for conformation, deadlocks and hazards (reuse unfolding)</em> menu.

392

</p>

393

394

<p>

395

Try to alter the circuit and verify if it still conforms to the environment, is deadlock-free and operates without hazards.

396

</p>

397

398

</div>

399

400

<h2 class="sectionedit15" id="solutions">Solutions</h2>

401

402

403

<p>

404

Download all the Workcraft models discussed in this tutorial here:

405

</p>

406

407

<p>

408

<span class="wrap_download "><a href="celement.tar.gz" class="media mediafile mf_gz" title="tutorial:stg:celement:celement.tar.gz (5.9 KB)">C-element models</a> (5.94 KiB, <acronym title="Modified: 2014-11-13 10:49.47">1d ago</acronym>)</span>

409

</p>

410

411

</div>

412

413

414

</div>

415

416

</div></div>

417

418

419

420

421

422

</div>

423

</div>

424

425

426

427

428

429

430

<a href="http://www.dokuwiki.org/donate" title="Donate" ><img

431

src="../../lib/tpl/dokuwiki-light-export/images/button-donate.gif" width="80" height="15" alt="Donate" /></a>

432

<a href="http://www.php.net" title="Powered by PHP" ><img

433

src="../../lib/tpl/dokuwiki-light-export/images/button-php.gif" width="80" height="15" alt="Powered by PHP" /></a>

434

<a href="http://validator.w3.org/check/referer" title="Valid HTML5" ><img

435

src="../../lib/tpl/dokuwiki-light-export/images/button-html5.png" width="80" height="15" alt="Valid HTML5" /></a>

436

<a href="http://jigsaw.w3.org/css-validator/check/referer?profile=css3" title="Valid CSS" ><img

437

src="../../lib/tpl/dokuwiki-light-export/images/button-css.png" width="80" height="15" alt="Valid CSS" /></a>

438

<a href="http://dokuwiki.org/" title="Driven by DokuWiki" ><img

439

src="../../lib/tpl/dokuwiki-light-export/images/button-dw.png" width="80" height="15" alt="Driven by DokuWiki" /></a>

440

</div>

441

442

443

</div>

444

</div></div>

445

446

</div></div>

447

448

449

450

</body>

451

</html>

452

Older »